Let U be given.
Let x be given.
Assume HxU.
We prove the intermediate
claim HUsubX:
U ⊆ X.
An
exact proof term for the current goal is
(PowerE X U (SepE1 (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ B, x0 ∈ b ∧ b ⊆ U0) U HU)).
We prove the intermediate
claim HxX:
x ∈ X.
An exact proof term for the current goal is (HUsubX x HxU).
We prove the intermediate
claim HUprop:
∀x0 ∈ U, ∃b ∈ B, x0 ∈ b ∧ b ⊆ U.
An
exact proof term for the current goal is
(SepE2 (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ B, x0 ∈ b ∧ b ⊆ U0) U HU).
We prove the intermediate
claim Hexb:
∃b ∈ B, x ∈ b ∧ b ⊆ U.
An exact proof term for the current goal is (HUprop x HxU).
Apply Hexb to the current goal.
Let b be given.
Assume Hbpair.
We prove the intermediate
claim HbB:
b ∈ B.
An
exact proof term for the current goal is
(andEL (b ∈ B) (x ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate
claim Hbprop:
x ∈ b ∧ b ⊆ U.
An
exact proof term for the current goal is
(andER (b ∈ B) (x ∈ b ∧ b ⊆ U) Hbpair).
We prove the intermediate
claim Hxb:
x ∈ b.
An
exact proof term for the current goal is
(andEL (x ∈ b) (b ⊆ U) Hbprop).
We prove the intermediate
claim HbsubU:
b ⊆ U.
An
exact proof term for the current goal is
(andER (x ∈ b) (b ⊆ U) Hbprop).
We prove the intermediate
claim Hexb':
∃b' ∈ B', x ∈ b' ∧ b' ⊆ b.
An exact proof term for the current goal is (Hcond x HxX b HbB Hxb).
Apply Hexb' to the current goal.
Let b' be given.
Assume Hb'pair.
We prove the intermediate
claim Hb'B:
b' ∈ B'.
An
exact proof term for the current goal is
(andEL (b' ∈ B') (x ∈ b' ∧ b' ⊆ b) Hb'pair).
We prove the intermediate
claim Hb'prop:
x ∈ b' ∧ b' ⊆ b.
An
exact proof term for the current goal is
(andER (b' ∈ B') (x ∈ b' ∧ b' ⊆ b) Hb'pair).
We prove the intermediate
claim Hxb':
x ∈ b'.
An
exact proof term for the current goal is
(andEL (x ∈ b') (b' ⊆ b) Hb'prop).
We prove the intermediate
claim Hb'subb:
b' ⊆ b.
An
exact proof term for the current goal is
(andER (x ∈ b') (b' ⊆ b) Hb'prop).
We use b' to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is Hb'B.
Apply andI to the current goal.
An exact proof term for the current goal is Hxb'.
An
exact proof term for the current goal is
(Subq_tra b' b U Hb'subb HbsubU).