Metamath Proof Explorer

Theorem isomushgr

Description: The isomorphy relation for two simple hypergraphs. (Contributed by AV, 28-Nov-2022)

Ref Expression
Hypotheses isomushgr.v ⊢V=Vtx⁡A
isomushgr.w ⊢W=Vtx⁡B
isomushgr.e ⊢E=Edg⁡A
isomushgr.k ⊢K=Edg⁡B
Assertion isomushgr ⊢A∈USHGraph∧B∈USHGraph→AIsomGrB↔∃ff:V⟶1-1 ontoW∧∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e

Proof

Step Hyp Ref Expression
1 isomushgr.v ⊢V=Vtx⁡A
2 isomushgr.w ⊢W=Vtx⁡B
3 isomushgr.e ⊢E=Edg⁡A
4 isomushgr.k ⊢K=Edg⁡B
5 eqid ⊢iEdg⁡A=iEdg⁡A
6 eqid ⊢iEdg⁡B=iEdg⁡B
7 1 2 5 6 isomgr ⊢A∈USHGraph∧B∈USHGraph→AIsomGrB↔∃ff:V⟶1-1 ontoW∧∃hh:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i
8 fvex ⊢iEdg⁡B∈V
9 vex ⊢h∈V
10 fvex ⊢iEdg⁡A∈V
11 10 cnvex ⊢iEdg⁡A-1∈V
12 9 11 coex ⊢h∘iEdg⁡A-1∈V
13 8 12 coex ⊢iEdg⁡B∘h∘iEdg⁡A-1∈V
14 13 a1i ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→iEdg⁡B∘h∘iEdg⁡A-1∈V
15 2 6 ushgrf ⊢B∈USHGraph→iEdg⁡B:dom⁡iEdg⁡B⟶1-1𝒫W∖∅
16 f1f1orn ⊢iEdg⁡B:dom⁡iEdg⁡B⟶1-1𝒫W∖∅→iEdg⁡B:dom⁡iEdg⁡B⟶1-1 ontoran⁡iEdg⁡B
17 15 16 syl ⊢B∈USHGraph→iEdg⁡B:dom⁡iEdg⁡B⟶1-1 ontoran⁡iEdg⁡B
18 edgval ⊢Edg⁡B=ran⁡iEdg⁡B
19 4 18 eqtri ⊢K=ran⁡iEdg⁡B
20 f1oeq3 ⊢K=ran⁡iEdg⁡B→iEdg⁡B:dom⁡iEdg⁡B⟶1-1 ontoK↔iEdg⁡B:dom⁡iEdg⁡B⟶1-1 ontoran⁡iEdg⁡B
21 19 20 ax-mp ⊢iEdg⁡B:dom⁡iEdg⁡B⟶1-1 ontoK↔iEdg⁡B:dom⁡iEdg⁡B⟶1-1 ontoran⁡iEdg⁡B
22 17 21 sylibr ⊢B∈USHGraph→iEdg⁡B:dom⁡iEdg⁡B⟶1-1 ontoK
23 22 ad3antlr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→iEdg⁡B:dom⁡iEdg⁡B⟶1-1 ontoK
24 simprl ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B
25 1 5 ushgrf ⊢A∈USHGraph→iEdg⁡A:dom⁡iEdg⁡A⟶1-1𝒫V∖∅
26 f1f1orn ⊢iEdg⁡A:dom⁡iEdg⁡A⟶1-1𝒫V∖∅→iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoran⁡iEdg⁡A
27 25 26 syl ⊢A∈USHGraph→iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoran⁡iEdg⁡A
28 edgval ⊢Edg⁡A=ran⁡iEdg⁡A
29 3 28 eqtri ⊢E=ran⁡iEdg⁡A
30 f1oeq3 ⊢E=ran⁡iEdg⁡A→iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoE↔iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoran⁡iEdg⁡A
31 29 30 ax-mp ⊢iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoE↔iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoran⁡iEdg⁡A
32 27 31 sylibr ⊢A∈USHGraph→iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoE
33 f1ocnv ⊢iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoE→iEdg⁡A-1:E⟶1-1 ontodom⁡iEdg⁡A
34 32 33 syl ⊢A∈USHGraph→iEdg⁡A-1:E⟶1-1 ontodom⁡iEdg⁡A
35 34 ad3antrrr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→iEdg⁡A-1:E⟶1-1 ontodom⁡iEdg⁡A
36 f1oco ⊢h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧iEdg⁡A-1:E⟶1-1 ontodom⁡iEdg⁡A→h∘iEdg⁡A-1:E⟶1-1 ontodom⁡iEdg⁡B
37 24 35 36 syl2anc ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→h∘iEdg⁡A-1:E⟶1-1 ontodom⁡iEdg⁡B
38 f1oco ⊢iEdg⁡B:dom⁡iEdg⁡B⟶1-1 ontoK∧h∘iEdg⁡A-1:E⟶1-1 ontodom⁡iEdg⁡B→iEdg⁡B∘h∘iEdg⁡A-1:E⟶1-1 ontoK
39 23 37 38 syl2anc ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→iEdg⁡B∘h∘iEdg⁡A-1:E⟶1-1 ontoK
40 29 eleq2i ⊢e∈E↔e∈ran⁡iEdg⁡A
41 f1fn ⊢iEdg⁡A:dom⁡iEdg⁡A⟶1-1𝒫V∖∅→iEdg⁡AFndom⁡iEdg⁡A
42 25 41 syl ⊢A∈USHGraph→iEdg⁡AFndom⁡iEdg⁡A
43 fvelrnb ⊢iEdg⁡AFndom⁡iEdg⁡A→e∈ran⁡iEdg⁡A↔∃j∈dom⁡iEdg⁡AiEdg⁡A⁡j=e
44 42 43 syl ⊢A∈USHGraph→e∈ran⁡iEdg⁡A↔∃j∈dom⁡iEdg⁡AiEdg⁡A⁡j=e
45 44 ad3antrrr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→e∈ran⁡iEdg⁡A↔∃j∈dom⁡iEdg⁡AiEdg⁡A⁡j=e
46 fveq2 ⊢i=j→iEdg⁡A⁡i=iEdg⁡A⁡j
47 46 imaeq2d ⊢i=j→fiEdg⁡A⁡i=fiEdg⁡A⁡j
48 2fveq3 ⊢i=j→iEdg⁡B⁡h⁡i=iEdg⁡B⁡h⁡j
49 47 48 eqeq12d ⊢i=j→fiEdg⁡A⁡i=iEdg⁡B⁡h⁡i↔fiEdg⁡A⁡j=iEdg⁡B⁡h⁡j
50 49 rspccv ⊢∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→j∈dom⁡iEdg⁡A→fiEdg⁡A⁡j=iEdg⁡B⁡h⁡j
51 50 ad2antll ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→j∈dom⁡iEdg⁡A→fiEdg⁡A⁡j=iEdg⁡B⁡h⁡j
52 51 imp ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i∧j∈dom⁡iEdg⁡A→fiEdg⁡A⁡j=iEdg⁡B⁡h⁡j
53 coass ⊢iEdg⁡B∘h∘iEdg⁡A-1=iEdg⁡B∘h∘iEdg⁡A-1
54 53 eqcomi ⊢iEdg⁡B∘h∘iEdg⁡A-1=iEdg⁡B∘h∘iEdg⁡A-1
55 54 fveq1i ⊢iEdg⁡B∘h∘iEdg⁡A-1⁡iEdg⁡A⁡j=iEdg⁡B∘h∘iEdg⁡A-1⁡iEdg⁡A⁡j
56 dff1o4 ⊢iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoran⁡iEdg⁡A↔iEdg⁡AFndom⁡iEdg⁡A∧iEdg⁡A-1Fnran⁡iEdg⁡A
57 27 56 sylib ⊢A∈USHGraph→iEdg⁡AFndom⁡iEdg⁡A∧iEdg⁡A-1Fnran⁡iEdg⁡A
58 57 simprd ⊢A∈USHGraph→iEdg⁡A-1Fnran⁡iEdg⁡A
59 58 ad4antr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i∧j∈dom⁡iEdg⁡A→iEdg⁡A-1Fnran⁡iEdg⁡A
60 f1of ⊢iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoran⁡iEdg⁡A→iEdg⁡A:dom⁡iEdg⁡A⟶ran⁡iEdg⁡A
61 27 60 syl ⊢A∈USHGraph→iEdg⁡A:dom⁡iEdg⁡A⟶ran⁡iEdg⁡A
62 61 ad3antrrr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→iEdg⁡A:dom⁡iEdg⁡A⟶ran⁡iEdg⁡A
63 62 ffvelcdmda ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i∧j∈dom⁡iEdg⁡A→iEdg⁡A⁡j∈ran⁡iEdg⁡A
64 fvco2 ⊢iEdg⁡A-1Fnran⁡iEdg⁡A∧iEdg⁡A⁡j∈ran⁡iEdg⁡A→iEdg⁡B∘h∘iEdg⁡A-1⁡iEdg⁡A⁡j=iEdg⁡B∘h⁡iEdg⁡A-1⁡iEdg⁡A⁡j
65 59 63 64 syl2anc ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i∧j∈dom⁡iEdg⁡A→iEdg⁡B∘h∘iEdg⁡A-1⁡iEdg⁡A⁡j=iEdg⁡B∘h⁡iEdg⁡A-1⁡iEdg⁡A⁡j
66 32 ad3antrrr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoE
67 f1ocnvfv1 ⊢iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoE∧j∈dom⁡iEdg⁡A→iEdg⁡A-1⁡iEdg⁡A⁡j=j
68 66 67 sylan ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i∧j∈dom⁡iEdg⁡A→iEdg⁡A-1⁡iEdg⁡A⁡j=j
69 68 fveq2d ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i∧j∈dom⁡iEdg⁡A→iEdg⁡B∘h⁡iEdg⁡A-1⁡iEdg⁡A⁡j=iEdg⁡B∘h⁡j
70 f1ofn ⊢h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B→hFndom⁡iEdg⁡A
71 70 ad2antrl ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→hFndom⁡iEdg⁡A
72 fvco2 ⊢hFndom⁡iEdg⁡A∧j∈dom⁡iEdg⁡A→iEdg⁡B∘h⁡j=iEdg⁡B⁡h⁡j
73 71 72 sylan ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i∧j∈dom⁡iEdg⁡A→iEdg⁡B∘h⁡j=iEdg⁡B⁡h⁡j
74 65 69 73 3eqtrd ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i∧j∈dom⁡iEdg⁡A→iEdg⁡B∘h∘iEdg⁡A-1⁡iEdg⁡A⁡j=iEdg⁡B⁡h⁡j
75 55 74 eqtr2id ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i∧j∈dom⁡iEdg⁡A→iEdg⁡B⁡h⁡j=iEdg⁡B∘h∘iEdg⁡A-1⁡iEdg⁡A⁡j
76 75 ad2antrr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i∧j∈dom⁡iEdg⁡A∧fiEdg⁡A⁡j=iEdg⁡B⁡h⁡j∧iEdg⁡A⁡j=e→iEdg⁡B⁡h⁡j=iEdg⁡B∘h∘iEdg⁡A-1⁡iEdg⁡A⁡j
77 imaeq2 ⊢e=iEdg⁡A⁡j→fe=fiEdg⁡A⁡j
78 77 eqcoms ⊢iEdg⁡A⁡j=e→fe=fiEdg⁡A⁡j
79 simpr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i∧j∈dom⁡iEdg⁡A∧fiEdg⁡A⁡j=iEdg⁡B⁡h⁡j→fiEdg⁡A⁡j=iEdg⁡B⁡h⁡j
80 78 79 sylan9eqr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i∧j∈dom⁡iEdg⁡A∧fiEdg⁡A⁡j=iEdg⁡B⁡h⁡j∧iEdg⁡A⁡j=e→fe=iEdg⁡B⁡h⁡j
81 fveq2 ⊢e=iEdg⁡A⁡j→iEdg⁡B∘h∘iEdg⁡A-1⁡e=iEdg⁡B∘h∘iEdg⁡A-1⁡iEdg⁡A⁡j
82 81 eqcoms ⊢iEdg⁡A⁡j=e→iEdg⁡B∘h∘iEdg⁡A-1⁡e=iEdg⁡B∘h∘iEdg⁡A-1⁡iEdg⁡A⁡j
83 82 adantl ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i∧j∈dom⁡iEdg⁡A∧fiEdg⁡A⁡j=iEdg⁡B⁡h⁡j∧iEdg⁡A⁡j=e→iEdg⁡B∘h∘iEdg⁡A-1⁡e=iEdg⁡B∘h∘iEdg⁡A-1⁡iEdg⁡A⁡j
84 76 80 83 3eqtr4d ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i∧j∈dom⁡iEdg⁡A∧fiEdg⁡A⁡j=iEdg⁡B⁡h⁡j∧iEdg⁡A⁡j=e→fe=iEdg⁡B∘h∘iEdg⁡A-1⁡e
85 84 ex ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i∧j∈dom⁡iEdg⁡A∧fiEdg⁡A⁡j=iEdg⁡B⁡h⁡j→iEdg⁡A⁡j=e→fe=iEdg⁡B∘h∘iEdg⁡A-1⁡e
86 52 85 mpdan ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i∧j∈dom⁡iEdg⁡A→iEdg⁡A⁡j=e→fe=iEdg⁡B∘h∘iEdg⁡A-1⁡e
87 86 rexlimdva ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→∃j∈dom⁡iEdg⁡AiEdg⁡A⁡j=e→fe=iEdg⁡B∘h∘iEdg⁡A-1⁡e
88 45 87 sylbid ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→e∈ran⁡iEdg⁡A→fe=iEdg⁡B∘h∘iEdg⁡A-1⁡e
89 40 88 biimtrid ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→e∈E→fe=iEdg⁡B∘h∘iEdg⁡A-1⁡e
90 89 ralrimiv ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→∀e∈Efe=iEdg⁡B∘h∘iEdg⁡A-1⁡e
91 39 90 jca ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→iEdg⁡B∘h∘iEdg⁡A-1:E⟶1-1 ontoK∧∀e∈Efe=iEdg⁡B∘h∘iEdg⁡A-1⁡e
92 f1oeq1 ⊢g=iEdg⁡B∘h∘iEdg⁡A-1→g:E⟶1-1 ontoK↔iEdg⁡B∘h∘iEdg⁡A-1:E⟶1-1 ontoK
93 fveq1 ⊢g=iEdg⁡B∘h∘iEdg⁡A-1→g⁡e=iEdg⁡B∘h∘iEdg⁡A-1⁡e
94 93 eqeq2d ⊢g=iEdg⁡B∘h∘iEdg⁡A-1→fe=g⁡e↔fe=iEdg⁡B∘h∘iEdg⁡A-1⁡e
95 94 ralbidv ⊢g=iEdg⁡B∘h∘iEdg⁡A-1→∀e∈Efe=g⁡e↔∀e∈Efe=iEdg⁡B∘h∘iEdg⁡A-1⁡e
96 92 95 anbi12d ⊢g=iEdg⁡B∘h∘iEdg⁡A-1→g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e↔iEdg⁡B∘h∘iEdg⁡A-1:E⟶1-1 ontoK∧∀e∈Efe=iEdg⁡B∘h∘iEdg⁡A-1⁡e
97 14 91 96 spcedv ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e
98 97 ex ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW→h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e
99 98 exlimdv ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW→∃hh:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i→∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e
100 8 cnvex ⊢iEdg⁡B-1∈V
101 vex ⊢g∈V
102 101 10 coex ⊢g∘iEdg⁡A∈V
103 100 102 coex ⊢iEdg⁡B-1∘g∘iEdg⁡A∈V
104 103 a1i ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→iEdg⁡B-1∘g∘iEdg⁡A∈V
105 17 ad3antlr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→iEdg⁡B:dom⁡iEdg⁡B⟶1-1 ontoran⁡iEdg⁡B
106 f1ocnv ⊢iEdg⁡B:dom⁡iEdg⁡B⟶1-1 ontoran⁡iEdg⁡B→iEdg⁡B-1:ran⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡B
107 105 106 syl ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→iEdg⁡B-1:ran⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡B
108 f1oeq23 ⊢E=ran⁡iEdg⁡A∧K=ran⁡iEdg⁡B→g:E⟶1-1 ontoK↔g:ran⁡iEdg⁡A⟶1-1 ontoran⁡iEdg⁡B
109 29 19 108 mp2an ⊢g:E⟶1-1 ontoK↔g:ran⁡iEdg⁡A⟶1-1 ontoran⁡iEdg⁡B
110 109 biimpi ⊢g:E⟶1-1 ontoK→g:ran⁡iEdg⁡A⟶1-1 ontoran⁡iEdg⁡B
111 110 ad2antrl ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→g:ran⁡iEdg⁡A⟶1-1 ontoran⁡iEdg⁡B
112 27 ad3antrrr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoran⁡iEdg⁡A
113 f1oco ⊢g:ran⁡iEdg⁡A⟶1-1 ontoran⁡iEdg⁡B∧iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoran⁡iEdg⁡A→g∘iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoran⁡iEdg⁡B
114 111 112 113 syl2anc ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→g∘iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoran⁡iEdg⁡B
115 f1oco ⊢iEdg⁡B-1:ran⁡iEdg⁡B⟶1-1 ontodom⁡iEdg⁡B∧g∘iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoran⁡iEdg⁡B→iEdg⁡B-1∘g∘iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B
116 107 114 115 syl2anc ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→iEdg⁡B-1∘g∘iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B
117 61 ad2antrr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW→iEdg⁡A:dom⁡iEdg⁡A⟶ran⁡iEdg⁡A
118 117 ffund ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW→Fun⁡iEdg⁡A
119 118 adantr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→Fun⁡iEdg⁡A
120 fvelrn ⊢Fun⁡iEdg⁡A∧i∈dom⁡iEdg⁡A→iEdg⁡A⁡i∈ran⁡iEdg⁡A
121 119 120 sylan ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A→iEdg⁡A⁡i∈ran⁡iEdg⁡A
122 29 raleqi ⊢∀e∈Efe=g⁡e↔∀e∈ran⁡iEdg⁡Afe=g⁡e
123 122 biimpi ⊢∀e∈Efe=g⁡e→∀e∈ran⁡iEdg⁡Afe=g⁡e
124 123 ad2antll ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→∀e∈ran⁡iEdg⁡Afe=g⁡e
125 124 adantr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A→∀e∈ran⁡iEdg⁡Afe=g⁡e
126 imaeq2 ⊢e=iEdg⁡A⁡i→fe=fiEdg⁡A⁡i
127 fveq2 ⊢e=iEdg⁡A⁡i→g⁡e=g⁡iEdg⁡A⁡i
128 126 127 eqeq12d ⊢e=iEdg⁡A⁡i→fe=g⁡e↔fiEdg⁡A⁡i=g⁡iEdg⁡A⁡i
129 128 rspccva ⊢∀e∈ran⁡iEdg⁡Afe=g⁡e∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→fiEdg⁡A⁡i=g⁡iEdg⁡A⁡i
130 125 129 sylan ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→fiEdg⁡A⁡i=g⁡iEdg⁡A⁡i
131 feq3 ⊢E=ran⁡iEdg⁡A→iEdg⁡A:dom⁡iEdg⁡A⟶E↔iEdg⁡A:dom⁡iEdg⁡A⟶ran⁡iEdg⁡A
132 29 131 ax-mp ⊢iEdg⁡A:dom⁡iEdg⁡A⟶E↔iEdg⁡A:dom⁡iEdg⁡A⟶ran⁡iEdg⁡A
133 61 132 sylibr ⊢A∈USHGraph→iEdg⁡A:dom⁡iEdg⁡A⟶E
134 133 ad2antrr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW→iEdg⁡A:dom⁡iEdg⁡A⟶E
135 f1ofn ⊢g:E⟶1-1 ontoK→gFnE
136 135 adantr ⊢g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→gFnE
137 134 136 anim12ci ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→gFnE∧iEdg⁡A:dom⁡iEdg⁡A⟶E
138 137 ad2antrr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→gFnE∧iEdg⁡A:dom⁡iEdg⁡A⟶E
139 fnfco ⊢gFnE∧iEdg⁡A:dom⁡iEdg⁡A⟶E→g∘iEdg⁡AFndom⁡iEdg⁡A
140 138 139 syl ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→g∘iEdg⁡AFndom⁡iEdg⁡A
141 simplr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→i∈dom⁡iEdg⁡A
142 fvco2 ⊢g∘iEdg⁡AFndom⁡iEdg⁡A∧i∈dom⁡iEdg⁡A→I↾ran⁡iEdg⁡B∘g∘iEdg⁡A⁡i=I↾ran⁡iEdg⁡B⁡g∘iEdg⁡A⁡i
143 140 141 142 syl2anc ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→I↾ran⁡iEdg⁡B∘g∘iEdg⁡A⁡i=I↾ran⁡iEdg⁡B⁡g∘iEdg⁡A⁡i
144 f1of ⊢iEdg⁡B:dom⁡iEdg⁡B⟶1-1 ontoK→iEdg⁡B:dom⁡iEdg⁡B⟶K
145 22 144 syl ⊢B∈USHGraph→iEdg⁡B:dom⁡iEdg⁡B⟶K
146 145 ffund ⊢B∈USHGraph→Fun⁡iEdg⁡B
147 funcocnv2 ⊢Fun⁡iEdg⁡B→iEdg⁡B∘iEdg⁡B-1=I↾ran⁡iEdg⁡B
148 146 147 syl ⊢B∈USHGraph→iEdg⁡B∘iEdg⁡B-1=I↾ran⁡iEdg⁡B
149 148 eqcomd ⊢B∈USHGraph→I↾ran⁡iEdg⁡B=iEdg⁡B∘iEdg⁡B-1
150 149 ad5antlr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→I↾ran⁡iEdg⁡B=iEdg⁡B∘iEdg⁡B-1
151 150 coeq1d ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→I↾ran⁡iEdg⁡B∘g∘iEdg⁡A=iEdg⁡B∘iEdg⁡B-1∘g∘iEdg⁡A
152 151 fveq1d ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→I↾ran⁡iEdg⁡B∘g∘iEdg⁡A⁡i=iEdg⁡B∘iEdg⁡B-1∘g∘iEdg⁡A⁡i
153 coass ⊢iEdg⁡B∘iEdg⁡B-1∘g∘iEdg⁡A=iEdg⁡B∘iEdg⁡B-1∘g∘iEdg⁡A
154 153 fveq1i ⊢iEdg⁡B∘iEdg⁡B-1∘g∘iEdg⁡A⁡i=iEdg⁡B∘iEdg⁡B-1∘g∘iEdg⁡A⁡i
155 152 154 eqtrdi ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→I↾ran⁡iEdg⁡B∘g∘iEdg⁡A⁡i=iEdg⁡B∘iEdg⁡B-1∘g∘iEdg⁡A⁡i
156 f1of ⊢g:E⟶1-1 ontoK→g:E⟶K
157 eqid ⊢E=E
158 157 19 feq23i ⊢g:E⟶K↔g:E⟶ran⁡iEdg⁡B
159 156 158 sylib ⊢g:E⟶1-1 ontoK→g:E⟶ran⁡iEdg⁡B
160 159 adantr ⊢g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→g:E⟶ran⁡iEdg⁡B
161 f1of ⊢iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontoE→iEdg⁡A:dom⁡iEdg⁡A⟶E
162 32 161 syl ⊢A∈USHGraph→iEdg⁡A:dom⁡iEdg⁡A⟶E
163 162 ad2antrr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW→iEdg⁡A:dom⁡iEdg⁡A⟶E
164 fco ⊢g:E⟶ran⁡iEdg⁡B∧iEdg⁡A:dom⁡iEdg⁡A⟶E→g∘iEdg⁡A:dom⁡iEdg⁡A⟶ran⁡iEdg⁡B
165 160 163 164 syl2anr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→g∘iEdg⁡A:dom⁡iEdg⁡A⟶ran⁡iEdg⁡B
166 165 anim1i ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A→g∘iEdg⁡A:dom⁡iEdg⁡A⟶ran⁡iEdg⁡B∧i∈dom⁡iEdg⁡A
167 166 adantr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→g∘iEdg⁡A:dom⁡iEdg⁡A⟶ran⁡iEdg⁡B∧i∈dom⁡iEdg⁡A
168 ffvelcdm ⊢g∘iEdg⁡A:dom⁡iEdg⁡A⟶ran⁡iEdg⁡B∧i∈dom⁡iEdg⁡A→g∘iEdg⁡A⁡i∈ran⁡iEdg⁡B
169 167 168 syl ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→g∘iEdg⁡A⁡i∈ran⁡iEdg⁡B
170 fvresi ⊢g∘iEdg⁡A⁡i∈ran⁡iEdg⁡B→I↾ran⁡iEdg⁡B⁡g∘iEdg⁡A⁡i=g∘iEdg⁡A⁡i
171 169 170 syl ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→I↾ran⁡iEdg⁡B⁡g∘iEdg⁡A⁡i=g∘iEdg⁡A⁡i
172 162 ad3antrrr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→iEdg⁡A:dom⁡iEdg⁡A⟶E
173 172 anim1i ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A→iEdg⁡A:dom⁡iEdg⁡A⟶E∧i∈dom⁡iEdg⁡A
174 173 adantr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→iEdg⁡A:dom⁡iEdg⁡A⟶E∧i∈dom⁡iEdg⁡A
175 fvco3 ⊢iEdg⁡A:dom⁡iEdg⁡A⟶E∧i∈dom⁡iEdg⁡A→g∘iEdg⁡A⁡i=g⁡iEdg⁡A⁡i
176 174 175 syl ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→g∘iEdg⁡A⁡i=g⁡iEdg⁡A⁡i
177 171 176 eqtrd ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→I↾ran⁡iEdg⁡B⁡g∘iEdg⁡A⁡i=g⁡iEdg⁡A⁡i
178 143 155 177 3eqtr3rd ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→g⁡iEdg⁡A⁡i=iEdg⁡B∘iEdg⁡B-1∘g∘iEdg⁡A⁡i
179 dff1o4 ⊢iEdg⁡B:dom⁡iEdg⁡B⟶1-1 ontoK↔iEdg⁡BFndom⁡iEdg⁡B∧iEdg⁡B-1FnK
180 22 179 sylib ⊢B∈USHGraph→iEdg⁡BFndom⁡iEdg⁡B∧iEdg⁡B-1FnK
181 180 simprd ⊢B∈USHGraph→iEdg⁡B-1FnK
182 181 ad5antlr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→iEdg⁡B-1FnK
183 156 adantr ⊢g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→g:E⟶K
184 134 183 anim12ci ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→g:E⟶K∧iEdg⁡A:dom⁡iEdg⁡A⟶E
185 184 ad2antrr ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→g:E⟶K∧iEdg⁡A:dom⁡iEdg⁡A⟶E
186 fco ⊢g:E⟶K∧iEdg⁡A:dom⁡iEdg⁡A⟶E→g∘iEdg⁡A:dom⁡iEdg⁡A⟶K
187 185 186 syl ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→g∘iEdg⁡A:dom⁡iEdg⁡A⟶K
188 fnfco ⊢iEdg⁡B-1FnK∧g∘iEdg⁡A:dom⁡iEdg⁡A⟶K→iEdg⁡B-1∘g∘iEdg⁡AFndom⁡iEdg⁡A
189 182 187 188 syl2anc ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→iEdg⁡B-1∘g∘iEdg⁡AFndom⁡iEdg⁡A
190 fvco2 ⊢iEdg⁡B-1∘g∘iEdg⁡AFndom⁡iEdg⁡A∧i∈dom⁡iEdg⁡A→iEdg⁡B∘iEdg⁡B-1∘g∘iEdg⁡A⁡i=iEdg⁡B⁡iEdg⁡B-1∘g∘iEdg⁡A⁡i
191 189 141 190 syl2anc ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→iEdg⁡B∘iEdg⁡B-1∘g∘iEdg⁡A⁡i=iEdg⁡B⁡iEdg⁡B-1∘g∘iEdg⁡A⁡i
192 130 178 191 3eqtrd ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A∧iEdg⁡A⁡i∈ran⁡iEdg⁡A→fiEdg⁡A⁡i=iEdg⁡B⁡iEdg⁡B-1∘g∘iEdg⁡A⁡i
193 121 192 mpdan ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e∧i∈dom⁡iEdg⁡A→fiEdg⁡A⁡i=iEdg⁡B⁡iEdg⁡B-1∘g∘iEdg⁡A⁡i
194 193 ralrimiva ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡iEdg⁡B-1∘g∘iEdg⁡A⁡i
195 116 194 jca ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→iEdg⁡B-1∘g∘iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡iEdg⁡B-1∘g∘iEdg⁡A⁡i
196 f1oeq1 ⊢h=iEdg⁡B-1∘g∘iEdg⁡A→h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B↔iEdg⁡B-1∘g∘iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B
197 fveq1 ⊢h=iEdg⁡B-1∘g∘iEdg⁡A→h⁡i=iEdg⁡B-1∘g∘iEdg⁡A⁡i
198 197 fveq2d ⊢h=iEdg⁡B-1∘g∘iEdg⁡A→iEdg⁡B⁡h⁡i=iEdg⁡B⁡iEdg⁡B-1∘g∘iEdg⁡A⁡i
199 198 eqeq2d ⊢h=iEdg⁡B-1∘g∘iEdg⁡A→fiEdg⁡A⁡i=iEdg⁡B⁡h⁡i↔fiEdg⁡A⁡i=iEdg⁡B⁡iEdg⁡B-1∘g∘iEdg⁡A⁡i
200 199 ralbidv ⊢h=iEdg⁡B-1∘g∘iEdg⁡A→∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i↔∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡iEdg⁡B-1∘g∘iEdg⁡A⁡i
201 196 200 anbi12d ⊢h=iEdg⁡B-1∘g∘iEdg⁡A→h:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i↔iEdg⁡B-1∘g∘iEdg⁡A:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡iEdg⁡B-1∘g∘iEdg⁡A⁡i
202 104 195 201 spcedv ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW∧g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→∃hh:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i
203 202 ex ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW→g:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→∃hh:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i
204 203 exlimdv ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW→∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e→∃hh:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i
205 99 204 impbid ⊢A∈USHGraph∧B∈USHGraph∧f:V⟶1-1 ontoW→∃hh:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i↔∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e
206 205 pm5.32da ⊢A∈USHGraph∧B∈USHGraph→f:V⟶1-1 ontoW∧∃hh:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i↔f:V⟶1-1 ontoW∧∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e
207 206 exbidv ⊢A∈USHGraph∧B∈USHGraph→∃ff:V⟶1-1 ontoW∧∃hh:dom⁡iEdg⁡A⟶1-1 ontodom⁡iEdg⁡B∧∀i∈dom⁡iEdg⁡AfiEdg⁡A⁡i=iEdg⁡B⁡h⁡i↔∃ff:V⟶1-1 ontoW∧∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e
208 7 207 bitrd ⊢A∈USHGraph∧B∈USHGraph→AIsomGrB↔∃ff:V⟶1-1 ontoW∧∃gg:E⟶1-1 ontoK∧∀e∈Efe=g⁡e