Let X and F be given.
Assume HXF.
We will prove TransSet (⋃x ∈ XF x) ∧ ∀y ∈ (⋃x ∈ XF x), TransSet y.
Apply andI to the current goal.
Let y be given.
Assume Hy: y ∈ ⋃x ∈ XF x.
Apply famunionE X F y Hy to the current goal.
Let x be given.
Assume H1.
Apply H1 to the current goal.
Assume Hx: x ∈ X.
Assume Hy: y ∈ F x.
We will prove y ⊆ ⋃x ∈ XF x.
We prove the intermediate claim LFx: ordinal (F x).
An exact proof term for the current goal is HXF x Hx.
Apply LFx to the current goal.
Assume HFx1 _.
Let z be given.
Assume Hz: z ∈ y.
We will prove z ∈ ⋃x ∈ XF x.
We prove the intermediate claim LzFx: z ∈ F x.
An exact proof term for the current goal is HFx1 y Hy z Hz.
An exact proof term for the current goal is famunionI X F x z Hx LzFx.
Let y be given.
Assume Hy: y ∈ ⋃x ∈ XF x.
We will prove TransSet y.
Apply famunionE X F y Hy to the current goal.
Let x be given.
Assume H1.
Apply H1 to the current goal.
Assume Hx: x ∈ X.
Assume Hy: y ∈ F x.
We prove the intermediate claim LFx: ordinal (F x).
An exact proof term for the current goal is HXF x Hx.
We prove the intermediate claim Ly: ordinal y.
An exact proof term for the current goal is ordinal_Hered (F x) LFx y Hy.
Apply Ly to the current goal.
Assume Hy1 _.
An exact proof term for the current goal is Hy1.
∎