Let X, Tx, net and x be given.
Assume H: net_converges X Tx net x.
We will prove net_on net.
Apply H to the current goal.
Let J be given.
Assume HJ: ∃le : set, topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ U.
Apply HJ to the current goal.
Let le be given.
Assume Hdata: topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J ∧ x ∈ X ∧ ∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ U.
We will prove net_on net.
We will prove ∃J0 le0 X0 : set, directed_set J0 le0 ∧ total_function_on net J0 X0 ∧ functional_graph net ∧ graph_domain_subset net J0.
We use J to witness the existential quantifier.
We use le to witness the existential quantifier.
We use X to witness the existential quantifier.
We prove the intermediate claim Hcore: topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J ∧ x ∈ X.
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J ∧ x ∈ X) (∀U : set, U ∈ Tx → x ∈ U → ∃i0 : set, i0 ∈ J ∧ ∀i : set, i ∈ J → (i0,i) ∈ le → apply_fun net i ∈ U) Hdata).
We prove the intermediate claim Hcore5: topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J.
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J) (x ∈ X) Hcore).
We prove the intermediate claim Hcore4: topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net.
An exact proof term for the current goal is (andEL (topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net) (graph_domain_subset net J) Hcore5).
We prove the intermediate claim Hdir: directed_set J le.
An exact proof term for the current goal is (andER (topology_on X Tx) (directed_set J le) (andEL (topology_on X Tx ∧ directed_set J le) (total_function_on net J X) (andEL (topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X) (functional_graph net) Hcore4))).
We prove the intermediate claim Htot: total_function_on net J X.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ directed_set J le) (total_function_on net J X) (andEL (topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X) (functional_graph net) Hcore4)).
We prove the intermediate claim Hgraph: functional_graph net.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X) (functional_graph net) Hcore4).
We prove the intermediate claim Hdom: graph_domain_subset net J.
An exact proof term for the current goal is (andER (topology_on X Tx ∧ directed_set J le ∧ total_function_on net J X ∧ functional_graph net) (graph_domain_subset net J) Hcore5).
Apply and4I to the current goal.
An exact proof term for the current goal is Hdir.
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.
∎