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 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k j dom iEdg A v f iEdg A j = iEdg C w g j

Proof

Step Hyp Ref Expression
1 imaco v f iEdg A j = v f iEdg A j
2 1 a1i A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k j dom iEdg A v f iEdg A j = v f iEdg A j
3 fveq2 i = j iEdg A i = iEdg A j
4 3 imaeq2d i = j f iEdg A i = f iEdg A j
5 2fveq3 i = j iEdg B g i = iEdg B g j
6 4 5 eqeq12d i = j f iEdg A i = iEdg B g i f iEdg A j = iEdg B g j
7 6 rspccv i dom iEdg A f iEdg A i = iEdg B g i j dom iEdg A f iEdg A j = iEdg B g j
8 7 adantl g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i j dom iEdg A f iEdg A j = iEdg B g j
9 8 ad2antlr A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k j dom iEdg A f iEdg A j = iEdg B g j
10 9 imp A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k j dom iEdg A f iEdg A j = iEdg B g j
11 10 imaeq2d A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k j dom iEdg A v f iEdg A j = v iEdg B g j
12 simplrr A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k j dom iEdg A k dom iEdg B v iEdg B k = iEdg C w k
13 f1of g : dom iEdg A 1-1 onto dom iEdg B g : dom iEdg A dom iEdg B
14 ffvelrn 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 onto dom iEdg B j dom iEdg A g j dom iEdg B
17 16 adantr g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg 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 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg 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 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg 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 v iEdg B k = v iEdg B g j
22 2fveq3 k = g j iEdg C w k = iEdg C w g j
23 21 22 eqeq12d k = g j v iEdg B k = iEdg C w k v iEdg B g j = iEdg C w g j
24 23 rspccv k dom iEdg B v iEdg B k = iEdg C w k g j dom iEdg B v iEdg B g j = iEdg C w g j
25 12 19 24 sylc A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k j dom iEdg A v iEdg B g j = iEdg C w g j
26 11 25 eqtrd A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k j dom iEdg A v f iEdg A j = iEdg C w g j
27 f1ofn g : dom iEdg A 1-1 onto dom iEdg B g Fn dom iEdg A
28 27 adantr g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i g Fn dom iEdg A
29 28 ad2antlr A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k g Fn dom iEdg A
30 fvco2 g Fn dom 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 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg 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 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg 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 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg 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 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k j dom iEdg A v f iEdg A j = iEdg C w g j
35 34 ralrimiva A UHGraph B UHGraph C X f : Vtx A 1-1 onto Vtx B v : Vtx B 1-1 onto Vtx C g : dom iEdg A 1-1 onto dom iEdg B i dom iEdg A f iEdg A i = iEdg B g i w : dom iEdg B 1-1 onto dom iEdg C k dom iEdg B v iEdg B k = iEdg C w k j dom iEdg A v f iEdg A j = iEdg C w g j