Apply andI to the current goal.

Let b be given.

We will prove b ∈ 𝒫 X.

We prove the intermediate claim Hb_in_finite: b ∈ finite_intersections_of X S.

An exact proof term for the current goal is (SepE1 (finite_intersections_of X S) (λb0 ⇒ b0 ≠ Empty) b Hb).

We prove the intermediate claim Hex: ∃F ∈ finite_subcollections S, b = intersection_of_family X F.

An exact proof term for the current goal is (ReplE (finite_subcollections S) (λF ⇒ intersection_of_family X F) b Hb_in_finite).

Apply Hex to the current goal.

Let F be given.

Assume HF_and_eq.

Apply HF_and_eq to the current goal.

Assume HF: F ∈ finite_subcollections S.

Assume Hbeq: b = intersection_of_family X F.

We will prove b ∈ 𝒫 X.

Apply PowerI to the current goal.

Let x be given.

Assume Hx: x ∈ b.

We will prove x ∈ X.

We prove the intermediate claim Hx_intersect: x ∈ intersection_of_family X F.

rewrite the current goal using Hbeq (from right to left).

An exact proof term for the current goal is Hx.

An exact proof term for the current goal is (SepE1 X (λx0 ⇒ ∀U : set, U ∈ F → x0 ∈ U) x Hx_intersect).

Let x be given.

Assume Hx: x ∈ X.

We will prove ∃b ∈ basis_of_subbasis X S, x ∈ b.

We prove the intermediate claim HSsub: S ⊆ 𝒫 X.

An exact proof term for the current goal is (andEL (S ⊆ 𝒫 X) (⋃ S = X) HS).

We prove the intermediate claim HUnionS: ⋃ S = X.

An exact proof term for the current goal is (andER (S ⊆ 𝒫 X) (⋃ S = X) HS).

We prove the intermediate claim HxUnionS: x ∈ ⋃ S.

rewrite the current goal using HUnionS (from left to right).

An exact proof term for the current goal is Hx.

Apply (UnionE_impred S x HxUnionS) to the current goal.

Let s be given.

Assume Hxs: x ∈ s.

Assume HsS: s ∈ S.

We prove the intermediate claim HsNe: s ≠ Empty.

Assume Hseq: s = Empty.

We prove the intermediate claim HxEmpty: x ∈ Empty.

rewrite the current goal using Hseq (from right to left).

An exact proof term for the current goal is Hxs.

An exact proof term for the current goal is (EmptyE x HxEmpty).

We prove the intermediate claim HsInBasis: s ∈ basis_of_subbasis X S.

An exact proof term for the current goal is (subbasis_elem_in_basis X S s HS HsS HsNe).

We use s to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is HsInBasis.

An exact proof term for the current goal is Hxs.

Let b1 be given.

Assume Hb1: b1 ∈ basis_of_subbasis X S.

Let b2 be given.

Assume Hb2: b2 ∈ basis_of_subbasis X S.

Let x be given.

Assume Hxb1: x ∈ b1.

Assume Hxb2: x ∈ b2.

We will prove ∃b3 ∈ basis_of_subbasis X S, x ∈ b3 ∧ b3 ⊆ b1 ∩ b2.

Set b3 to be the term b1 ∩ b2.

We prove the intermediate claim Hxb3: x ∈ b3.

Apply binintersectI to the current goal.

An exact proof term for the current goal is Hxb1.

An exact proof term for the current goal is Hxb2.

We prove the intermediate claim Hb3_ne: b3 ≠ Empty.

Assume Hempty: b3 = Empty.

We prove the intermediate claim Hx_in_empty: x ∈ Empty.

rewrite the current goal using Hempty (from right to left).

An exact proof term for the current goal is Hxb3.

An exact proof term for the current goal is (EmptyE x Hx_in_empty).

We use b3 to witness the existential quantifier.

Apply andI to the current goal.

We will prove b3 ∈ basis_of_subbasis X S.

We prove the intermediate claim Hb1_finite: b1 ∈ finite_intersections_of X S.

An exact proof term for the current goal is (SepE1 (finite_intersections_of X S) (λb0 ⇒ b0 ≠ Empty) b1 Hb1).

We prove the intermediate claim Hb2_finite: b2 ∈ finite_intersections_of X S.

