This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem gricushgr

Description: The "is isomorphic to" relation for two simple hypergraphs. (Contributed by AV, 28-Nov-2022)

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

Proof

Step Hyp Ref Expression
1 gricushgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐴 )
2 gricushgr.w ⊢ 𝑊 = ( Vtx ‘ 𝐵 )
3 gricushgr.e ⊢ 𝐸 = ( Edg ‘ 𝐴 )
4 gricushgr.k ⊢ 𝐾 = ( Edg ‘ 𝐵 )
5 eqid ⊢ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐴 )
6 eqid ⊢ ( iEdg ‘ 𝐵 ) = ( iEdg ‘ 𝐵 )
7 1 2 5 6 dfgric2 ⊢ ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) → ( 𝐴 ≃𝑔𝑟 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –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 ffvelcdmda ⊢ ( ( ( ( ( 𝐴 ∈ 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 eqtr2id ⊢ ( ( ( ( ( 𝐴 ∈ 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 biimtrid ⊢ ( ( ( ( 𝐴 ∈ 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 simplr ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) )
142 fvco2 ⊢ ( ( ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) Fn dom ( iEdg ‘ 𝐴 ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( ( I ↾ ran ( iEdg ‘ 𝐵 ) ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ‘ 𝑖 ) = ( ( I ↾ ran ( iEdg ‘ 𝐵 ) ) ‘ ( ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ) )
143 140 141 142 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ( ( ( I ↾ ran ( iEdg ‘ 𝐵 ) ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ‘ 𝑖 ) = ( ( I ↾ ran ( iEdg ‘ 𝐵 ) ) ‘ ( ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ) )
144 f1of ⊢ ( ( iEdg ‘ 𝐵 ) : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ 𝐾 → ( iEdg ‘ 𝐵 ) : dom ( iEdg ‘ 𝐵 ) ⟶ 𝐾 )
145 22 144 syl ⊢ ( 𝐵 ∈ USHGraph → ( iEdg ‘ 𝐵 ) : dom ( iEdg ‘ 𝐵 ) ⟶ 𝐾 )
146 145 ffund ⊢ ( 𝐵 ∈ USHGraph → Fun ( iEdg ‘ 𝐵 ) )
147 funcocnv2 ⊢ ( Fun ( iEdg ‘ 𝐵 ) → ( ( iEdg ‘ 𝐵 ) ∘ ◡ ( iEdg ‘ 𝐵 ) ) = ( I ↾ ran ( iEdg ‘ 𝐵 ) ) )
148 146 147 syl ⊢ ( 𝐵 ∈ USHGraph → ( ( iEdg ‘ 𝐵 ) ∘ ◡ ( iEdg ‘ 𝐵 ) ) = ( I ↾ ran ( iEdg ‘ 𝐵 ) ) )
149 148 eqcomd ⊢ ( 𝐵 ∈ USHGraph → ( I ↾ ran ( iEdg ‘ 𝐵 ) ) = ( ( iEdg ‘ 𝐵 ) ∘ ◡ ( iEdg ‘ 𝐵 ) ) )
150 149 ad5antlr ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ( I ↾ ran ( iEdg ‘ 𝐵 ) ) = ( ( iEdg ‘ 𝐵 ) ∘ ◡ ( iEdg ‘ 𝐵 ) ) )
151 150 coeq1d ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ( ( I ↾ ran ( iEdg ‘ 𝐵 ) ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) = ( ( ( iEdg ‘ 𝐵 ) ∘ ◡ ( iEdg ‘ 𝐵 ) ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) )
152 151 fveq1d ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ( ( ( I ↾ ran ( iEdg ‘ 𝐵 ) ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ‘ 𝑖 ) = ( ( ( ( iEdg ‘ 𝐵 ) ∘ ◡ ( iEdg ‘ 𝐵 ) ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ‘ 𝑖 ) )
153 coass ⊢ ( ( ( iEdg ‘ 𝐵 ) ∘ ◡ ( iEdg ‘ 𝐵 ) ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) = ( ( iEdg ‘ 𝐵 ) ∘ ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) )
154 153 fveq1i ⊢ ( ( ( ( iEdg ‘ 𝐵 ) ∘ ◡ ( iEdg ‘ 𝐵 ) ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ‘ 𝑖 ) = ( ( ( iEdg ‘ 𝐵 ) ∘ ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ) ‘ 𝑖 )
155 152 154 eqtrdi ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ( ( ( I ↾ ran ( iEdg ‘ 𝐵 ) ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ‘ 𝑖 ) = ( ( ( iEdg ‘ 𝐵 ) ∘ ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ) ‘ 𝑖 ) )
156 f1of ⊢ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 → 𝑔 : 𝐸 ⟶ 𝐾 )
157 eqid ⊢ 𝐸 = 𝐸
158 157 19 feq23i ⊢ ( 𝑔 : 𝐸 ⟶ 𝐾 ↔ 𝑔 : 𝐸 ⟶ ran ( iEdg ‘ 𝐵 ) )
159 156 158 sylib ⊢ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 → 𝑔 : 𝐸 ⟶ ran ( iEdg ‘ 𝐵 ) )
160 159 adantr ⊢ ( ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → 𝑔 : 𝐸 ⟶ ran ( iEdg ‘ 𝐵 ) )
161 f1of ⊢ ( ( iEdg ‘ 𝐴 ) : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ 𝐸 → ( iEdg ‘ 𝐴 ) : dom ( iEdg ‘ 𝐴 ) ⟶ 𝐸 )
162 32 161 syl ⊢ ( 𝐴 ∈ USHGraph → ( iEdg ‘ 𝐴 ) : dom ( iEdg ‘ 𝐴 ) ⟶ 𝐸 )
163 162 ad2antrr ⊢ ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) → ( iEdg ‘ 𝐴 ) : dom ( iEdg ‘ 𝐴 ) ⟶ 𝐸 )
164 fco ⊢ ( ( 𝑔 : 𝐸 ⟶ ran ( iEdg ‘ 𝐵 ) ∧ ( iEdg ‘ 𝐴 ) : dom ( iEdg ‘ 𝐴 ) ⟶ 𝐸 ) → ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) : dom ( iEdg ‘ 𝐴 ) ⟶ ran ( iEdg ‘ 𝐵 ) )
165 160 163 164 syl2anr ⊢ ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) : dom ( iEdg ‘ 𝐴 ) ⟶ ran ( iEdg ‘ 𝐵 ) )
166 165 anim1i ⊢ ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) : dom ( iEdg ‘ 𝐴 ) ⟶ ran ( iEdg ‘ 𝐵 ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) )
167 166 adantr ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ( ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) : dom ( iEdg ‘ 𝐴 ) ⟶ ran ( iEdg ‘ 𝐵 ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) )
168 ffvelcdm ⊢ ( ( ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) : dom ( iEdg ‘ 𝐴 ) ⟶ ran ( iEdg ‘ 𝐵 ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐵 ) )
169 167 168 syl ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ( ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐵 ) )
170 fvresi ⊢ ( ( ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐵 ) → ( ( I ↾ ran ( iEdg ‘ 𝐵 ) ) ‘ ( ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ) = ( ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) )
171 169 170 syl ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ( ( I ↾ ran ( iEdg ‘ 𝐵 ) ) ‘ ( ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ) = ( ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) )
172 162 ad3antrrr ⊢ ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( iEdg ‘ 𝐴 ) : dom ( iEdg ‘ 𝐴 ) ⟶ 𝐸 )
173 172 anim1i ⊢ ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( iEdg ‘ 𝐴 ) : dom ( iEdg ‘ 𝐴 ) ⟶ 𝐸 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) )
174 173 adantr ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ( ( iEdg ‘ 𝐴 ) : dom ( iEdg ‘ 𝐴 ) ⟶ 𝐸 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) )
175 fvco3 ⊢ ( ( ( iEdg ‘ 𝐴 ) : dom ( iEdg ‘ 𝐴 ) ⟶ 𝐸 ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) = ( 𝑔 ‘ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) )
176 174 175 syl ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ( ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) = ( 𝑔 ‘ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) )
177 171 176 eqtrd ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ( ( I ↾ ran ( iEdg ‘ 𝐵 ) ) ‘ ( ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ‘ 𝑖 ) ) = ( 𝑔 ‘ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) )
178 143 155 177 3eqtr3rd ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ( 𝑔 ‘ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( ( iEdg ‘ 𝐵 ) ∘ ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ) ‘ 𝑖 ) )
179 dff1o4 ⊢ ( ( iEdg ‘ 𝐵 ) : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ 𝐾 ↔ ( ( iEdg ‘ 𝐵 ) Fn dom ( iEdg ‘ 𝐵 ) ∧ ◡ ( iEdg ‘ 𝐵 ) Fn 𝐾 ) )
180 22 179 sylib ⊢ ( 𝐵 ∈ USHGraph → ( ( iEdg ‘ 𝐵 ) Fn dom ( iEdg ‘ 𝐵 ) ∧ ◡ ( iEdg ‘ 𝐵 ) Fn 𝐾 ) )
181 180 simprd ⊢ ( 𝐵 ∈ USHGraph → ◡ ( iEdg ‘ 𝐵 ) Fn 𝐾 )
182 181 ad5antlr ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ◡ ( iEdg ‘ 𝐵 ) Fn 𝐾 )
183 156 adantr ⊢ ( ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → 𝑔 : 𝐸 ⟶ 𝐾 )
184 134 183 anim12ci ⊢ ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( 𝑔 : 𝐸 ⟶ 𝐾 ∧ ( iEdg ‘ 𝐴 ) : dom ( iEdg ‘ 𝐴 ) ⟶ 𝐸 ) )
185 184 ad2antrr ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ( 𝑔 : 𝐸 ⟶ 𝐾 ∧ ( iEdg ‘ 𝐴 ) : dom ( iEdg ‘ 𝐴 ) ⟶ 𝐸 ) )
186 fco ⊢ ( ( 𝑔 : 𝐸 ⟶ 𝐾 ∧ ( iEdg ‘ 𝐴 ) : dom ( iEdg ‘ 𝐴 ) ⟶ 𝐸 ) → ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) : dom ( iEdg ‘ 𝐴 ) ⟶ 𝐾 )
187 185 186 syl ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) : dom ( iEdg ‘ 𝐴 ) ⟶ 𝐾 )
188 fnfco ⊢ ( ( ◡ ( iEdg ‘ 𝐵 ) Fn 𝐾 ∧ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) : dom ( iEdg ‘ 𝐴 ) ⟶ 𝐾 ) → ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) Fn dom ( iEdg ‘ 𝐴 ) )
189 182 187 188 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) Fn dom ( iEdg ‘ 𝐴 ) )
190 fvco2 ⊢ ( ( ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) Fn dom ( iEdg ‘ 𝐴 ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( ( iEdg ‘ 𝐵 ) ∘ ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ) ‘ 𝑖 ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ‘ 𝑖 ) ) )
191 189 141 190 syl2anc ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ( ( ( iEdg ‘ 𝐵 ) ∘ ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ) ‘ 𝑖 ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ‘ 𝑖 ) ) )
192 130 178 191 3eqtrd ⊢ ( ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) ∧ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ∈ ran ( iEdg ‘ 𝐴 ) ) → ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ‘ 𝑖 ) ) )
193 121 192 mpdan ⊢ ( ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ∧ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ‘ 𝑖 ) ) )
194 193 ralrimiva ⊢ ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ‘ 𝑖 ) ) )
195 116 194 jca ⊢ ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ‘ 𝑖 ) ) ) )
196 f1oeq1 ⊢ ( ℎ = ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) → ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ↔ ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ) )
197 fveq1 ⊢ ( ℎ = ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) → ( ℎ ‘ 𝑖 ) = ( ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ‘ 𝑖 ) )
198 197 fveq2d ⊢ ( ℎ = ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) → ( ( iEdg ‘ 𝐵 ) ‘ ( ℎ ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ‘ 𝑖 ) ) )
199 198 eqeq2d ⊢ ( ℎ = ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) → ( ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ℎ ‘ 𝑖 ) ) ↔ ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ‘ 𝑖 ) ) ) )
200 199 ralbidv ⊢ ( ℎ = ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ℎ ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ( ◡ ( iEdg ‘ 𝐵 ) ∘ ( 𝑔 ∘ ( iEdg ‘ 𝐴 ) ) ) ‘ 𝑖 ) ) ) )
201 196 200 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 ‘ 𝐴 ) ) ) ‘ 𝑖 ) ) ) ) )
202 104 195 201 spcedv ⊢ ( ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ∃ ℎ ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ℎ ‘ 𝑖 ) ) ) )
203 202 ex ⊢ ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) → ( ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → ∃ ℎ ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) )
204 203 exlimdv ⊢ ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) → ( ∃ 𝑔 ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → ∃ ℎ ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) )
205 99 204 impbid ⊢ ( ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) → ( ∃ ℎ ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ↔ ∃ 𝑔 ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) )
206 205 pm5.32da ⊢ ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) → ( ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ ℎ ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
207 206 exbidv ⊢ ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) → ( ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ ℎ ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( ℎ ‘ 𝑖 ) ) ) ) ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
208 7 207 bitrd ⊢ ( ( 𝐴 ∈ USHGraph ∧ 𝐵 ∈ USHGraph ) → ( 𝐴 ≃𝑔𝑟 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : 𝐸 –1-1-onto→ 𝐾 ∧ ∀ 𝑒 ∈ 𝐸 ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )