Metamath Proof Explorer


Theorem isomushgr

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

Ref Expression
Hypotheses isomushgr.v 𝑉 = ( Vtx ‘ 𝐴 )
isomushgr.w 𝑊 = ( Vtx ‘ 𝐵 )
isomushgr.e 𝐸 = ( Edg ‘ 𝐴 )
isomushgr.k 𝐾 = ( Edg ‘ 𝐵 )
Assertion isomushgr ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) → ( 𝐴 IsomGr 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉1-1-onto𝑊 ∧ ∃ 𝑔 ( 𝑔 : 𝐸1-1-onto𝐾 ∧ ∀ 𝑒𝐸 ( 𝑓𝑒 ) = ( 𝑔𝑒 ) ) ) ) )

Proof

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