Let net and sub be given.
Assume H: subnet_of net sub.
We will prove ∃J leJ K leK X phi : set, subnet_of_witness net sub J leJ K leK X phi.
Apply H to the current goal.
Let J be given.
Assume HJ: ∃leJ K leK X phi : set, 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)).
Apply HJ to the current goal.
Let leJ be given.
Assume HJ2: ∃K leK X phi : set, 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)).
Apply HJ2 to the current goal.
Let K be given.
Assume HK: ∃leK X phi : set, 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)).
Apply HK to the current goal.
Let leK be given.
Assume HK2: ∃X phi : set, 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)).
Apply HK2 to the current goal.
Let X be given.
Assume HX: ∃phi : set, 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)).
Apply HX to the current goal.
Let phi be given.
Assume Hcore: 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)).
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 Hcore to the current goal.
Assume Hcore13 Hvals.
Apply Hcore13 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 Hdomsub.
Apply Hcore9 to the current goal.
Assume Hcore8 Hdomnet.
Apply Hcore8 to the current goal.
Assume Hcore7 Hgraphphi.
Apply Hcore7 to the current goal.
Assume Hcore6 Htotphi.
Apply Hcore6 to the current goal.
Assume Hcore5 Hgraphsub.
Apply Hcore5 to the current goal.
Assume Hcore4 Htotsub.
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) (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).
∎