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 ‘ 𝐶 ) ‘ ( ( 𝑤 ∘ 𝑔 ) ‘ 𝑗 ) ) )