Let X, Tx and U be given.
Set Fam to be the term
{V ∈ Tx|V ⊆ U}.
We prove the intermediate
claim HFamSub:
Fam ⊆ Tx.
Let V be given.
An
exact proof term for the current goal is
(SepE1 Tx (λW : set ⇒ W ⊆ U) V HV).
We prove the intermediate
claim HFamPow:
Fam ∈ 𝒫 Tx.
An
exact proof term for the current goal is
(PowerI Tx Fam HFamSub).
We prove the intermediate
claim HUnionFamIn:
⋃ Fam ∈ Tx.
We prove the intermediate
claim HUeq:
U = ⋃ Fam.
Let x be given.
We prove the intermediate
claim HexV:
∃V : set, V ∈ Tx ∧ x ∈ V ∧ V ⊆ U.
An exact proof term for the current goal is (Hnbhd x HxU).
Apply HexV to the current goal.
Let V be given.
We prove the intermediate
claim HVTx_x:
V ∈ Tx ∧ x ∈ V.
An
exact proof term for the current goal is
(andEL (V ∈ Tx ∧ x ∈ V) (V ⊆ U) HVpack).
We prove the intermediate
claim HVTx:
V ∈ Tx.
An
exact proof term for the current goal is
(andEL (V ∈ Tx) (x ∈ V) HVTx_x).
We prove the intermediate
claim HxV:
x ∈ V.
An
exact proof term for the current goal is
(andER (V ∈ Tx) (x ∈ V) HVTx_x).
We prove the intermediate
claim HVSubU:
V ⊆ U.
An
exact proof term for the current goal is
(andER (V ∈ Tx ∧ x ∈ V) (V ⊆ U) HVpack).
We prove the intermediate
claim HVFam:
V ∈ Fam.
An
exact proof term for the current goal is
(SepI Tx (λW : set ⇒ W ⊆ U) V HVTx HVSubU).
An
exact proof term for the current goal is
(UnionI Fam x V HxV HVFam).
Let x be given.
Let V be given.
We prove the intermediate
claim HVSubU:
V ⊆ U.
An
exact proof term for the current goal is
(SepE2 Tx (λW : set ⇒ W ⊆ U) V HVFam).
An exact proof term for the current goal is (HVSubU x HxV).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is HUnionFamIn.
∎