Let net, J, leJ, K, leK, X and phi be given.
Assume HdirJ: directed_set J leJ.
Assume HdirK: directed_set K leK.
Assume Htotnet: total_function_on net J X.
Assume Hgraphnet: functional_graph net.
Assume Hdomnet: graph_domain_subset net J.
Assume Htotphi: total_function_on phi K J.
Assume Hgraphphi: functional_graph phi.
Assume Hdomphi: 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.
Set sub to be the term compose_fun K phi net.
We will prove subnet_of_witness net sub J leJ K leK X phi.
We prove the intermediate claim Hfunphi: function_on phi K J.
An exact proof term for the current goal is (total_function_on_function_on phi K J Htotphi).
We prove the intermediate claim Hfunnet: function_on net J X.
An exact proof term for the current goal is (total_function_on_function_on net J X Htotnet).
We prove the intermediate claim Htotsub: total_function_on sub K X.
An exact proof term for the current goal is (total_function_on_compose_fun K J X phi net Hfunphi Hfunnet).
We prove the intermediate claim Hgraphsub: functional_graph sub.
An exact proof term for the current goal is (functional_graph_compose_fun K phi net).
We prove the intermediate claim Hdomsub: graph_domain_subset sub K.
An exact proof term for the current goal is (graph_domain_subset_compose_fun K phi net).
We prove the intermediate claim Hvals: ∀k : set, k ∈ K → apply_fun sub k = apply_fun net (apply_fun phi k).
Let k be given.
Assume HkK: k ∈ K.
We prove the intermediate claim Hsubdef: sub = graph K (λk0 : set ⇒ apply_fun net (apply_fun phi k0)).
Use reflexivity.
rewrite the current goal using Hsubdef (from left to right).
rewrite the current goal using (apply_fun_graph K (λk0 : set ⇒ apply_fun net (apply_fun phi k0)) k HkK) (from left to right).
Use reflexivity.
Apply (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))) to the current goal.
An exact proof term for the current goal is HdirJ.
An exact proof term for the current goal is HdirK.
An exact proof term for the current goal is Htotnet.
An exact proof term for the current goal is Hgraphnet.
An exact proof term for the current goal is Hdomnet.
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 Htotphi.
An exact proof term for the current goal is Hgraphphi.
An exact proof term for the current goal is Hdomphi.
An exact proof term for the current goal is Hmono.
An exact proof term for the current goal is Hcofinal.
An exact proof term for the current goal is Hvals.
∎