Let X and D be given.
Assume Hmax: maximal_finite_intersection_property X D.
Let F be given.
Assume HFfin: finite F.
Assume HFsub: F ⊆ D.
We will prove intersection_of_family X F ∈ D.
Apply Hmax to the current goal.
Assume HfipD HmaxD.
We prove the intermediate claim HDpow: D ⊆ 𝒫 X.
An exact proof term for the current goal is (andEL (D ⊆ 𝒫 X) (∀F0 : set, finite F0 → F0 ⊆ D → intersection_of_family X F0 ≠ Empty) HfipD).
We prove the intermediate claim HDfip: ∀F0 : set, finite F0 → F0 ⊆ D → intersection_of_family X F0 ≠ Empty.
An exact proof term for the current goal is (andER (D ⊆ 𝒫 X) (∀F0 : set, finite F0 → F0 ⊆ D → intersection_of_family X F0 ≠ Empty) HfipD).
Set B to be the term intersection_of_family X F.
Set E to be the term D ∪ {B}.
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 {B} U HU).
We prove the intermediate claim HEfip: finite_intersection_property X E.
We will prove E ⊆ 𝒫 X ∧ ∀G : set, finite G → G ⊆ E → intersection_of_family X G ≠ Empty.
Apply andI to the current goal.
Let U be given.
Assume HU: U ∈ E.
Apply (binunionE' D {B} U (U ∈ 𝒫 X)) to the current goal.
Assume HUD: U ∈ D.
An exact proof term for the current goal is (HDpow U HUD).
Assume HUB: U ∈ {B}.
We prove the intermediate claim HUeq: U = B.
An exact proof term for the current goal is (SingE B U HUB).
rewrite the current goal using HUeq (from left to right).
We prove the intermediate claim HBsubX: B ⊆ X.
An exact proof term for the current goal is (intersection_of_family_sub_X X F).
An exact proof term for the current goal is (PowerI X B HBsubX).
An exact proof term for the current goal is HU.
Let G be given.
Assume HGfin: finite G.
Assume HGsub: G ⊆ E.
Apply (xm (B ∈ G)) to the current goal.
Assume HBInG: B ∈ G.
Set G0 to be the term G ∖ {B}.
Set H to be the term G0 ∪ F.
We prove the intermediate claim HG0subG: G0 ⊆ G.
An exact proof term for the current goal is (setminus_Subq G {B}).
We prove the intermediate claim HG0fin: finite G0.
An exact proof term for the current goal is (Subq_finite G HGfin G0 HG0subG).
We prove the intermediate claim Hfin: finite H.
An exact proof term for the current goal is (binunion_finite G0 HG0fin F HFfin).
We prove the intermediate claim HG0subD: G0 ⊆ D.
Let U be given.
Assume HU0: U ∈ G0.
We prove the intermediate claim HUG: U ∈ G.
An exact proof term for the current goal is (setminusE1 G {B} U HU0).
We prove the intermediate claim HUE: U ∈ E.
An exact proof term for the current goal is (HGsub U HUG).
Apply (binunionE' D {B} U (U ∈ D)) to the current goal.
Assume HUD: U ∈ D.
An exact proof term for the current goal is HUD.
Assume HUB: U ∈ {B}.
Apply FalseE to the current goal.
An exact proof term for the current goal is ((setminusE2 G {B} U HU0) HUB).
An exact proof term for the current goal is HUE.
We prove the intermediate claim HsubD: H ⊆ D.
Let U be given.
Assume HU: U ∈ H.
Apply (binunionE' G0 F U (U ∈ D)) to the current goal.
Assume HUG0: U ∈ G0.
An exact proof term for the current goal is (HG0subD U HUG0).
Assume HUF: U ∈ F.
An exact proof term for the current goal is (HFsub U HUF).
An exact proof term for the current goal is HU.
We prove the intermediate claim HnonH: intersection_of_family X H ≠ Empty.
An exact proof term for the current goal is (HDfip H Hfin HsubD).
Apply (nonempty_has_element (intersection_of_family X H) HnonH) to the current goal.
Let x be given.
Assume HxH: x ∈ intersection_of_family X H.
We will prove intersection_of_family X G ≠ Empty.
Apply (elem_implies_nonempty (intersection_of_family X G) x) to the current goal.
We will prove x ∈ intersection_of_family X G.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (SepE1 X (λz : set ⇒ ∀T : set, T ∈ H → z ∈ T) x HxH).
We prove the intermediate claim HallH: ∀T : set, T ∈ H → x ∈ T.
An exact proof term for the current goal is (SepE2 X (λz : set ⇒ ∀T : set, T ∈ H → z ∈ T) x HxH).
We prove the intermediate claim HallG: ∀T : set, T ∈ G → x ∈ T.
Let T be given.
Assume HTG: T ∈ G.
We will prove x ∈ T.
Apply (xm (T = B)) to the current goal.
Assume HTB: T = B.
rewrite the current goal using HTB (from left to right).
We prove the intermediate claim HallF: ∀U : set, U ∈ F → x ∈ U.
Let U be given.
Assume HUF: U ∈ F.
An exact proof term for the current goal is (HallH U (binunionI2 G0 F U HUF)).
An exact proof term for the current goal is (intersection_of_familyI X F x HxX HallF).
Assume HTnB: ¬ (T = B).
We prove the intermediate claim HTnSing: T ∉ {B}.
Assume HTSing: T ∈ {B}.
We prove the intermediate claim HTB: T = B.
An exact proof term for the current goal is (SingE B T HTSing).
An exact proof term for the current goal is (HTnB HTB).
We prove the intermediate claim HTG0: T ∈ G0.
An exact proof term for the current goal is (setminusI G {B} T HTG HTnSing).
An exact proof term for the current goal is (HallH T (binunionI1 G0 F T HTG0)).
An exact proof term for the current goal is (intersection_of_familyI X G x HxX HallG).
Assume HBnot: ¬ (B ∈ G).
We prove the intermediate claim HGsubD: G ⊆ D.
Let U be given.
Assume HUG: U ∈ G.
We prove the intermediate claim HUE: U ∈ E.
An exact proof term for the current goal is (HGsub U HUG).
Apply (binunionE' D {B} U (U ∈ D)) to the current goal.
Assume HUD: U ∈ D.
An exact proof term for the current goal is HUD.
Assume HUB: U ∈ {B}.
Apply FalseE to the current goal.
We prove the intermediate claim HUBEq: U = B.
An exact proof term for the current goal is (SingE B U HUB).
We prove the intermediate claim HBInG: B ∈ G.
We will prove B ∈ G.
rewrite the current goal using HUBEq (from right to left).
An exact proof term for the current goal is HUG.
An exact proof term for the current goal is (HBnot HBInG).
An exact proof term for the current goal is HUE.
An exact proof term for the current goal is (HDfip G HGfin HGsubD).
We prove the intermediate claim HEsubD: E ⊆ D.
An exact proof term for the current goal is (HmaxD E HDsubE HEfip).
We will prove intersection_of_family X F ∈ D.
An exact proof term for the current goal is (HEsubD B (binunionI2 D {B} B (SingI B))).
∎