Let X, B and b be given.
We prove the intermediate
claim H1:
(B ⊆ 𝒫 X ∧ (∀x ∈ X, ∃b0 ∈ B, x ∈ b0)) ∧ (∀b1 ∈ B, ∀b2 ∈ B, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ B, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2).
An exact proof term for the current goal is HB.
We prove the intermediate
claim H2:
B ⊆ 𝒫 X ∧ (∀x ∈ X, ∃b0 ∈ B, x ∈ b0).
An
exact proof term for the current goal is
(andEL (B ⊆ 𝒫 X ∧ (∀x ∈ X, ∃b0 ∈ B, x ∈ b0)) (∀b1 ∈ B, ∀b2 ∈ B, ∀x : set, x ∈ b1 → x ∈ b2 → ∃b3 ∈ B, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2) H1).
We prove the intermediate
claim HBPower:
B ⊆ 𝒫 X.
An
exact proof term for the current goal is
(andEL (B ⊆ 𝒫 X) (∀x ∈ X, ∃b0 ∈ B, x ∈ b0) H2).
We prove the intermediate
claim HbPower:
b ∈ 𝒫 X.
An exact proof term for the current goal is (HBPower b Hb).
An
exact proof term for the current goal is
(PowerE X b HbPower).