Let net, sub, sub2, J, leJ, K, leK, L, leL, X, phi and psi be given.
Assume H1: subnet_of_witness net sub J leJ K leK X phi.
Assume H2: subnet_of_witness sub sub2 K leK L leL X psi.
We will prove subnet_of_witness net sub2 J leJ L leL X (compose_fun L psi phi).
Apply H1 to the current goal.
Assume H1core13 H1vals.
Apply H1core13 to the current goal.
Assume H1core12 H1cofinal.
Apply H1core12 to the current goal.
Assume H1core11 H1mono.
Apply H1core11 to the current goal.
Assume H1core10 H1domphi.
Apply H1core10 to the current goal.
Assume H1core9 H1graphphi.
Apply H1core9 to the current goal.
Assume H1core8 H1totphi.
Apply H1core8 to the current goal.
Assume H1core7 H1domsub.
Apply H1core7 to the current goal.
Assume H1core6 H1graphsub.
Apply H1core6 to the current goal.
Assume H1core5 H1totsub.
Apply H1core5 to the current goal.
Assume H1core4 H1domnet.
Apply H1core4 to the current goal.
Assume H1core3 H1graphnet.
Apply H1core3 to the current goal.
Assume H1core2 H1totnet.
Apply H1core2 to the current goal.
Assume HdirJ HdirK.
Apply H2 to the current goal.
Assume H2core13 H2vals.
Apply H2core13 to the current goal.
Assume H2core12 H2cofinal.
Apply H2core12 to the current goal.
Assume H2core11 H2mono.
Apply H2core11 to the current goal.
Assume H2core10 H2dompsi.
Apply H2core10 to the current goal.
Assume H2core9 H2graphpsi.
Apply H2core9 to the current goal.
Assume H2core8 H2totpsi.
Apply H2core8 to the current goal.
Assume H2core7 H2domsub2.
Apply H2core7 to the current goal.
Assume H2core6 H2graphsub2.
Apply H2core6 to the current goal.
Assume H2core5 H2totsub2.
Apply H2core5 to the current goal.
Assume H2core4 H2domsub.
Apply H2core4 to the current goal.
Assume H2core3 H2graphsub.
Apply H2core3 to the current goal.
Assume H2core2 H2totsub.
Apply H2core2 to the current goal.
Assume HdirK2 HdirL.
We prove the intermediate claim Hphifun: function_on phi K J.
An exact proof term for the current goal is (total_function_on_function_on phi K J H1totphi).
We prove the intermediate claim Hpsifun: function_on psi L K.
An exact proof term for the current goal is (total_function_on_function_on psi L K H2totpsi).
We prove the intermediate claim HcompTot: total_function_on (compose_fun L psi phi) L J.
An exact proof term for the current goal is (total_function_on_compose_fun L K J psi phi Hpsifun Hphifun).
We prove the intermediate claim HmonoComp: ∀i j : set, i ∈ L → j ∈ L → (i,j) ∈ leL → (apply_fun (compose_fun L psi phi) i,apply_fun (compose_fun L psi phi) j) ∈ leJ.
Let i and j be given.
Assume HiL: i ∈ L.
Assume HjL: j ∈ L.
Assume Hij: (i,j) ∈ leL.
We prove the intermediate claim Hpsiij: (apply_fun psi i,apply_fun psi j) ∈ leK.
An exact proof term for the current goal is (H2mono i j HiL HjL Hij).
We prove the intermediate claim HpsiiK: apply_fun psi i ∈ K.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y psi L K i H2totpsi HiL).
We prove the intermediate claim HpsijK: apply_fun psi j ∈ K.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y psi L K j H2totpsi HjL).
We prove the intermediate claim Hphiij: (apply_fun phi (apply_fun psi i),apply_fun phi (apply_fun psi j)) ∈ leJ.
An exact proof term for the current goal is (H1mono (apply_fun psi i) (apply_fun psi j) HpsiiK HpsijK Hpsiij).
We prove the intermediate claim Hci: apply_fun (compose_fun L psi phi) i = apply_fun phi (apply_fun psi i).
An exact proof term for the current goal is (compose_fun_apply L psi phi i HiL).
We prove the intermediate claim Hcj: apply_fun (compose_fun L psi phi) j = apply_fun phi (apply_fun psi j).
An exact proof term for the current goal is (compose_fun_apply L psi phi j HjL).
rewrite the current goal using Hci (from left to right).
rewrite the current goal using Hcj (from left to right).
An exact proof term for the current goal is Hphiij.
We prove the intermediate claim HcofinalComp: ∀j : set, j ∈ J → ∃l : set, l ∈ L ∧ (j,apply_fun (compose_fun L psi phi) l) ∈ leJ.
Let j be given.
Assume HjJ: j ∈ J.
We prove the intermediate claim Hexk: ∃k : set, k ∈ K ∧ (j,apply_fun phi k) ∈ leJ.
An exact proof term for the current goal is (H1cofinal j HjJ).
Apply Hexk to the current goal.
Let k be given.
Assume Hkpack.
We prove the intermediate claim HkK: k ∈ K.
An exact proof term for the current goal is (andEL (k ∈ K) ((j,apply_fun phi k) ∈ leJ) Hkpack).
We prove the intermediate claim HjphiK: (j,apply_fun phi k) ∈ leJ.
An exact proof term for the current goal is (andER (k ∈ K) ((j,apply_fun phi k) ∈ leJ) Hkpack).
We prove the intermediate claim Hexl: ∃l : set, l ∈ L ∧ (k,apply_fun psi l) ∈ leK.
An exact proof term for the current goal is (H2cofinal k HkK).
Apply Hexl to the current goal.
Let l be given.
Assume Hlpack.
We use l to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (l ∈ L) ((k,apply_fun psi l) ∈ leK) Hlpack).
We prove the intermediate claim HlL: l ∈ L.
An exact proof term for the current goal is (andEL (l ∈ L) ((k,apply_fun psi l) ∈ leK) Hlpack).
We prove the intermediate claim Hkpsil: (k,apply_fun psi l) ∈ leK.
An exact proof term for the current goal is (andER (l ∈ L) ((k,apply_fun psi l) ∈ leK) Hlpack).
We prove the intermediate claim HpsilK: apply_fun psi l ∈ K.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y psi L K l H2totpsi HlL).
We prove the intermediate claim HphikJ: 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 H1totphi HkK).
We prove the intermediate claim HphipsilJ: apply_fun phi (apply_fun psi l) ∈ J.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y phi K J (apply_fun psi l) H1totphi HpsilK).
We prove the intermediate claim HphiAbove: (apply_fun phi k,apply_fun phi (apply_fun psi l)) ∈ leJ.
An exact proof term for the current goal is (H1mono k (apply_fun psi l) HkK HpsilK Hkpsil).
We prove the intermediate claim Hcl: apply_fun (compose_fun L psi phi) l = apply_fun phi (apply_fun psi l).
An exact proof term for the current goal is (compose_fun_apply L psi phi l HlL).
rewrite the current goal using Hcl (from left to right).
An exact proof term for the current goal is (directed_set_trans J leJ HdirJ j (apply_fun phi k) (apply_fun phi (apply_fun psi l)) HjJ HphikJ HphipsilJ HjphiK HphiAbove).
We will prove directed_set J leJ ∧ directed_set L leL ∧ total_function_on net J X ∧ functional_graph net ∧ graph_domain_subset net J ∧ total_function_on sub2 L X ∧ functional_graph sub2 ∧ graph_domain_subset sub2 L ∧ total_function_on (compose_fun L psi phi) L J ∧ functional_graph (compose_fun L psi phi) ∧ graph_domain_subset (compose_fun L psi phi) L ∧ (∀i j : set, i ∈ L → j ∈ L → (i,j) ∈ leL → (apply_fun (compose_fun L psi phi) i,apply_fun (compose_fun L psi phi) j) ∈ leJ) ∧ (∀j : set, j ∈ J → ∃l : set, l ∈ L ∧ (j,apply_fun (compose_fun L psi phi) l) ∈ leJ) ∧ (∀l : set, l ∈ L → apply_fun sub2 l = apply_fun net (apply_fun (compose_fun L psi phi) l)).
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 HdirL.
An exact proof term for the current goal is H1totnet.
An exact proof term for the current goal is H1graphnet.
An exact proof term for the current goal is H1domnet.
An exact proof term for the current goal is H2totsub2.
An exact proof term for the current goal is H2graphsub2.
An exact proof term for the current goal is H2domsub2.
An exact proof term for the current goal is HcompTot.
An exact proof term for the current goal is (functional_graph_compose_fun L psi phi).
An exact proof term for the current goal is (graph_domain_subset_compose_fun L psi phi).
An exact proof term for the current goal is HmonoComp.
An exact proof term for the current goal is HcofinalComp.
Let l be given.
Assume HlL: l ∈ L.
We prove the intermediate claim Hsub2l: apply_fun sub2 l = apply_fun sub (apply_fun psi l).
An exact proof term for the current goal is (H2vals l HlL).
We prove the intermediate claim HpsilK: apply_fun psi l ∈ K.
An exact proof term for the current goal is (total_function_on_apply_fun_in_Y psi L K l H2totpsi HlL).
We prove the intermediate claim Hsubl: apply_fun sub (apply_fun psi l) = apply_fun net (apply_fun phi (apply_fun psi l)).
An exact proof term for the current goal is (H1vals (apply_fun psi l) HpsilK).
We prove the intermediate claim Hcl: apply_fun (compose_fun L psi phi) l = apply_fun phi (apply_fun psi l).
An exact proof term for the current goal is (compose_fun_apply L psi phi l HlL).
rewrite the current goal using Hsub2l (from left to right).
rewrite the current goal using Hsubl (from left to right).
rewrite the current goal using Hcl (from right to left).
Use reflexivity.
∎