Let X, Tx and Fam be given.
Assume HTx: topology_on X Tx.
Assume Hcover: open_cover_of X Tx Fam.
Assume Hnofin: ¬ (has_finite_subcover X Tx Fam).
We will prove ∃J le net0 : set, directed_set J le ∧ total_function_on net0 J X ∧ functional_graph net0 ∧ graph_domain_subset net0 J ∧ (∀sub K leK phi x : set, subnet_of_witness net0 sub J le K leK X phi → ¬ (net_converges_on X Tx sub K leK x)).
Set J to be the term finite_subcollections Fam.
Set le to be the term inclusion_rel J.
Set pickx to be the term (λF : set ⇒ Eps_i (λx : set ⇒ x ∈ X ∧ ¬ (x ∈ ⋃ F))).
Set net0 to be the term graph J pickx.
We prove the intermediate claim HdirJ: directed_set J le.
An exact proof term for the current goal is (finite_subcollections_directed_by_subset Fam).
We prove the intermediate claim Hpick_spec: ∀F : set, F ∈ J → pickx F ∈ X ∧ ¬ (pickx F ∈ ⋃ F).
Let F be given.
Assume HFJ: F ∈ J.
We prove the intermediate claim HFpow: F ∈ 𝒫 Fam.
An exact proof term for the current goal is (SepE1 (𝒫 Fam) (λF0 : set ⇒ finite F0) F HFJ).
We prove the intermediate claim HFfin: finite F.
An exact proof term for the current goal is (SepE2 (𝒫 Fam) (λF0 : set ⇒ finite F0) F HFJ).
We prove the intermediate claim HFsub: F ⊆ Fam.
An exact proof term for the current goal is (PowerE Fam F HFpow).
We prove the intermediate claim Hnotcov: ¬ (X ⊆ ⋃ F).
Assume Hcov: X ⊆ ⋃ F.
Apply Hnofin to the current goal.
Apply (has_finite_subcoverI X Tx Fam F) to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HFsub.
An exact proof term for the current goal is HFfin.
An exact proof term for the current goal is Hcov.
We prove the intermediate claim Hexx: ∃x : set, x ∈ X ∧ ¬ (x ∈ ⋃ F).
We prove the intermediate claim Hex': ∃x : set, ¬ (x ∈ X → x ∈ ⋃ F).
An exact proof term for the current goal is (not_all_ex_demorgan_i (λx : set ⇒ x ∈ X → x ∈ ⋃ F) Hnotcov).
Apply Hex' to the current goal.
Let x be given.
Assume Hnx: ¬ (x ∈ X → x ∈ ⋃ F).
We use x to witness the existential quantifier.
An exact proof term for the current goal is (not_imp (x ∈ X) (x ∈ ⋃ F) Hnx).
Apply Hexx to the current goal.
Let x be given.
Assume Hx: x ∈ X ∧ ¬ (x ∈ ⋃ F).
An exact proof term for the current goal is (Eps_i_ax (λx0 : set ⇒ x0 ∈ X ∧ ¬ (x0 ∈ ⋃ F)) x Hx).
We prove the intermediate claim Hpick_in: ∀F : set, F ∈ J → pickx F ∈ X.
Let F be given.
Assume HFJ: F ∈ J.
We prove the intermediate claim Hspec: pickx F ∈ X ∧ ¬ (pickx F ∈ ⋃ F).
An exact proof term for the current goal is (Hpick_spec F HFJ).
An exact proof term for the current goal is (andEL (pickx F ∈ X) (¬ (pickx F ∈ ⋃ F)) Hspec).
We prove the intermediate claim Htotnet: total_function_on net0 J X.
An exact proof term for the current goal is (total_function_on_graph J X pickx Hpick_in).
We prove the intermediate claim Hgraphnet: functional_graph net0.
An exact proof term for the current goal is (functional_graph_graph J pickx).
We prove the intermediate claim Hdomnet: graph_domain_subset net0 J.
An exact proof term for the current goal is (graph_domain_subset_graph J pickx).
We use J to witness the existential quantifier.
We use le to witness the existential quantifier.
We use net0 to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HdirJ.
An exact proof term for the current goal is Htotnet.
An exact proof term for the current goal is Hgraphnet.
An exact proof term for the current goal is Hdomnet.
Let sub, K, leK, phi and x be given.
Assume Hw: subnet_of_witness net0 sub J le K leK X phi.
We will prove ¬ (net_converges_on X Tx sub K leK x).
Assume Hconv: net_converges_on X Tx sub K leK x.
We will prove False.
Apply Hw to the current goal.
Assume Hwcore Hvals.
Apply Hwcore to the current goal.
Assume Hwcore2 Hcofinal.
Apply Hwcore2 to the current goal.
Assume Hwcore3 Hmono.
Apply Hwcore3 to the current goal.
Assume Hwcore4 Hdomphi.
Apply Hwcore4 to the current goal.
Assume Hwcore5 Hgraphphi.
Apply Hwcore5 to the current goal.
Assume Hwcore6 Htotphi.
Apply Hwcore6 to the current goal.
Assume Hwcore7 Hdomsub.
Apply Hwcore7 to the current goal.
Assume Hwcore8 Hgraphsub.
Apply Hwcore8 to the current goal.
Assume Hwcore9 Htotsub.
Apply Hwcore9 to the current goal.
Assume Hwcore10 Hdomnet2.
Apply Hwcore10 to the current goal.
Assume Hwcore11 Hgraphnet2.
Apply Hwcore11 to the current goal.
Assume Hwcore12 Htotnet2.
Apply Hwcore12 to the current goal.
Assume HdirJ2 HdirK.
Apply Hconv to the current goal.
Assume HcCore HcTail.
Apply HcCore to the current goal.
Assume HcCore5 HxX.
Apply HcCore5 to the current goal.
Assume HcCore4 HdomC.
Apply HcCore4 to the current goal.
Assume HcCore3 HgraphC.
Apply HcCore3 to the current goal.
Assume HcCore2 HtotC.
Apply HcCore2 to the current goal.
Assume HTx2 HdirK2.
We prove the intermediate claim HcovX: X ⊆ ⋃ Fam.
An exact proof term for the current goal is (open_cover_of_covers X Tx Fam Hcover).
We prove the intermediate claim HxUnion: x ∈ ⋃ Fam.
An exact proof term for the current goal is (HcovX x HxX).
We prove the intermediate claim HexU: ∃U : set, x ∈ U ∧ U ∈ Fam.
An exact proof term for the current goal is (UnionE Fam x HxUnion).
Apply HexU to the current goal.
Let U be given.
Assume HU.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (andEL (x ∈ U) (U ∈ Fam) HU).
We prove the intermediate claim HUFam: U ∈ Fam.
An exact proof term for the current goal is (andER (x ∈ U) (U ∈ Fam) HU).
We prove the intermediate claim HUopen: U ∈ Tx.
An exact proof term for the current goal is (open_cover_of_members_open X Tx Fam U Hcover HUFam).
We prove the intermediate claim Hexk0: ∃k0 : set, k0 ∈ K ∧ ∀k : set, k ∈ K → (k0,k) ∈ leK → apply_fun sub k ∈ U.
An exact proof term for the current goal is (HcTail U HUopen HxU).
Apply Hexk0 to the current goal.
Let k0 be given.
Assume Hk0pack.
We prove the intermediate claim Hk0K: k0 ∈ K.
An exact proof term for the current goal is (andEL (k0 ∈ K) (∀k : set, k ∈ K → (k0,k) ∈ leK → apply_fun sub k ∈ U) Hk0pack).
We prove the intermediate claim HtailU: ∀k : set, k ∈ K → (k0,k) ∈ leK → apply_fun sub k ∈ U.
An exact proof term for the current goal is (andER (k0 ∈ K) (∀k : set, k ∈ K → (k0,k) ∈ leK → apply_fun sub k ∈ U) Hk0pack).
Set jU to be the term {U}.
We prove the intermediate claim HjUsub: jU ⊆ Fam.
Let V be given.
Assume HV: V ∈ jU.
We prove the intermediate claim HVeq: V = U.
An exact proof term for the current goal is (SingE U V HV).
rewrite the current goal using HVeq (from left to right).
An exact proof term for the current goal is HUFam.
We prove the intermediate claim HjUpow: jU ∈ 𝒫 Fam.
An exact proof term for the current goal is (PowerI Fam jU HjUsub).
We prove the intermediate claim HjUfin: finite jU.
An exact proof term for the current goal is (Sing_finite U).
We prove the intermediate claim HjUJ: jU ∈ J.
An exact proof term for the current goal is (SepI (𝒫 Fam) (λF0 : set ⇒ finite F0) jU HjUpow HjUfin).
We prove the intermediate claim HexkU: ∃kU : set, kU ∈ K ∧ (jU,apply_fun phi kU) ∈ le.
An exact proof term for the current goal is (Hcofinal jU HjUJ).
Apply HexkU to the current goal.
Let kU be given.
Assume HkUpack.
We prove the intermediate claim HkUK: kU ∈ K.
An exact proof term for the current goal is (andEL (kU ∈ K) ((jU,apply_fun phi kU) ∈ le) HkUpack).
We prove the intermediate claim HjUle: (jU,apply_fun phi kU) ∈ le.
An exact proof term for the current goal is (andER (kU ∈ K) ((jU,apply_fun phi kU) ∈ le) HkUpack).
We prove the intermediate claim Hexkstar: ∃kstar : set, kstar ∈ K ∧ (k0,kstar) ∈ leK ∧ (kU,kstar) ∈ leK.
Apply HdirK2 to the current goal.
Assume _ HdirUB.
An exact proof term for the current goal is (HdirUB k0 kU Hk0K HkUK).
Apply Hexkstar to the current goal.
Let kstar be given.
Assume Hkstarpack.
We prove the intermediate claim Hkstar12: kstar ∈ K ∧ (k0,kstar) ∈ leK.
An exact proof term for the current goal is (andEL (kstar ∈ K ∧ (k0,kstar) ∈ leK) ((kU,kstar) ∈ leK) Hkstarpack).
We prove the intermediate claim HkUle: (kU,kstar) ∈ leK.
An exact proof term for the current goal is (andER (kstar ∈ K ∧ (k0,kstar) ∈ leK) ((kU,kstar) ∈ leK) Hkstarpack).
We prove the intermediate claim HkstarK: kstar ∈ K.
An exact proof term for the current goal is (andEL (kstar ∈ K) ((k0,kstar) ∈ leK) Hkstar12).
We prove the intermediate claim Hk0le: (k0,kstar) ∈ leK.
An exact proof term for the current goal is (andER (kstar ∈ K) ((k0,kstar) ∈ leK) Hkstar12).
We prove the intermediate claim HsubU: apply_fun sub kstar ∈ U.
An exact proof term for the current goal is (HtailU kstar HkstarK Hk0le).
We prove the intermediate claim Hphi_kU_J: apply_fun phi kU ∈ J.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y phi K J kU Htotphi HkUK).
We prove the intermediate claim Hphi_kstar_J: apply_fun phi kstar ∈ J.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y phi K J kstar Htotphi HkstarK).
We prove the intermediate claim Hphimon: (apply_fun phi kU,apply_fun phi kstar) ∈ le.
An exact proof term for the current goal is (Hmono kU kstar HkUK HkstarK HkUle).
We prove the intermediate claim HjUle2: (jU,apply_fun phi kstar) ∈ le.
An exact proof term for the current goal is (directed_set_trans J le HdirJ jU (apply_fun phi kU) (apply_fun phi kstar) HjUJ Hphi_kU_J Hphi_kstar_J HjUle Hphimon).
We prove the intermediate claim HjUsubPhi: jU ⊆ apply_fun phi kstar.
An exact proof term for the current goal is (andER ((jU,apply_fun phi kstar) ∈ setprod J J) (jU ⊆ apply_fun phi kstar) (inclusion_relE J jU (apply_fun phi kstar) HjUle2)).
We prove the intermediate claim HUinPhi: U ∈ apply_fun phi kstar.
Apply (HjUsubPhi U) to the current goal.
An exact proof term for the current goal is (SingI U).
We prove the intermediate claim Hsubeq: apply_fun sub kstar = apply_fun net0 (apply_fun phi kstar).
An exact proof term for the current goal is (Hvals kstar HkstarK).
We prove the intermediate claim Hnet0eq: apply_fun net0 (apply_fun phi kstar) = pickx (apply_fun phi kstar).
rewrite the current goal using (apply_fun_graph J pickx (apply_fun phi kstar) Hphi_kstar_J) (from left to right).
Use reflexivity.
We prove the intermediate claim HsubisPick: apply_fun sub kstar = pickx (apply_fun phi kstar).
rewrite the current goal using Hsubeq (from left to right).
rewrite the current goal using Hnet0eq (from left to right).
Use reflexivity.
We prove the intermediate claim HpickU: pickx (apply_fun phi kstar) ∈ U.
rewrite the current goal using HsubisPick (from right to left) at position 1.
An exact proof term for the current goal is HsubU.
We prove the intermediate claim HspecStar: pickx (apply_fun phi kstar) ∈ X ∧ ¬ (pickx (apply_fun phi kstar) ∈ ⋃ (apply_fun phi kstar)).
An exact proof term for the current goal is (Hpick_spec (apply_fun phi kstar) Hphi_kstar_J).
We prove the intermediate claim HnotUnion: ¬ (pickx (apply_fun phi kstar) ∈ ⋃ (apply_fun phi kstar)).
An exact proof term for the current goal is (andER (pickx (apply_fun phi kstar) ∈ X) (¬ (pickx (apply_fun phi kstar) ∈ ⋃ (apply_fun phi kstar))) HspecStar).
We prove the intermediate claim HnotU: ¬ (pickx (apply_fun phi kstar) ∈ U).
Assume HmemU: pickx (apply_fun phi kstar) ∈ U.
Apply HnotUnion to the current goal.
An exact proof term for the current goal is (UnionI (apply_fun phi kstar) (pickx (apply_fun phi kstar)) U HmemU HUinPhi).
An exact proof term for the current goal is (HnotU HpickU).
∎