Metamath Proof Explorer

Theorem isomgrtr

Description: The isomorphy relation is transitive for hypergraphs. (Contributed by AV, 5-Dec-2022)

Ref Expression
Assertion isomgrtr ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 IsomGr 𝐵 ∧ 𝐵 IsomGr 𝐶 ) → 𝐴 IsomGr 𝐶 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ( Vtx ‘ 𝐴 ) = ( Vtx ‘ 𝐴 )
2 eqid ⊢ ( Vtx ‘ 𝐵 ) = ( Vtx ‘ 𝐵 )
3 eqid ⊢ ( iEdg ‘ 𝐴 ) = ( iEdg ‘ 𝐴 )
4 eqid ⊢ ( iEdg ‘ 𝐵 ) = ( iEdg ‘ 𝐵 )
5 1 2 3 4 isomgr ⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ) → ( 𝐴 IsomGr 𝐵 ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
6 5 3adant3 ⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 IsomGr 𝐵 ↔ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
7 eqid ⊢ ( Vtx ‘ 𝐶 ) = ( Vtx ‘ 𝐶 )
8 eqid ⊢ ( iEdg ‘ 𝐶 ) = ( iEdg ‘ 𝐶 )
9 2 7 4 8 isomgr ⊢ ( ( 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 IsomGr 𝐶 ↔ ∃ 𝑣 ( 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ 𝑤 ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ 𝑘 ) ) ) ) ) )
10 9 3adant1 ⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) → ( 𝐵 IsomGr 𝐶 ↔ ∃ 𝑣 ( 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ 𝑤 ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ 𝑘 ) ) ) ) ) )
11 6 10 anbi12d ⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 IsomGr 𝐵 ∧ 𝐵 IsomGr 𝐶 ) ↔ ( ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ∧ ∃ 𝑣 ( 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ 𝑤 ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ 𝑘 ) ) ) ) ) ) )
12 vex ⊢ 𝑣 ∈ V
13 vex ⊢ 𝑓 ∈ V
14 12 13 coex ⊢ ( 𝑣 ∘ 𝑓 ) ∈ V
15 14 a1i ⊢ ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ 𝑤 ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ 𝑘 ) ) ) ) ) → ( 𝑣 ∘ 𝑓 ) ∈ V )
16 simpl ⊢ ( ( 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ 𝑤 ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ 𝑘 ) ) ) ) → 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) )
17 simprl ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) → 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) )
18 f1oco ⊢ ( ( 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ) → ( 𝑣 ∘ 𝑓 ) : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) )
19 16 17 18 syl2anr ⊢ ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ 𝑤 ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ 𝑘 ) ) ) ) ) → ( 𝑣 ∘ 𝑓 ) : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) )
20 vex ⊢ 𝑤 ∈ V
21 vex ⊢ 𝑔 ∈ V
22 20 21 coex ⊢ ( 𝑤 ∘ 𝑔 ) ∈ V
23 22 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 ‘ 𝐶 ) ‘ ( 𝑤 ‘ 𝑘 ) ) ) ) → ( 𝑤 ∘ 𝑔 ) ∈ V )
24 simpl ⊢ ( ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ 𝑘 ) ) ) → 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) )
25 simprl ⊢ ( ( ( ( 𝐴 ∈ 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 ‘ 𝐵 ) )
26 f1oco ⊢ ( ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ) → ( 𝑤 ∘ 𝑔 ) : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) )
27 24 25 26 syl2anr ⊢ ( ( ( ( ( 𝐴 ∈ 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 ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) )
28 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 ‘ 𝐶 ) ‘ ( ( 𝑤 ∘ 𝑔 ) ‘ 𝑗 ) ) )
29 27 28 jca ⊢ ( ( ( ( ( 𝐴 ∈ 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 ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ( 𝑤 ∘ 𝑔 ) ‘ 𝑗 ) ) ) )
30 f1oeq1 ⊢ ( ℎ = ( 𝑤 ∘ 𝑔 ) → ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ↔ ( 𝑤 ∘ 𝑔 ) : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ) )
31 fveq1 ⊢ ( ℎ = ( 𝑤 ∘ 𝑔 ) → ( ℎ ‘ 𝑗 ) = ( ( 𝑤 ∘ 𝑔 ) ‘ 𝑗 ) )
32 31 fveq2d ⊢ ( ℎ = ( 𝑤 ∘ 𝑔 ) → ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ( 𝑤 ∘ 𝑔 ) ‘ 𝑗 ) ) )
33 32 eqeq2d ⊢ ( ℎ = ( 𝑤 ∘ 𝑔 ) → ( ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ↔ ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ( 𝑤 ∘ 𝑔 ) ‘ 𝑗 ) ) ) )
34 33 ralbidv ⊢ ( ℎ = ( 𝑤 ∘ 𝑔 ) → ( ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ( 𝑤 ∘ 𝑔 ) ‘ 𝑗 ) ) ) )
35 30 34 anbi12d ⊢ ( ℎ = ( 𝑤 ∘ 𝑔 ) → ( ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ↔ ( ( 𝑤 ∘ 𝑔 ) : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ( 𝑤 ∘ 𝑔 ) ‘ 𝑗 ) ) ) ) )
36 23 29 35 spcedv ⊢ ( ( ( ( ( 𝐴 ∈ 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 ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) )
37 36 ex ⊢ ( ( ( ( 𝐴 ∈ 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 ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ) )
38 37 exlimdv ⊢ ( ( ( ( 𝐴 ∈ 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 ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ) )
39 38 ex ⊢ ( ( ( 𝐴 ∈ 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 ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ) ) )
40 39 exlimdv ⊢ ( ( ( 𝐴 ∈ 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 ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ) ) )
41 40 3exp ⊢ ( ( 𝐴 ∈ 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 ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ) ) ) ) )
42 41 com34 ⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) → ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) → ( ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) → ( 𝑣 : ( 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 ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ) ) ) ) )
43 42 imp32 ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) → ( 𝑣 : ( 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 ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ) ) )
44 43 imp32 ⊢ ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑣 : ( 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 ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) )
45 19 44 jca ⊢ ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ 𝑤 ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ 𝑘 ) ) ) ) ) → ( ( 𝑣 ∘ 𝑓 ) : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ ℎ ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ) )
46 f1oeq1 ⊢ ( 𝑒 = ( 𝑣 ∘ 𝑓 ) → ( 𝑒 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ↔ ( 𝑣 ∘ 𝑓 ) : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ) )
47 imaeq1 ⊢ ( 𝑒 = ( 𝑣 ∘ 𝑓 ) → ( 𝑒 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) )
48 47 eqeq1d ⊢ ( 𝑒 = ( 𝑣 ∘ 𝑓 ) → ( ( 𝑒 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ↔ ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) )
49 48 ralbidv ⊢ ( 𝑒 = ( 𝑣 ∘ 𝑓 ) → ( ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑒 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ↔ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) )
50 49 anbi2d ⊢ ( 𝑒 = ( 𝑣 ∘ 𝑓 ) → ( ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑒 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ↔ ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ) )
51 50 exbidv ⊢ ( 𝑒 = ( 𝑣 ∘ 𝑓 ) → ( ∃ ℎ ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑒 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ↔ ∃ ℎ ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ) )
52 46 51 anbi12d ⊢ ( 𝑒 = ( 𝑣 ∘ 𝑓 ) → ( ( 𝑒 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ ℎ ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑒 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ) ↔ ( ( 𝑣 ∘ 𝑓 ) : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ ℎ ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( ( 𝑣 ∘ 𝑓 ) “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ) ) )
53 15 45 52 spcedv ⊢ ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ 𝑤 ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ 𝑘 ) ) ) ) ) → ∃ 𝑒 ( 𝑒 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ ℎ ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑒 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ) )
54 1 7 3 8 isomgr ⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 IsomGr 𝐶 ↔ ∃ 𝑒 ( 𝑒 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ ℎ ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑒 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ) ) )
55 54 3adant2 ⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 IsomGr 𝐶 ↔ ∃ 𝑒 ( 𝑒 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ ℎ ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑒 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ) ) )
56 55 ad2antrr ⊢ ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ 𝑤 ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ 𝑘 ) ) ) ) ) → ( 𝐴 IsomGr 𝐶 ↔ ∃ 𝑒 ( 𝑒 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ ℎ ( ℎ : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑗 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑒 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑗 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( ℎ ‘ 𝑗 ) ) ) ) ) )
57 53 56 mpbird ⊢ ( ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) ∧ ( 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ 𝑤 ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ 𝑘 ) ) ) ) ) → 𝐴 IsomGr 𝐶 )
58 57 ex ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) → ( ( 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ 𝑤 ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ 𝑘 ) ) ) ) → 𝐴 IsomGr 𝐶 ) )
59 58 exlimdv ⊢ ( ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) ∧ ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) → ( ∃ 𝑣 ( 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ 𝑤 ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ 𝑘 ) ) ) ) → 𝐴 IsomGr 𝐶 ) )
60 59 ex ⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) → ( ∃ 𝑣 ( 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ 𝑤 ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ 𝑘 ) ) ) ) → 𝐴 IsomGr 𝐶 ) ) )
61 60 exlimdv ⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) → ( ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) → ( ∃ 𝑣 ( 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ 𝑤 ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ 𝑘 ) ) ) ) → 𝐴 IsomGr 𝐶 ) ) )
62 61 impd ⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) → ( ( ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝐴 ) –1-1-onto→ ( Vtx ‘ 𝐵 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝐴 ) –1-1-onto→ dom ( iEdg ‘ 𝐵 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐴 ) ( 𝑓 “ ( ( iEdg ‘ 𝐴 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐵 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ∧ ∃ 𝑣 ( 𝑣 : ( Vtx ‘ 𝐵 ) –1-1-onto→ ( Vtx ‘ 𝐶 ) ∧ ∃ 𝑤 ( 𝑤 : dom ( iEdg ‘ 𝐵 ) –1-1-onto→ dom ( iEdg ‘ 𝐶 ) ∧ ∀ 𝑘 ∈ dom ( iEdg ‘ 𝐵 ) ( 𝑣 “ ( ( iEdg ‘ 𝐵 ) ‘ 𝑘 ) ) = ( ( iEdg ‘ 𝐶 ) ‘ ( 𝑤 ‘ 𝑘 ) ) ) ) ) → 𝐴 IsomGr 𝐶 ) )
63 11 62 sylbid ⊢ ( ( 𝐴 ∈ UHGraph ∧ 𝐵 ∈ UHGraph ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 IsomGr 𝐵 ∧ 𝐵 IsomGr 𝐶 ) → 𝐴 IsomGr 𝐶 ) )