Let X, Tx, net, sub, x, J, leJ, K, leK and phi be given.
Assume HTx: topology_on X Tx.
Assume HdirJ: directed_set J leJ.
Assume HdirK: directed_set K leK.
Assume Hnettot: total_function_on net J X.
Assume Hnetgraph: functional_graph net.
Assume Hnetdom: graph_domain_subset net J.
Assume Hsubtot: total_function_on sub K X.
Assume Hsubgraph: functional_graph sub.
Assume Hsubdom: graph_domain_subset sub K.
Assume Hphitot: total_function_on phi K J.
Assume Hphigraph: functional_graph phi.
Assume Hphidom: graph_domain_subset phi K.
Assume Hmono: ∀i j : set, i ∈ K → j ∈ K → (i,j) ∈ leK → (apply_fun phi i,apply_fun phi j) ∈ leJ.
Assume Hcofinal: ∀j : set, j ∈ J → ∃k : set, k ∈ K ∧ (j,apply_fun phi k) ∈ leJ.
Assume Hsubeq: ∀k : set, k ∈ K → apply_fun sub k = apply_fun net (apply_fun phi k).
Assume HxX: x ∈ X.
Assume Htail: ∀U : set, U ∈ Tx → x ∈ U → ∃j0 : set, j0 ∈ J ∧ ∀j : set, j ∈ J → (j0,j) ∈ leJ → apply_fun net j ∈ U.
We will prove net_converges X Tx sub x.
We will prove ∃J0 le0 : set, topology_on X Tx ∧ directed_set J0 le0 ∧ total_function_on sub J0 X ∧ functional_graph sub ∧ graph_domain_subset sub J0 ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ J0 ∧ ∀i : set, i ∈ J0 → (i0,i) ∈ le0 → apply_fun sub i ∈ U.
We use K to witness the existential quantifier.
We use leK to witness the existential quantifier.
Apply andI to the current goal.
We will prove topology_on X Tx ∧ directed_set K leK ∧ total_function_on sub K X ∧ functional_graph sub ∧ graph_domain_subset sub K ∧ x ∈ X.
Apply and6I to the current goal.
An exact proof term for the current goal is HTx.
An exact proof term for the current goal is HdirK.
An exact proof term for the current goal is Hsubtot.
An exact proof term for the current goal is Hsubgraph.
An exact proof term for the current goal is Hsubdom.
An exact proof term for the current goal is HxX.
Let U be given.
Assume HU: U ∈ Tx.
Assume HxU: x ∈ U.
We prove the intermediate claim Hexj0: ∃j0 : set, j0 ∈ J ∧ ∀j : set, j ∈ J → (j0,j) ∈ leJ → apply_fun net j ∈ U.
An exact proof term for the current goal is (Htail U HU HxU).
Apply Hexj0 to the current goal.
Let j0 be given.
Assume Hj0pair.
Apply Hj0pair to the current goal.
Assume Hj0J HafterJ.
We prove the intermediate claim Hwsub: subnet_of_witness net sub J leJ K leK X phi.
An exact proof term for the current goal is (and14I (directed_set J leJ) (directed_set K leK) (total_function_on net J X) (functional_graph net) (graph_domain_subset net J) (total_function_on sub K X) (functional_graph sub) (graph_domain_subset sub K) (total_function_on phi K J) (functional_graph phi) (graph_domain_subset phi K) (∀i j : set, i ∈ K → j ∈ K → (i,j) ∈ leK → (apply_fun phi i,apply_fun phi j) ∈ leJ) (∀j : set, j ∈ J → ∃k : set, k ∈ K ∧ (j,apply_fun phi k) ∈ leJ) (∀k : set, k ∈ K → apply_fun sub k = apply_fun net (apply_fun phi k)) HdirJ HdirK Hnettot Hnetgraph Hnetdom Hsubtot Hsubgraph Hsubdom Hphitot Hphigraph Hphidom Hmono Hcofinal Hsubeq).
We prove the intermediate claim Hexk0: ∃k0 : set, k0 ∈ K ∧ ∀k : set, k ∈ K → (k0,k) ∈ leK → (j0,apply_fun phi k) ∈ leJ.
An exact proof term for the current goal is (subnet_of_witness_tail_above net sub J leJ K leK X phi j0 Hwsub Hj0J).
Apply Hexk0 to the current goal.
Let k0 be given.
Assume Hk0pack.
We use k0 to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (k0 ∈ K) (∀k : set, k ∈ K → (k0,k) ∈ leK → (j0,apply_fun phi k) ∈ leJ) Hk0pack).
Let k be given.
Assume HkK: k ∈ K.
Assume Hk0k: (k0,k) ∈ leK.
We will prove apply_fun sub k ∈ U.
We prove the intermediate claim HphikJ: apply_fun phi k ∈ J.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y phi K J k Hphitot HkK).
We prove the intermediate claim Hj0phik: (j0,apply_fun phi k) ∈ leJ.
We prove the intermediate claim HtailAbove: ∀k1 : set, k1 ∈ K → (k0,k1) ∈ leK → (j0,apply_fun phi k1) ∈ leJ.
An exact proof term for the current goal is (andER (k0 ∈ K) (∀k1 : set, k1 ∈ K → (k0,k1) ∈ leK → (j0,apply_fun phi k1) ∈ leJ) Hk0pack).
An exact proof term for the current goal is (HtailAbove k HkK Hk0k).
rewrite the current goal using (Hsubeq k HkK) (from left to right).
An exact proof term for the current goal is (HafterJ (apply_fun phi k) HphikJ Hj0phik).
∎