Let X, Tx, net, sub, x, J, leJ, K, leK and phi be given.
Assume Hw: subnet_of_witness net sub J leJ K leK X phi.
Assume Hconv: net_converges_on X Tx net J leJ x.
We will prove net_converges_on X Tx sub K leK x.
Apply Hconv to the current goal.
Assume Hcore Htail.
Apply Hcore to the current goal.
Assume Hcore5 HxX.
Apply Hcore5 to the current goal.
Assume Hcore4 Hdomnet.
Apply Hcore4 to the current goal.
Assume Hcore3 Hgraphnet.
Apply Hcore3 to the current goal.
Assume Hcore2 Htotnet.
Apply Hcore2 to the current goal.
Assume HTx HdirJ.
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.
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 ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ K ∧ ∀i : set, i ∈ K → (i0,i) ∈ leK → apply_fun sub i ∈ U.
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 Htotsub.
An exact proof term for the current goal is Hgraphsub.
An exact proof term for the current goal is Hdomsub.
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 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 (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 Htotnet Hgraphnet Hdomnet Htotsub Hgraphsub Hdomsub Htotphi Hgraphphi Hdomphi Hmono Hcofinal Hvals) 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 Htotphi 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 (Hvals k HkK) (from left to right).
An exact proof term for the current goal is (HafterJ (apply_fun phi k) HphikJ Hj0phik).
∎