Let net, sub, J, leJ, K, leK, X and phi be given.
Assume H: subnet_of_witness net sub J leJ K leK X phi.
We will prove subnet_of net sub.
We will prove ∃J0 leJ0 K0 leK0 X0 phi0 : set, directed_set J0 leJ0 ∧ directed_set K0 leK0 ∧ total_function_on net J0 X0 ∧ functional_graph net ∧ total_function_on sub K0 X0 ∧ functional_graph sub ∧ total_function_on phi0 K0 J0 ∧ functional_graph phi0 ∧ graph_domain_subset net J0 ∧ graph_domain_subset sub K0 ∧ graph_domain_subset phi0 K0 ∧ (∀i j : set, i ∈ K0 → j ∈ K0 → (i,j) ∈ leK0 → (apply_fun phi0 i,apply_fun phi0 j) ∈ leJ0) ∧ (∀j : set, j ∈ J0 → ∃k : set, k ∈ K0 ∧ (j,apply_fun phi0 k) ∈ leJ0) ∧ (∀k : set, k ∈ K0 → apply_fun sub k = apply_fun net (apply_fun phi0 k)).
We use J to witness the existential quantifier.
We use leJ to witness the existential quantifier.
We use K to witness the existential quantifier.
We use leK to witness the existential quantifier.
We use X to witness the existential quantifier.
We use phi to witness the existential quantifier.
Apply H to the current goal.
Assume Hcore Hvals.
Apply Hcore to the current goal.
Assume Hcore12 Hcofinal.
Apply Hcore12 to the current goal.
Assume Hcore11 Hmono.
Apply Hcore11 to the current goal.
Assume Hcore10 Hdomphi.
Apply Hcore10 to the current goal.
Assume Hcore9 Hgraphphi.
Apply Hcore9 to the current goal.
Assume Hcore8 Htotphi.
Apply Hcore8 to the current goal.
Assume Hcore7 Hdomsub.
Apply Hcore7 to the current goal.
Assume Hcore6 Hgraphsub.
Apply Hcore6 to the current goal.
Assume Hcore5 Htotsub.
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 HdirJ HdirK.
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) (total_function_on sub K X) (functional_graph sub) (total_function_on phi K J) (functional_graph phi) (graph_domain_subset net J) (graph_domain_subset sub K) (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 Htotsub Hgraphsub Htotphi Hgraphphi Hdomnet Hdomsub Hdomphi Hmono Hcofinal Hvals).
∎