Let X, T and UFam be given.
Assume HT Hfam.
We prove the intermediate
claim Hchunk1:
((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀UFam' ∈ 𝒫 T, ⋃ UFam' ∈ T).
An
exact proof term for the current goal is
(andEL (((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) ∧ (∀UFam' ∈ 𝒫 T, ⋃ UFam' ∈ T)) (∀U ∈ T, ∀V ∈ T, U ∩ V ∈ T) HT).
We prove the intermediate
claim Hunion_axiom:
∀UFam' ∈ 𝒫 T, ⋃ UFam' ∈ T.
An
exact proof term for the current goal is
(andER ((T ⊆ 𝒫 X ∧ Empty ∈ T) ∧ X ∈ T) (∀UFam' ∈ 𝒫 T, ⋃ UFam' ∈ T) Hchunk1).
An exact proof term for the current goal is (Hunion_axiom UFam Hfam).
∎