Metamath Proof Explorer

Theorem isomgrtrlem

Description: Lemma for isomgrtr . (Contributed by AV, 5-Dec-2022)

Ref Expression
Assertion isomgrtrlem ⊢A∈UHGraph∧B∈UHGraph∧C∈X∧f:Vtx⁡A⟶1-1 ontoVtx⁡B∧v:Vtx⁡B⟶1-1 ontoVtx⁡C∧g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i∧w:dom⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡C∧∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k→∀j∈dom⁡iEdg⁡Av∘fiEdg⁡A⁡j=iEdg⁡C⁡w∘g⁡j

Proof

Step Hyp Ref Expression
1 imaco ⊢v∘fiEdg⁡A⁡j=vfiEdg⁡A⁡j
2 1 a1i ⊢A∈UHGraph∧B∈UHGraph∧C∈X∧f:Vtx⁡A⟶1-1 ontoVtx⁡B∧v:Vtx⁡B⟶1-1 ontoVtx⁡C∧g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i∧w:dom⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡C∧∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k∧j∈dom⁡iEdg⁡A→v∘fiEdg⁡A⁡j=vfiEdg⁡A⁡j
3 fveq2 ⊢i=j→iEdg⁡A⁡i=iEdg⁡A⁡j
4 3 imaeq2d ⊢i=j→fiEdg⁡A⁡i=fiEdg⁡A⁡j
5 2fveq3 ⊢i=j→iEdg⁡B⁡g⁡i=iEdg⁡B⁡g⁡j
6 4 5 eqeq12d ⊢i=j→fiEdg⁡A⁡i=iEdg⁡B⁡g⁡i↔fiEdg⁡A⁡j=iEdg⁡B⁡g⁡j
7 6 rspccv ⊢∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i→j∈dom⁡iEdg⁡A→fiEdg⁡A⁡j=iEdg⁡B⁡g⁡j
8 7 adantl ⊢g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i→j∈dom⁡iEdg⁡A→fiEdg⁡A⁡j=iEdg⁡B⁡g⁡j
9 8 ad2antlr ⊢A∈UHGraph∧B∈UHGraph∧C∈X∧f:Vtx⁡A⟶1-1 ontoVtx⁡B∧v:Vtx⁡B⟶1-1 ontoVtx⁡C∧g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i∧w:dom⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡C∧∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k→j∈dom⁡iEdg⁡A→fiEdg⁡A⁡j=iEdg⁡B⁡g⁡j
10 9 imp ⊢A∈UHGraph∧B∈UHGraph∧C∈X∧f:Vtx⁡A⟶1-1 ontoVtx⁡B∧v:Vtx⁡B⟶1-1 ontoVtx⁡C∧g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i∧w:dom⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡C∧∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k∧j∈dom⁡iEdg⁡A→fiEdg⁡A⁡j=iEdg⁡B⁡g⁡j
11 10 imaeq2d ⊢A∈UHGraph∧B∈UHGraph∧C∈X∧f:Vtx⁡A⟶1-1 ontoVtx⁡B∧v:Vtx⁡B⟶1-1 ontoVtx⁡C∧g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i∧w:dom⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡C∧∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k∧j∈dom⁡iEdg⁡A→vfiEdg⁡A⁡j=viEdg⁡B⁡g⁡j
12 simplrr ⊢A∈UHGraph∧B∈UHGraph∧C∈X∧f:Vtx⁡A⟶1-1 ontoVtx⁡B∧v:Vtx⁡B⟶1-1 ontoVtx⁡C∧g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i∧w:dom⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡C∧∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k∧j∈dom⁡iEdg⁡A→∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k
13 f1of ⊢g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B→g:dom⁡iEdg⁡A⟶dom⁡iEdg⁡B
14 ffvelcdm ⊢g:dom⁡iEdg⁡A⟶dom⁡iEdg⁡B∧j∈dom⁡iEdg⁡A→g⁡j∈dom⁡iEdg⁡B
15 14 ex ⊢g:dom⁡iEdg⁡A⟶dom⁡iEdg⁡B→j∈dom⁡iEdg⁡A→g⁡j∈dom⁡iEdg⁡B
16 13 15 syl ⊢g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B→j∈dom⁡iEdg⁡A→g⁡j∈dom⁡iEdg⁡B
17 16 adantr ⊢g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i→j∈dom⁡iEdg⁡A→g⁡j∈dom⁡iEdg⁡B
18 17 ad2antlr ⊢A∈UHGraph∧B∈UHGraph∧C∈X∧f:Vtx⁡A⟶1-1 ontoVtx⁡B∧v:Vtx⁡B⟶1-1 ontoVtx⁡C∧g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i∧w:dom⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡C∧∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k→j∈dom⁡iEdg⁡A→g⁡j∈dom⁡iEdg⁡B
19 18 imp ⊢A∈UHGraph∧B∈UHGraph∧C∈X∧f:Vtx⁡A⟶1-1 ontoVtx⁡B∧v:Vtx⁡B⟶1-1 ontoVtx⁡C∧g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i∧w:dom⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡C∧∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k∧j∈dom⁡iEdg⁡A→g⁡j∈dom⁡iEdg⁡B
20 fveq2 ⊢k=g⁡j→iEdg⁡B⁡k=iEdg⁡B⁡g⁡j
21 20 imaeq2d ⊢k=g⁡j→viEdg⁡B⁡k=viEdg⁡B⁡g⁡j
22 2fveq3 ⊢k=g⁡j→iEdg⁡C⁡w⁡k=iEdg⁡C⁡w⁡g⁡j
23 21 22 eqeq12d ⊢k=g⁡j→viEdg⁡B⁡k=iEdg⁡C⁡w⁡k↔viEdg⁡B⁡g⁡j=iEdg⁡C⁡w⁡g⁡j
24 23 rspccv ⊢∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k→g⁡j∈dom⁡iEdg⁡B→viEdg⁡B⁡g⁡j=iEdg⁡C⁡w⁡g⁡j
25 12 19 24 sylc ⊢A∈UHGraph∧B∈UHGraph∧C∈X∧f:Vtx⁡A⟶1-1 ontoVtx⁡B∧v:Vtx⁡B⟶1-1 ontoVtx⁡C∧g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i∧w:dom⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡C∧∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k∧j∈dom⁡iEdg⁡A→viEdg⁡B⁡g⁡j=iEdg⁡C⁡w⁡g⁡j
26 11 25 eqtrd ⊢A∈UHGraph∧B∈UHGraph∧C∈X∧f:Vtx⁡A⟶1-1 ontoVtx⁡B∧v:Vtx⁡B⟶1-1 ontoVtx⁡C∧g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i∧w:dom⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡C∧∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k∧j∈dom⁡iEdg⁡A→vfiEdg⁡A⁡j=iEdg⁡C⁡w⁡g⁡j
27 f1ofn ⊢g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B→gFndom⁡iEdg⁡A
28 27 adantr ⊢g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i→gFndom⁡iEdg⁡A
29 28 ad2antlr ⊢A∈UHGraph∧B∈UHGraph∧C∈X∧f:Vtx⁡A⟶1-1 ontoVtx⁡B∧v:Vtx⁡B⟶1-1 ontoVtx⁡C∧g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i∧w:dom⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡C∧∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k→gFndom⁡iEdg⁡A
30 fvco2 ⊢gFndom⁡iEdg⁡A∧j∈dom⁡iEdg⁡A→w∘g⁡j=w⁡g⁡j
31 29 30 sylan ⊢A∈UHGraph∧B∈UHGraph∧C∈X∧f:Vtx⁡A⟶1-1 ontoVtx⁡B∧v:Vtx⁡B⟶1-1 ontoVtx⁡C∧g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i∧w:dom⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡C∧∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k∧j∈dom⁡iEdg⁡A→w∘g⁡j=w⁡g⁡j
32 31 eqcomd ⊢A∈UHGraph∧B∈UHGraph∧C∈X∧f:Vtx⁡A⟶1-1 ontoVtx⁡B∧v:Vtx⁡B⟶1-1 ontoVtx⁡C∧g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i∧w:dom⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡C∧∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k∧j∈dom⁡iEdg⁡A→w⁡g⁡j=w∘g⁡j
33 32 fveq2d ⊢A∈UHGraph∧B∈UHGraph∧C∈X∧f:Vtx⁡A⟶1-1 ontoVtx⁡B∧v:Vtx⁡B⟶1-1 ontoVtx⁡C∧g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i∧w:dom⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡C∧∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k∧j∈dom⁡iEdg⁡A→iEdg⁡C⁡w⁡g⁡j=iEdg⁡C⁡w∘g⁡j
34 2 26 33 3eqtrd ⊢A∈UHGraph∧B∈UHGraph∧C∈X∧f:Vtx⁡A⟶1-1 ontoVtx⁡B∧v:Vtx⁡B⟶1-1 ontoVtx⁡C∧g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i∧w:dom⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡C∧∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k∧j∈dom⁡iEdg⁡A→v∘fiEdg⁡A⁡j=iEdg⁡C⁡w∘g⁡j
35 34 ralrimiva ⊢A∈UHGraph∧B∈UHGraph∧C∈X∧f:Vtx⁡A⟶1-1 ontoVtx⁡B∧v:Vtx⁡B⟶1-1 ontoVtx⁡C∧g:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡g⁡i∧w:dom⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡C∧∀k∈dom⁡iEdg⁡BviEdg⁡B⁡k=iEdg⁡C⁡w⁡k→∀j∈dom⁡iEdg⁡Av∘fiEdg⁡A⁡j=iEdg⁡C⁡w∘g⁡j