Let net, sub, J, leJ, K, leK, X, phi, Y and f be given.
Assume Hw: subnet_of_witness net sub J leJ K leK X phi.
Assume Hf: function_on f X Y.
We will prove subnet_of_witness (compose_fun J net f) (compose_fun K sub f) J leJ K leK Y phi.
Apply Hw 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 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.
We prove the intermediate claim Hnetfun: 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 Hsubfun: function_on sub K X.
An exact proof term for the current goal is (total_function_on_function_on sub K X Htotsub).
We prove the intermediate claim Htotnet2: total_function_on (compose_fun J net f) J Y.
An exact proof term for the current goal is (total_function_on_compose_fun J X Y net f Hnetfun Hf).
We prove the intermediate claim Htotsub2: total_function_on (compose_fun K sub f) K Y.
An exact proof term for the current goal is (total_function_on_compose_fun K X Y sub f Hsubfun Hf).
We will prove directed_set J leJ ∧ directed_set K leK ∧ total_function_on (compose_fun J net f) J Y ∧ functional_graph (compose_fun J net f) ∧ graph_domain_subset (compose_fun J net f) J ∧ total_function_on (compose_fun K sub f) K Y ∧ functional_graph (compose_fun K sub f) ∧ graph_domain_subset (compose_fun K sub f) 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 (compose_fun K sub f) k = apply_fun (compose_fun J net f) (apply_fun phi k)).
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI 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 Htotnet2.
An exact proof term for the current goal is (functional_graph_compose_fun J net f).
An exact proof term for the current goal is (graph_domain_subset_compose_fun J net f).
An exact proof term for the current goal is Htotsub2.
An exact proof term for the current goal is (functional_graph_compose_fun K sub f).
An exact proof term for the current goal is (graph_domain_subset_compose_fun K sub f).
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.
Let k be given.
Assume HkK: k ∈ K.
We prove the intermediate claim Hsubk: apply_fun sub k = apply_fun net (apply_fun phi k).
An exact proof term for the current goal is (Hvals k HkK).
We prove the intermediate claim Happ1: apply_fun (compose_fun K sub f) k = apply_fun f (apply_fun sub k).
An exact proof term for the current goal is (compose_fun_apply K sub f k HkK).
We prove the intermediate claim Hphik: 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 Happ2: apply_fun (compose_fun J net f) (apply_fun phi k) = apply_fun f (apply_fun net (apply_fun phi k)).
An exact proof term for the current goal is (compose_fun_apply J net f (apply_fun phi k) Hphik).
rewrite the current goal using Happ1 (from left to right).
rewrite the current goal using Happ2 (from left to right).
rewrite the current goal using Hsubk (from left to right).
Use reflexivity.
∎