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 ∃N : set, net_pack_in_space X N ∧ (∀S x : set, subnet_pack_of_in X N S → ¬ (net_pack_converges X Tx S x)).
Apply (open_cover_no_finite_subcover_implies_net_counterexample X Tx Fam HTx Hcover Hnofin) to the current goal.
Let J be given.
Assume Hex1.
Apply Hex1 to the current goal.
Let le be given.
Assume Hex2.
Apply Hex2 to the current goal.
Let net0 be given.
Assume Hdata.
We use (net_pack J le net0) to witness the existential quantifier.
Apply andI to the current goal.
We will prove net_pack_in_space X (net_pack J le net0).
We will prove ∃J0 le0 net1 : set, net_pack J le net0 = net_pack J0 le0 net1 ∧ directed_set J0 le0 ∧ total_function_on net1 J0 X ∧ functional_graph net1 ∧ graph_domain_subset net1 J0.
We use J to witness the existential quantifier.
We use le to witness the existential quantifier.
We use net0 to witness the existential quantifier.
We prove the intermediate claim Hleft: (((directed_set J le ∧ total_function_on net0 J X) ∧ functional_graph net0) ∧ graph_domain_subset net0 J).
An exact proof term for the current goal is (andEL (((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)) Hdata).
We prove the intermediate claim Htmp: (directed_set J le ∧ total_function_on net0 J X) ∧ functional_graph net0.
An exact proof term for the current goal is (andEL ((directed_set J le ∧ total_function_on net0 J X) ∧ functional_graph net0) (graph_domain_subset net0 J) Hleft).
We prove the intermediate claim HdirTot: directed_set J le ∧ total_function_on net0 J X.
An exact proof term for the current goal is (andEL (directed_set J le ∧ total_function_on net0 J X) (functional_graph net0) Htmp).
We prove the intermediate claim HdirJ: directed_set J le.
An exact proof term for the current goal is (andEL (directed_set J le) (total_function_on net0 J X) HdirTot).
We prove the intermediate claim Htot: total_function_on net0 J X.
An exact proof term for the current goal is (andER (directed_set J le) (total_function_on net0 J X) HdirTot).
We prove the intermediate claim Hgraph: functional_graph net0.
An exact proof term for the current goal is (andER (directed_set J le ∧ total_function_on net0 J X) (functional_graph net0) Htmp).
We prove the intermediate claim Hdom: graph_domain_subset net0 J.
An exact proof term for the current goal is (andER ((directed_set J le ∧ total_function_on net0 J X) ∧ functional_graph net0) (graph_domain_subset net0 J) Hleft).
Apply and5I to the current goal.
Use reflexivity.
An exact proof term for the current goal is HdirJ.
An exact proof term for the current goal is Htot.
An exact proof term for the current goal is Hgraph.
An exact proof term for the current goal is Hdom.
Let S and x be given.
Assume Hsub: subnet_pack_of_in X (net_pack J le net0) S.
We will prove ¬ (net_pack_converges X Tx S x).
Assume Hconv: net_pack_converges X Tx S x.
Apply Hconv to the current goal.
Let K be given.
Assume HexK.
Apply HexK to the current goal.
Let leK be given.
Assume HexleK.
Apply HexleK to the current goal.
Let sub be given.
Assume Hpair: S = net_pack K leK sub ∧ net_converges_on X Tx sub K leK x.
We prove the intermediate claim HS: S = net_pack K leK sub.
An exact proof term for the current goal is (andEL (S = net_pack K leK sub) (net_converges_on X Tx sub K leK x) Hpair).
We prove the intermediate claim Hsubconv: net_converges_on X Tx sub K leK x.
An exact proof term for the current goal is (andER (S = net_pack K leK sub) (net_converges_on X Tx sub K leK x) Hpair).
We prove the intermediate claim HindexS: net_pack_index S = K.
rewrite the current goal using HS (from left to right).
An exact proof term for the current goal is (net_pack_index_eq K leK sub).
We prove the intermediate claim HleS: net_pack_le S = leK.
rewrite the current goal using HS (from left to right).
An exact proof term for the current goal is (net_pack_le_eq K leK sub).
We prove the intermediate claim HfunS: net_pack_fun S = sub.
rewrite the current goal using HS (from left to right).
An exact proof term for the current goal is (net_pack_fun_eq K leK sub).
Apply Hsub to the current goal.
Let phi be given.
Assume HphiRaw: subnet_of_witness (net_pack_fun (net_pack J le net0)) (net_pack_fun S) (net_pack_index (net_pack J le net0)) (net_pack_le (net_pack J le net0)) (net_pack_index S) (net_pack_le S) X phi.
We prove the intermediate claim Hno: ∀sub0 K0 leK0 phi0 x0 : set, subnet_of_witness net0 sub0 J le K0 leK0 X phi0 → ¬ (net_converges_on X Tx sub0 K0 leK0 x0).
An exact proof term for the current goal is (andER (((directed_set J le ∧ total_function_on net0 J X) ∧ functional_graph net0) ∧ graph_domain_subset net0 J) (∀sub0 K0 leK0 phi0 x0 : set, subnet_of_witness net0 sub0 J le K0 leK0 X phi0 → ¬ (net_converges_on X Tx sub0 K0 leK0 x0)) Hdata).
We prove the intermediate claim Hphi: subnet_of_witness net0 sub J le K leK X phi.
An exact proof term for the current goal is (subnet_of_witness_congr (net_pack_fun (net_pack J le net0)) net0 (net_pack_fun S) sub (net_pack_index (net_pack J le net0)) J (net_pack_le (net_pack J le net0)) le (net_pack_index S) K (net_pack_le S) leK X phi (net_pack_fun_eq J le net0) HfunS (net_pack_index_eq J le net0) (net_pack_le_eq J le net0) HindexS HleS HphiRaw).
An exact proof term for the current goal is ((Hno sub K leK phi x Hphi) Hsubconv).
∎