# Metamath Proof Explorer

## Theorem isomgrtrlem

Description: Lemma for isomgrtr . (Contributed by AV, 5-Dec-2022)

Ref Expression
Assertion isomgrtrlem ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶𝑋 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ∧ ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) ) ) → ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ( 𝑤𝑔 ) ‘ 𝑗 ) ) )

### Proof

Step Hyp Ref Expression
1 imaco ( ( 𝑣𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( 𝑣 “ ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) )
2 1 a1i ( ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶𝑋 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ∧ ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( 𝑣𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( 𝑣 “ ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) ) )
3 fveq2 ( 𝑖 = 𝑗 → ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) = ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) )
4 3 imaeq2d ( 𝑖 = 𝑗 → ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) )
5 2fveq3 ( 𝑖 = 𝑗 → ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑗 ) ) )
6 4 5 eqeq12d ( 𝑖 = 𝑗 → ( ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ↔ ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑗 ) ) ) )
7 6 rspccv ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) → ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑗 ) ) ) )
8 7 adantl ( ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) → ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑗 ) ) ) )
9 8 ad2antlr ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶𝑋 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ∧ ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) ) ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) → ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑗 ) ) ) )
10 9 imp ( ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶𝑋 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ∧ ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑗 ) ) )
11 10 imaeq2d ( ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶𝑋 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ∧ ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( 𝑣 “ ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) ) = ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑗 ) ) ) )
12 simplrr ( ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶𝑋 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ∧ ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ) → ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) )
13 f1of ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) → 𝑔 : dom ( iEdg ‘ 𝐴 ) ⟶ dom ( iEdg ‘ 𝐵 ) )
14 ffvelrn ( ( 𝑔 : dom ( iEdg ‘ 𝐴 ) ⟶ dom ( iEdg ‘ 𝐵 ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( 𝑔𝑗 ) ∈ dom ( iEdg ‘ 𝐵 ) )
15 14 ex ( 𝑔 : dom ( iEdg ‘ 𝐴 ) ⟶ dom ( iEdg ‘ 𝐵 ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) → ( 𝑔𝑗 ) ∈ dom ( iEdg ‘ 𝐵 ) ) )
16 13 15 syl ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) → ( 𝑔𝑗 ) ∈ dom ( iEdg ‘ 𝐵 ) ) )
17 16 adantr ( ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) → ( 𝑔𝑗 ) ∈ dom ( iEdg ‘ 𝐵 ) ) )
18 17 ad2antlr ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶𝑋 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ∧ ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) ) ) → ( 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) → ( 𝑔𝑗 ) ∈ dom ( iEdg ‘ 𝐵 ) ) )
19 18 imp ( ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶𝑋 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ∧ ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( 𝑔𝑗 ) ∈ dom ( iEdg ‘ 𝐵 ) )
20 fveq2 ( 𝑘 = ( 𝑔𝑗 ) → ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑗 ) ) )
21 20 imaeq2d ( 𝑘 = ( 𝑔𝑗 ) → ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑗 ) ) ) )
22 2fveq3 ( 𝑘 = ( 𝑔𝑗 ) → ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ ( 𝑔𝑗 ) ) ) )
23 21 22 eqeq12d ( 𝑘 = ( 𝑔𝑗 ) → ( ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) ↔ ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑗 ) ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ ( 𝑔𝑗 ) ) ) ) )
24 23 rspccv ( ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) → ( ( 𝑔𝑗 ) ∈ dom ( iEdg ‘ 𝐵 ) → ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑗 ) ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ ( 𝑔𝑗 ) ) ) ) )
25 12 19 24 sylc ( ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶𝑋 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ∧ ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑗 ) ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ ( 𝑔𝑗 ) ) ) )
26 11 25 eqtrd ( ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶𝑋 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ∧ ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( 𝑣 “ ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ ( 𝑔𝑗 ) ) ) )
27 f1ofn ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) → 𝑔 Fn dom ( iEdg ‘ 𝐴 ) )
28 27 adantr ( ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) → 𝑔 Fn dom ( iEdg ‘ 𝐴 ) )
29 28 ad2antlr ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶𝑋 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ∧ ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) ) ) → 𝑔 Fn dom ( iEdg ‘ 𝐴 ) )
30 fvco2 ( ( 𝑔 Fn dom ( iEdg ‘ 𝐴 ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( 𝑤𝑔 ) ‘ 𝑗 ) = ( 𝑤 ‘ ( 𝑔𝑗 ) ) )
31 29 30 sylan ( ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶𝑋 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ∧ ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( 𝑤𝑔 ) ‘ 𝑗 ) = ( 𝑤 ‘ ( 𝑔𝑗 ) ) )
32 31 eqcomd ( ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶𝑋 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ∧ ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( 𝑤 ‘ ( 𝑔𝑗 ) ) = ( ( 𝑤𝑔 ) ‘ 𝑗 ) )
33 32 fveq2d ( ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶𝑋 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ∧ ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ ( 𝑔𝑗 ) ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ( 𝑤𝑔 ) ‘ 𝑗 ) ) )
34 2 26 33 3eqtrd ( ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶𝑋 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ∧ ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) ) ) ∧ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ) → ( ( 𝑣𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ( 𝑤𝑔 ) ‘ 𝑗 ) ) )
35 34 ralrimiva ( ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶𝑋 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ) ∧ ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔𝑖 ) ) ) ) ∧ ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤𝑘 ) ) ) ) → ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ( 𝑤𝑔 ) ‘ 𝑗 ) ) )