Let U be given.
Assume HU.
We prove the intermediate
claim HexFam:
∃Fam ∈ 𝒫 B, ⋃ Fam = U.
Apply HexFam to the current goal.
Let Fam be given.
Assume HFampair.
We prove the intermediate
claim HFamPow:
Fam ∈ 𝒫 B.
An
exact proof term for the current goal is
(andEL (Fam ∈ 𝒫 B) (⋃ Fam = U) HFampair).
We prove the intermediate
claim HUnion:
⋃ Fam = U.
An
exact proof term for the current goal is
(andER (Fam ∈ 𝒫 B) (⋃ Fam = U) HFampair).
We prove the intermediate
claim HUnionFam:
⋃ Fam ∈ {⋃ Fam0|Fam0 ∈ 𝒫 B}.
An
exact proof term for the current goal is
(ReplI (𝒫 B) (λFam0 : set ⇒ ⋃ Fam0) Fam HFamPow).
rewrite the current goal using HUnion (from right to left).
An exact proof term for the current goal is HUnionFam.
Let U be given.
Assume HUUnion.
We prove the intermediate
claim HexFamPowRaw:
∃Fam ∈ 𝒫 B, U = ⋃ Fam.
An
exact proof term for the current goal is
(ReplE (𝒫 B) (λFam0 : set ⇒ ⋃ Fam0) U HUUnion).
We prove the intermediate
claim HexFamPow:
∃Fam ∈ 𝒫 B, ⋃ Fam = U.
Apply HexFamPowRaw to the current goal.
Let Fam be given.
Assume HFamPair.
We prove the intermediate
claim HFamPow:
Fam ∈ 𝒫 B.
An
exact proof term for the current goal is
(andEL (Fam ∈ 𝒫 B) (U = ⋃ Fam) HFamPair).
We prove the intermediate
claim HUnion:
U = ⋃ Fam.
An
exact proof term for the current goal is
(andER (Fam ∈ 𝒫 B) (U = ⋃ Fam) HFamPair).
We use Fam to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HFamPow.
rewrite the current goal using HUnion (from right to left).
Use reflexivity.