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 → A IsomGr B ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∃ g g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 → A IsomGr B ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∃ h h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ 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 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ 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 onto ran ⁡ iEdg ⁡ B
17 15 16 syl ⊢ B ∈ USHGraph → iEdg ⁡ B : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto ran ⁡ 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 onto K ↔ iEdg ⁡ B : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto ran ⁡ iEdg ⁡ B
21 19 20 ax-mp ⊢ iEdg ⁡ B : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto K ↔ iEdg ⁡ B : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto ran ⁡ iEdg ⁡ B
22 17 21 sylibr ⊢ B ∈ USHGraph → iEdg ⁡ B : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto K
23 22 ad3antlr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → iEdg ⁡ B : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto K
24 simprl ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ 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 onto ran ⁡ iEdg ⁡ A
27 25 26 syl ⊢ A ∈ USHGraph → iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto ran ⁡ 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 onto E ↔ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto ran ⁡ iEdg ⁡ A
31 29 30 ax-mp ⊢ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto E ↔ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto ran ⁡ iEdg ⁡ A
32 27 31 sylibr ⊢ A ∈ USHGraph → iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto E
33 f1ocnv ⊢ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto E → iEdg ⁡ A -1 : E ⟶ 1-1 onto dom ⁡ iEdg ⁡ A
34 32 33 syl ⊢ A ∈ USHGraph → iEdg ⁡ A -1 : E ⟶ 1-1 onto dom ⁡ iEdg ⁡ A
35 34 ad3antrrr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → iEdg ⁡ A -1 : E ⟶ 1-1 onto dom ⁡ iEdg ⁡ A
36 f1oco ⊢ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ iEdg ⁡ A -1 : E ⟶ 1-1 onto dom ⁡ iEdg ⁡ A → h ∘ iEdg ⁡ A -1 : E ⟶ 1-1 onto dom ⁡ iEdg ⁡ B
37 24 35 36 syl2anc ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → h ∘ iEdg ⁡ A -1 : E ⟶ 1-1 onto dom ⁡ iEdg ⁡ B
38 f1oco ⊢ iEdg ⁡ B : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto K ∧ h ∘ iEdg ⁡ A -1 : E ⟶ 1-1 onto dom ⁡ iEdg ⁡ B → iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 : E ⟶ 1-1 onto K
39 23 37 38 syl2anc ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 : E ⟶ 1-1 onto K
40 29 eleq2i ⊢ e ∈ E ↔ e ∈ ran ⁡ iEdg ⁡ A
41 f1fn ⊢ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 𝒫 V ∖ ∅ → iEdg ⁡ A Fn dom ⁡ iEdg ⁡ A
42 25 41 syl ⊢ A ∈ USHGraph → iEdg ⁡ A Fn dom ⁡ iEdg ⁡ A
43 fvelrnb ⊢ iEdg ⁡ A Fn dom ⁡ iEdg ⁡ A → e ∈ ran ⁡ iEdg ⁡ A ↔ ∃ j ∈ dom ⁡ iEdg ⁡ A iEdg ⁡ A ⁡ j = e
44 42 43 syl ⊢ A ∈ USHGraph → e ∈ ran ⁡ iEdg ⁡ A ↔ ∃ j ∈ dom ⁡ iEdg ⁡ A iEdg ⁡ A ⁡ j = e
45 44 ad3antrrr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → e ∈ ran ⁡ iEdg ⁡ A ↔ ∃ j ∈ dom ⁡ iEdg ⁡ A iEdg ⁡ A ⁡ j = e
46 fveq2 ⊢ i = j → iEdg ⁡ A ⁡ i = iEdg ⁡ A ⁡ j
47 46 imaeq2d ⊢ i = j → f iEdg ⁡ A ⁡ i = f iEdg ⁡ A ⁡ j
48 2fveq3 ⊢ i = j → iEdg ⁡ B ⁡ h ⁡ i = iEdg ⁡ B ⁡ h ⁡ j
49 47 48 eqeq12d ⊢ i = j → f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i ↔ f iEdg ⁡ A ⁡ j = iEdg ⁡ B ⁡ h ⁡ j
50 49 rspccv ⊢ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → j ∈ dom ⁡ iEdg ⁡ A → f iEdg ⁡ A ⁡ j = iEdg ⁡ B ⁡ h ⁡ j
51 50 ad2antll ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → j ∈ dom ⁡ iEdg ⁡ A → f iEdg ⁡ A ⁡ j = iEdg ⁡ B ⁡ h ⁡ j
52 51 imp ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i ∧ j ∈ dom ⁡ iEdg ⁡ A → f iEdg ⁡ 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 onto ran ⁡ iEdg ⁡ A ↔ iEdg ⁡ A Fn dom ⁡ iEdg ⁡ A ∧ iEdg ⁡ A -1 Fn ran ⁡ iEdg ⁡ A
57 27 56 sylib ⊢ A ∈ USHGraph → iEdg ⁡ A Fn dom ⁡ iEdg ⁡ A ∧ iEdg ⁡ A -1 Fn ran ⁡ iEdg ⁡ A
58 57 simprd ⊢ A ∈ USHGraph → iEdg ⁡ A -1 Fn ran ⁡ iEdg ⁡ A
59 58 ad4antr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i ∧ j ∈ dom ⁡ iEdg ⁡ A → iEdg ⁡ A -1 Fn ran ⁡ iEdg ⁡ A
60 f1of ⊢ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto ran ⁡ 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 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ ran ⁡ iEdg ⁡ A
63 62 ffvelrnda ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i ∧ j ∈ dom ⁡ iEdg ⁡ A → iEdg ⁡ A ⁡ j ∈ ran ⁡ iEdg ⁡ A
64 fvco2 ⊢ iEdg ⁡ A -1 Fn ran ⁡ 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 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ 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 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto E
67 f1ocnvfv1 ⊢ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto E ∧ j ∈ dom ⁡ iEdg ⁡ A → iEdg ⁡ A -1 ⁡ iEdg ⁡ A ⁡ j = j
68 66 67 sylan ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ 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 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ 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 onto dom ⁡ iEdg ⁡ B → h Fn dom ⁡ iEdg ⁡ A
71 70 ad2antrl ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → h Fn dom ⁡ iEdg ⁡ A
72 fvco2 ⊢ h Fn dom ⁡ 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 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ 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 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ 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 syl5req ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ 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 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i ∧ j ∈ dom ⁡ iEdg ⁡ A ∧ f iEdg ⁡ 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 → f e = f iEdg ⁡ A ⁡ j
78 77 eqcoms ⊢ iEdg ⁡ A ⁡ j = e → f e = f iEdg ⁡ A ⁡ j
79 simpr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i ∧ j ∈ dom ⁡ iEdg ⁡ A ∧ f iEdg ⁡ A ⁡ j = iEdg ⁡ B ⁡ h ⁡ j → f iEdg ⁡ A ⁡ j = iEdg ⁡ B ⁡ h ⁡ j
80 78 79 sylan9eqr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i ∧ j ∈ dom ⁡ iEdg ⁡ A ∧ f iEdg ⁡ A ⁡ j = iEdg ⁡ B ⁡ h ⁡ j ∧ iEdg ⁡ A ⁡ j = e → f e = 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 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i ∧ j ∈ dom ⁡ iEdg ⁡ A ∧ f iEdg ⁡ 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 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i ∧ j ∈ dom ⁡ iEdg ⁡ A ∧ f iEdg ⁡ A ⁡ j = iEdg ⁡ B ⁡ h ⁡ j ∧ iEdg ⁡ A ⁡ j = e → f e = iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 ⁡ e
85 84 ex ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i ∧ j ∈ dom ⁡ iEdg ⁡ A ∧ f iEdg ⁡ A ⁡ j = iEdg ⁡ B ⁡ h ⁡ j → iEdg ⁡ A ⁡ j = e → f e = iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 ⁡ e
86 52 85 mpdan ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i ∧ j ∈ dom ⁡ iEdg ⁡ A → iEdg ⁡ A ⁡ j = e → f e = iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 ⁡ e
87 86 rexlimdva ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → ∃ j ∈ dom ⁡ iEdg ⁡ A iEdg ⁡ A ⁡ j = e → f e = iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 ⁡ e
88 45 87 sylbid ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → e ∈ ran ⁡ iEdg ⁡ A → f e = iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 ⁡ e
89 40 88 syl5bi ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → e ∈ E → f e = iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 ⁡ e
90 89 ralrimiv ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → ∀ e ∈ E f e = iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 ⁡ e
91 39 90 jca ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 ⁡ e
92 f1oeq1 ⊢ g = iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 → g : E ⟶ 1-1 onto K ↔ iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 : E ⟶ 1-1 onto K
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 → f e = g ⁡ e ↔ f e = iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 ⁡ e
95 94 ralbidv ⊢ g = iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 → ∀ e ∈ E f e = g ⁡ e ↔ ∀ e ∈ E f e = iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 ⁡ e
96 92 95 anbi12d ⊢ g = iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 → g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ↔ iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = iEdg ⁡ B ∘ h ∘ iEdg ⁡ A -1 ⁡ e
97 14 91 96 spcedv ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → ∃ g g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e
98 97 ex ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W → h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → ∃ g g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e
99 98 exlimdv ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W → ∃ h h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i → ∃ g g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → iEdg ⁡ B -1 ∘ g ∘ iEdg ⁡ A ∈ V
105 17 ad3antlr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → iEdg ⁡ B : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto ran ⁡ iEdg ⁡ B
106 f1ocnv ⊢ iEdg ⁡ B : dom ⁡ iEdg ⁡ B ⟶ 1-1 onto ran ⁡ iEdg ⁡ B → iEdg ⁡ B -1 : ran ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ B
107 105 106 syl ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → iEdg ⁡ B -1 : ran ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ B
108 f1oeq23 ⊢ E = ran ⁡ iEdg ⁡ A ∧ K = ran ⁡ iEdg ⁡ B → g : E ⟶ 1-1 onto K ↔ g : ran ⁡ iEdg ⁡ A ⟶ 1-1 onto ran ⁡ iEdg ⁡ B
109 29 19 108 mp2an ⊢ g : E ⟶ 1-1 onto K ↔ g : ran ⁡ iEdg ⁡ A ⟶ 1-1 onto ran ⁡ iEdg ⁡ B
110 109 biimpi ⊢ g : E ⟶ 1-1 onto K → g : ran ⁡ iEdg ⁡ A ⟶ 1-1 onto ran ⁡ iEdg ⁡ B
111 110 ad2antrl ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → g : ran ⁡ iEdg ⁡ A ⟶ 1-1 onto ran ⁡ iEdg ⁡ B
112 27 ad3antrrr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto ran ⁡ iEdg ⁡ A
113 f1oco ⊢ g : ran ⁡ iEdg ⁡ A ⟶ 1-1 onto ran ⁡ iEdg ⁡ B ∧ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto ran ⁡ iEdg ⁡ A → g ∘ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto ran ⁡ iEdg ⁡ B
114 111 112 113 syl2anc ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → g ∘ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto ran ⁡ iEdg ⁡ B
115 f1oco ⊢ iEdg ⁡ B -1 : ran ⁡ iEdg ⁡ B ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ g ∘ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto ran ⁡ iEdg ⁡ B → iEdg ⁡ B -1 ∘ g ∘ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B
116 107 114 115 syl2anc ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → iEdg ⁡ B -1 ∘ g ∘ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B
117 61 ad2antrr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W → iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ ran ⁡ iEdg ⁡ A
118 117 ffund ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W → Fun ⁡ iEdg ⁡ A
119 118 adantr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ A → iEdg ⁡ A ⁡ i ∈ ran ⁡ iEdg ⁡ A
122 29 raleqi ⊢ ∀ e ∈ E f e = g ⁡ e ↔ ∀ e ∈ ran ⁡ iEdg ⁡ A f e = g ⁡ e
123 122 biimpi ⊢ ∀ e ∈ E f e = g ⁡ e → ∀ e ∈ ran ⁡ iEdg ⁡ A f e = g ⁡ e
124 123 ad2antll ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → ∀ e ∈ ran ⁡ iEdg ⁡ A f e = g ⁡ e
125 124 adantr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ A → ∀ e ∈ ran ⁡ iEdg ⁡ A f e = g ⁡ e
126 imaeq2 ⊢ e = iEdg ⁡ A ⁡ i → f e = f iEdg ⁡ A ⁡ i
127 fveq2 ⊢ e = iEdg ⁡ A ⁡ i → g ⁡ e = g ⁡ iEdg ⁡ A ⁡ i
128 126 127 eqeq12d ⊢ e = iEdg ⁡ A ⁡ i → f e = g ⁡ e ↔ f iEdg ⁡ A ⁡ i = g ⁡ iEdg ⁡ A ⁡ i
129 128 rspccva ⊢ ∀ e ∈ ran ⁡ iEdg ⁡ A f e = g ⁡ e ∧ iEdg ⁡ A ⁡ i ∈ ran ⁡ iEdg ⁡ A → f iEdg ⁡ A ⁡ i = g ⁡ iEdg ⁡ A ⁡ i
130 125 129 sylan ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ A ∧ iEdg ⁡ A ⁡ i ∈ ran ⁡ iEdg ⁡ A → f iEdg ⁡ 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 onto W → iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ E
135 f1ofn ⊢ g : E ⟶ 1-1 onto K → g Fn E
136 135 adantr ⊢ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → g Fn E
137 134 136 anim12ci ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → g Fn E ∧ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ E
138 137 ad2antrr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ A ∧ iEdg ⁡ A ⁡ i ∈ ran ⁡ iEdg ⁡ A → g Fn E ∧ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ E
139 fnfco ⊢ g Fn E ∧ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ E → g ∘ iEdg ⁡ A Fn dom ⁡ iEdg ⁡ A
140 138 139 syl ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ A ∧ iEdg ⁡ A ⁡ i ∈ ran ⁡ iEdg ⁡ A → g ∘ iEdg ⁡ A Fn dom ⁡ iEdg ⁡ A
141 simplr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ A ∧ iEdg ⁡ A ⁡ i ∈ ran ⁡ iEdg ⁡ A → i ∈ dom ⁡ iEdg ⁡ A
142 fvco2 ⊢ g ∘ iEdg ⁡ A Fn dom ⁡ 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 onto K → 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 onto K → 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 onto K → g : E ⟶ ran ⁡ iEdg ⁡ B
160 159 adantr ⊢ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → g : E ⟶ ran ⁡ iEdg ⁡ B
161 f1of ⊢ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto E → 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 onto W → 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → g ∘ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ ran ⁡ iEdg ⁡ B
166 165 anim1i ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 ffvelrn ⊢ 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ E
173 172 anim1i ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 onto K ↔ iEdg ⁡ B Fn dom ⁡ iEdg ⁡ B ∧ iEdg ⁡ B -1 Fn K
180 22 179 sylib ⊢ B ∈ USHGraph → iEdg ⁡ B Fn dom ⁡ iEdg ⁡ B ∧ iEdg ⁡ B -1 Fn K
181 180 simprd ⊢ B ∈ USHGraph → iEdg ⁡ B -1 Fn K
182 181 ad5antlr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ A ∧ iEdg ⁡ A ⁡ i ∈ ran ⁡ iEdg ⁡ A → iEdg ⁡ B -1 Fn K
183 156 adantr ⊢ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → g : E ⟶ K
184 134 183 anim12ci ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → g : E ⟶ K ∧ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ E
185 184 ad2antrr ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ A ∧ iEdg ⁡ A ⁡ i ∈ ran ⁡ iEdg ⁡ A → g ∘ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ K
188 fnfco ⊢ iEdg ⁡ B -1 Fn K ∧ g ∘ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ K → iEdg ⁡ B -1 ∘ g ∘ iEdg ⁡ A Fn dom ⁡ iEdg ⁡ A
189 182 187 188 syl2anc ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ A ∧ iEdg ⁡ A ⁡ i ∈ ran ⁡ iEdg ⁡ A → iEdg ⁡ B -1 ∘ g ∘ iEdg ⁡ A Fn dom ⁡ iEdg ⁡ A
190 fvco2 ⊢ iEdg ⁡ B -1 ∘ g ∘ iEdg ⁡ A Fn dom ⁡ 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = 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 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ A ∧ iEdg ⁡ A ⁡ i ∈ ran ⁡ iEdg ⁡ A → f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ iEdg ⁡ B -1 ∘ g ∘ iEdg ⁡ A ⁡ i
193 121 192 mpdan ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e ∧ i ∈ dom ⁡ iEdg ⁡ A → f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ iEdg ⁡ B -1 ∘ g ∘ iEdg ⁡ A ⁡ i
194 193 ralrimiva ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ iEdg ⁡ B -1 ∘ g ∘ iEdg ⁡ A ⁡ i
195 116 194 jca ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → iEdg ⁡ B -1 ∘ g ∘ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ 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 onto dom ⁡ iEdg ⁡ B ↔ iEdg ⁡ B -1 ∘ g ∘ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ 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 → f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i ↔ f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ iEdg ⁡ B -1 ∘ g ∘ iEdg ⁡ A ⁡ i
200 199 ralbidv ⊢ h = iEdg ⁡ B -1 ∘ g ∘ iEdg ⁡ A → ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i ↔ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ 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 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i ↔ iEdg ⁡ B -1 ∘ g ∘ iEdg ⁡ A : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ iEdg ⁡ B -1 ∘ g ∘ iEdg ⁡ A ⁡ i
202 104 195 201 spcedv ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W ∧ g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → ∃ h h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i
203 202 ex ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W → g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → ∃ h h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i
204 203 exlimdv ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W → ∃ g g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e → ∃ h h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i
205 99 204 impbid ⊢ A ∈ USHGraph ∧ B ∈ USHGraph ∧ f : V ⟶ 1-1 onto W → ∃ h h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i ↔ ∃ g g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e
206 205 pm5.32da ⊢ A ∈ USHGraph ∧ B ∈ USHGraph → f : V ⟶ 1-1 onto W ∧ ∃ h h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i ↔ f : V ⟶ 1-1 onto W ∧ ∃ g g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e
207 206 exbidv ⊢ A ∈ USHGraph ∧ B ∈ USHGraph → ∃ f f : V ⟶ 1-1 onto W ∧ ∃ h h : dom ⁡ iEdg ⁡ A ⟶ 1-1 onto dom ⁡ iEdg ⁡ B ∧ ∀ i ∈ dom ⁡ iEdg ⁡ A f iEdg ⁡ A ⁡ i = iEdg ⁡ B ⁡ h ⁡ i ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∃ g g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e
208 7 207 bitrd ⊢ A ∈ USHGraph ∧ B ∈ USHGraph → A IsomGr B ↔ ∃ f f : V ⟶ 1-1 onto W ∧ ∃ g g : E ⟶ 1-1 onto K ∧ ∀ e ∈ E f e = g ⁡ e