Let X, D and A be given.
Assume Hmax: maximal_finite_intersection_property X D.
Assume HAsubX: A ⊆ X.
Assume Hmeet: ∀B : set, B ∈ D → A ∩ B ≠ Empty.
We will prove A ∈ D.
Apply Hmax to the current goal.
Assume HfipD HmaxD.
Set E to be the term D ∪ {A}.
We prove the intermediate claim HDsubE: D ⊆ E.
Let U be given.
Assume HU: U ∈ D.
An exact proof term for the current goal is (binunionI1 D {A} U HU).
We prove the intermediate claim HEfip: finite_intersection_property X E.
We will prove E ⊆ 𝒫 X ∧ ∀F : set, finite F → F ⊆ E → intersection_of_family X F ≠ Empty.
Apply andI to the current goal.
Apply HfipD to the current goal.
Assume HDpow _.
Let U be given.
Assume HU: U ∈ E.
Apply (binunionE' D {A} U (U ∈ 𝒫 X)) to the current goal.
Assume HUD: U ∈ D.
An exact proof term for the current goal is (HDpow U HUD).
Assume HUA: U ∈ {A}.
We prove the intermediate claim HUeq: U = A.
An exact proof term for the current goal is (SingE A U HUA).
rewrite the current goal using HUeq (from left to right).
An exact proof term for the current goal is (PowerI X A HAsubX).
An exact proof term for the current goal is HU.
Let F be given.
Assume HFfin: finite F.
Assume HFsub: F ⊆ E.
Apply (xm (A ∈ F)) to the current goal.
Assume HAinF: A ∈ F.
Set F0 to be the term F ∖ {A}.
We prove the intermediate claim HF0subF: F0 ⊆ F.
An exact proof term for the current goal is (setminus_Subq F {A}).
We prove the intermediate claim HF0fin: finite F0.
An exact proof term for the current goal is (Subq_finite F HFfin F0 HF0subF).
We prove the intermediate claim HF0subD: F0 ⊆ D.
Let U be given.
Assume HU0: U ∈ F0.
We prove the intermediate claim HUF: U ∈ F.
An exact proof term for the current goal is (setminusE1 F {A} U HU0).
We prove the intermediate claim HUE: U ∈ E.
An exact proof term for the current goal is (HFsub U HUF).
Apply (binunionE' D {A} U (U ∈ D)) to the current goal.
Assume HUD: U ∈ D.
An exact proof term for the current goal is HUD.
Assume HUA: U ∈ {A}.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((setminusE2 F {A} U HU0) HUA).
An exact proof term for the current goal is HUE.
Set B0 to be the term intersection_of_family X F0.
We prove the intermediate claim HB0inD: B0 ∈ D.
An exact proof term for the current goal is (Lemma37_2a_max_fip_finite_intersections_in X D (andI (finite_intersection_property X D) (∀E0 : set, D ⊆ E0 → finite_intersection_property X E0 → E0 ⊆ D) HfipD HmaxD) F0 HF0fin HF0subD).
We prove the intermediate claim Hnon: A ∩ B0 ≠ Empty.
An exact proof term for the current goal is (Hmeet B0 HB0inD).
We prove the intermediate claim HsubInt: (A ∩ B0) ⊆ intersection_of_family X F.
Let x be given.
Assume Hx: x ∈ A ∩ B0.
We prove the intermediate claim HxA: x ∈ A.
An exact proof term for the current goal is (binintersectE1 A B0 x Hx).
We prove the intermediate claim HxB0: x ∈ B0.
An exact proof term for the current goal is (binintersectE2 A B0 x Hx).
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λz : set ⇒ ∀T : set, T ∈ F0 → z ∈ T) x HxB0).
We prove the intermediate claim HallF0: ∀T : set, T ∈ F0 → x ∈ T.
An exact proof term for the current goal is (SepE2 X (λz : set ⇒ ∀T : set, T ∈ F0 → z ∈ T) x HxB0).
We prove the intermediate claim HallF: ∀T : set, T ∈ F → x ∈ T.
Let T be given.
Assume HTF: T ∈ F.
We will prove x ∈ T.
Apply (xm (T = A)) to the current goal.
Assume HTA: T = A.
rewrite the current goal using HTA (from left to right).
An exact proof term for the current goal is HxA.
Assume HTnA: ¬ (T = A).
We prove the intermediate claim HTnSing: T ∉ {A}.
Assume HTSing: T ∈ {A}.
We prove the intermediate claim HTA: T = A.
An exact proof term for the current goal is (SingE A T HTSing).
An exact proof term for the current goal is (HTnA HTA).
We prove the intermediate claim HTF0: T ∈ F0.
An exact proof term for the current goal is (setminusI F {A} T HTF HTnSing).
An exact proof term for the current goal is (HallF0 T HTF0).
An exact proof term for the current goal is (intersection_of_familyI X F x HxX HallF).
Apply (nonempty_has_element (A ∩ B0) Hnon) to the current goal.
Let x be given.
Assume Hx: x ∈ A ∩ B0.
We will prove intersection_of_family X F ≠ Empty.
Apply (elem_implies_nonempty (intersection_of_family X F) x) to the current goal.
An exact proof term for the current goal is (HsubInt x Hx).
Assume HAnot: ¬ (A ∈ F).
Apply HfipD to the current goal.
Assume _ HDfip.
We prove the intermediate claim HFsubD: F ⊆ D.
Let U be given.
Assume HUF: U ∈ F.
We prove the intermediate claim HUE: U ∈ E.
An exact proof term for the current goal is (HFsub U HUF).
Apply (binunionE' D {A} U (U ∈ D)) to the current goal.
Assume HUD: U ∈ D.
An exact proof term for the current goal is HUD.
Assume HUA: U ∈ {A}.
Apply FalseE to the current goal.
We prove the intermediate claim HUeq: U = A.
An exact proof term for the current goal is (SingE A U HUA).
We prove the intermediate claim HAinF: A ∈ F.
We will prove A ∈ F.
rewrite the current goal using HUeq (from right to left).
An exact proof term for the current goal is HUF.
An exact proof term for the current goal is (HAnot HAinF).
An exact proof term for the current goal is HUE.
An exact proof term for the current goal is (HDfip F HFfin HFsubD).
We prove the intermediate claim HEsubD: E ⊆ D.
An exact proof term for the current goal is (HmaxD E HDsubE HEfip).
An exact proof term for the current goal is (HEsubD A (binunionI2 D {A} A (SingI A))).
∎