An exact proof term for the current goal is (SepE1 (finite_intersections_of X S) (λb0 ⇒ b0 ≠ Empty) b2 Hb2).

We prove the intermediate claim Hex1: ∃F1 ∈ finite_subcollections S, b1 = intersection_of_family X F1.

An exact proof term for the current goal is (ReplE (finite_subcollections S) (λF ⇒ intersection_of_family X F) b1 Hb1_finite).

Apply Hex1 to the current goal.

Let F1 be given.

Assume HF1_and_eq1.

Apply HF1_and_eq1 to the current goal.

Assume HF1: F1 ∈ finite_subcollections S.

Assume Hb1eq: b1 = intersection_of_family X F1.

We prove the intermediate claim Hex2: ∃F2 ∈ finite_subcollections S, b2 = intersection_of_family X F2.

An exact proof term for the current goal is (ReplE (finite_subcollections S) (λF ⇒ intersection_of_family X F) b2 Hb2_finite).

Apply Hex2 to the current goal.

Let F2 be given.

Assume HF2_and_eq2.

Apply HF2_and_eq2 to the current goal.

Assume HF2: F2 ∈ finite_subcollections S.

Assume Hb2eq: b2 = intersection_of_family X F2.

Set F12 to be the term F1 ∪ F2.

We prove the intermediate claim HF12_finite: F12 ∈ finite_subcollections S.

We will prove F12 ∈ {F ∈ 𝒫 S|finite F}.

We prove the intermediate claim HF12_sub: F12 ⊆ S.

We prove the intermediate claim HF1_sub: F1 ⊆ S.

We prove the intermediate claim HF1_power: F1 ∈ 𝒫 S.

An exact proof term for the current goal is (SepE1 (𝒫 S) (λF0 ⇒ finite F0) F1 HF1).

An exact proof term for the current goal is (PowerE S F1 HF1_power).

We prove the intermediate claim HF2_sub: F2 ⊆ S.

We prove the intermediate claim HF2_power: F2 ∈ 𝒫 S.

An exact proof term for the current goal is (SepE1 (𝒫 S) (λF0 ⇒ finite F0) F2 HF2).

An exact proof term for the current goal is (PowerE S F2 HF2_power).

An exact proof term for the current goal is (binunion_Subq_min F1 F2 S HF1_sub HF2_sub).

We prove the intermediate claim HF12_power: F12 ∈ 𝒫 S.

Apply PowerI to the current goal.

An exact proof term for the current goal is HF12_sub.

We prove the intermediate claim HF12_is_finite: finite F12.

We prove the intermediate claim HF1_is_finite: finite F1.

An exact proof term for the current goal is (SepE2 (𝒫 S) (λF0 ⇒ finite F0) F1 HF1).

We prove the intermediate claim HF2_is_finite: finite F2.

An exact proof term for the current goal is (SepE2 (𝒫 S) (λF0 ⇒ finite F0) F2 HF2).

An exact proof term for the current goal is (binunion_finite F1 HF1_is_finite F2 HF2_is_finite).

An exact proof term for the current goal is (SepI (𝒫 S) (λF ⇒ finite F) F12 HF12_power HF12_is_finite).

We prove the intermediate claim Hb3_eq: b3 = intersection_of_family X F12.

Apply set_ext to the current goal.

Let z be given.

Assume Hz: z ∈ b3.

We will prove z ∈ intersection_of_family X F12.

We prove the intermediate claim Hzb1: z ∈ b1.

An exact proof term for the current goal is (binintersectE1 b1 b2 z Hz).

We prove the intermediate claim Hzb2: z ∈ b2.

An exact proof term for the current goal is (binintersectE2 b1 b2 z Hz).

We prove the intermediate claim Hz_intersect1: z ∈ intersection_of_family X F1.

rewrite the current goal using Hb1eq (from right to left).

An exact proof term for the current goal is Hzb1.

We prove the intermediate claim Hz_intersect2: z ∈ intersection_of_family X F2.

rewrite the current goal using Hb2eq (from right to left).

An exact proof term for the current goal is Hzb2.

We will prove z ∈ intersection_of_family X F12.

We prove the intermediate claim Hz_in_X: z ∈ X.

An exact proof term for the current goal is (SepE1 X (λx ⇒ ∀U : set, U ∈ F1 → x ∈ U) z Hz_intersect1).

We prove the intermediate claim Hz_all1: ∀U : set, U ∈ F1 → z ∈ U.

An exact proof term for the current goal is (SepE2 X (λx ⇒ ∀U : set, U ∈ F1 → x ∈ U) z Hz_intersect1).

We prove the intermediate claim Hz_all2: ∀U : set, U ∈ F2 → z ∈ U.

An exact proof term for the current goal is (SepE2 X (λx ⇒ ∀U : set, U ∈ F2 → x ∈ U) z Hz_intersect2).

We prove the intermediate claim Hz_all12: ∀U : set, U ∈ F12 → z ∈ U.

Let U be given.

Assume HU: U ∈ F12.

We will prove z ∈ U.

Apply (binunionE F1 F2 U HU) to the current goal.

Assume HUF1: U ∈ F1.

An exact proof term for the current goal is (Hz_all1 U HUF1).

Assume HUF2: U ∈ F2.

An exact proof term for the current goal is (Hz_all2 U HUF2).

An exact proof term for the current goal is (SepI X (λx ⇒ ∀U : set, U ∈ F12 → x ∈ U) z Hz_in_X Hz_all12).

Let z be given.

Assume Hz: z ∈ intersection_of_family X F12.

We will prove z ∈ b3.

We prove the intermediate claim Hz_in_X: z ∈ X.

An exact proof term for the current goal is (SepE1 X (λx ⇒ ∀U : set, U ∈ F12 → x ∈ U) z Hz).

We prove the intermediate claim Hz_all12: ∀U : set, U ∈ F12 → z ∈ U.

An exact proof term for the current goal is (SepE2 X (λx ⇒ ∀U : set, U ∈ F12 → x ∈ U) z Hz).

We prove the intermediate claim Hz_all1: ∀U : set, U ∈ F1 → z ∈ U.

Let U be given.

Assume HU: U ∈ F1.

We will prove z ∈ U.

An exact proof term for the current goal is (Hz_all12 U (binunionI1 F1 F2 U HU)).

We prove the intermediate claim Hz_all2: ∀U : set, U ∈ F2 → z ∈ U.

Let U be given.

Assume HU: U ∈ F2.

We will prove z ∈ U.

An exact proof term for the current goal is (Hz_all12 U (binunionI2 F1 F2 U HU)).

We prove the intermediate claim Hz_intersect1: z ∈ intersection_of_family X F1.

An exact proof term for the current goal is (SepI X (λx ⇒ ∀U : set, U ∈ F1 → x ∈ U) z Hz_in_X Hz_all1).

We prove the intermediate claim Hz_intersect2: z ∈ intersection_of_family X F2.

An exact proof term for the current goal is (SepI X (λx ⇒ ∀U : set, U ∈ F2 → x ∈ U) z Hz_in_X Hz_all2).

We prove the intermediate claim Hzb1: z ∈ b1.

rewrite the current goal using Hb1eq (from left to right).

An exact proof term for the current goal is Hz_intersect1.

We prove the intermediate claim Hzb2: z ∈ b2.

rewrite the current goal using Hb2eq (from left to right).

An exact proof term for the current goal is Hz_intersect2.

An exact proof term for the current goal is (binintersectI b1 b2 z Hzb1 Hzb2).

We prove the intermediate claim H_intersect_ne: intersection_of_family X F12 ≠ Empty.

Assume Hempty_intersect: intersection_of_family X F12 = Empty.

We prove the intermediate claim Hb3_empty: b3 = Empty.

rewrite the current goal using Hb3_eq (from left to right).

An exact proof term for the current goal is Hempty_intersect.

An exact proof term for the current goal is (Hb3_ne Hb3_empty).

We prove the intermediate claim H_intersect_in_basis: intersection_of_family X F12 ∈ basis_of_subbasis X S.

An exact proof term for the current goal is (finite_intersection_in_basis X S F12 HF12_finite H_intersect_ne).

We prove the intermediate claim Hb3_in_basis: b3 ∈ basis_of_subbasis X S.

rewrite the current goal using Hb3_eq (from left to right).

An exact proof term for the current goal is H_intersect_in_basis.

An exact proof term for the current goal is Hb3_in_basis.

Apply andI to the current goal.

An exact proof term for the current goal is Hxb3.

An exact proof term for the current goal is (Subq_ref (b1 ∩ b2)).