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

Metamath Proof Explorer

Theorem grimcnv

Description: The converse of a graph isomorphism is a graph isomorphism. (Contributed by AV, 1-May-2025)

Ref Expression
Assertion grimcnv ( 𝑆 ∈ UHGraph → ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → ◡ 𝐹 ∈ ( 𝑇 GraphIso 𝑆 ) ) )

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 grimprop ⊢ ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) )
6 5 adantl ⊢ ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) → ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) )
7 f1ocnv ⊢ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) → ◡ 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) )
8 7 ad2antrl ⊢ ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ) → ◡ 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) )
9 vex ⊢ 𝑗 ∈ V
10 cnvexg ⊢ ( 𝑗 ∈ V → ◡ 𝑗 ∈ V )
11 9 10 mp1i ⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) → ◡ 𝑗 ∈ V )
12 f1ocnv ⊢ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) → ◡ 𝑗 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) )
13 12 ad2antrl ⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) → ◡ 𝑗 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) )
14 f1ofo ⊢ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) → 𝑗 : dom ( iEdg ‘ 𝑆 ) –onto→ dom ( iEdg ‘ 𝑇 ) )
15 14 ad2antrl ⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) → 𝑗 : dom ( iEdg ‘ 𝑆 ) –onto→ dom ( iEdg ‘ 𝑇 ) )
16 foelcdmi ⊢ ( ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –onto→ dom ( iEdg ‘ 𝑇 ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ) → ∃ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( 𝑗 ‘ 𝑦 ) = 𝑥 )
17 15 16 sylan ⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ) → ∃ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( 𝑗 ‘ 𝑦 ) = 𝑥 )
18 2fveq3 ⊢ ( 𝑖 = 𝑦 → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) )
19 fveq2 ⊢ ( 𝑖 = 𝑦 → ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) = ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) )
20 19 imaeq2d ⊢ ( 𝑖 = 𝑦 → ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) )
21 18 20 eqeq12d ⊢ ( 𝑖 = 𝑦 → ( ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ↔ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) )
22 21 rspcv ⊢ ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) )
23 22 adantl ⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) )
24 f1ocnvfv1 ⊢ ( ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) = 𝑦 )
25 24 ad4ant23 ⊢ ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) = 𝑦 )
26 25 fveq2d ⊢ ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) )
27 f1of1 ⊢ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) → 𝐹 : ( Vtx ‘ 𝑆 ) –1-1→ ( Vtx ‘ 𝑇 ) )
28 27 ad2antlr ⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) → 𝐹 : ( Vtx ‘ 𝑆 ) –1-1→ ( Vtx ‘ 𝑇 ) )
29 1 3 uhgrss ⊢ ( ( 𝑆 ∈ UHGraph ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ⊆ ( Vtx ‘ 𝑆 ) )
30 29 ad5ant15 ⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ⊆ ( Vtx ‘ 𝑆 ) )
31 f1imacnv ⊢ ( ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1→ ( Vtx ‘ 𝑇 ) ∧ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ⊆ ( Vtx ‘ 𝑆 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) = ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) )
32 28 30 31 syl2an2r ⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) = ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) )
33 32 eqcomd ⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) = ( ◡ 𝐹 “ ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) )
34 33 adantr ⊢ ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) = ( ◡ 𝐹 “ ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) )
35 26 34 eqtrd ⊢ ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) )
36 35 adantlr ⊢ ( ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) )
37 simplr ⊢ ( ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) )
38 37 eqcomd ⊢ ( ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) )
39 38 imaeq2d ⊢ ( ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ◡ 𝐹 “ ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) )
40 36 39 eqtrd ⊢ ( ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) ∧ ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) )
41 40 ex ⊢ ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) ∧ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) ) → ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) )
42 41 ex ⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑦 ) ) → ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) ) )
43 23 42 syld ⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) ) )
44 43 ex ⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) ) ) )
45 44 com23 ⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ) → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) ) ) )
46 45 impr ⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) ) )
47 eleq1 ⊢ ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) ↔ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ) )
48 2fveq3 ⊢ ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) )
49 fveq2 ⊢ ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) = ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) )
50 49 imaeq2d ⊢ ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) )
51 48 50 eqeq12d ⊢ ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ↔ ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) )
52 47 51 imbi12d ⊢ ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) ↔ ( 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) )
53 52 imbi2d ⊢ ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( 𝑗 ‘ 𝑦 ) ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ ( 𝑗 ‘ 𝑦 ) ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑦 ) ) ) ) ) ↔ ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) )
54 46 53 syl5ibcom ⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) → ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) )
55 54 com24 ⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) → ( 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) → ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) )
56 55 imp31 ⊢ ( ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) )
57 56 rexlimdva ⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ∃ 𝑦 ∈ dom ( iEdg ‘ 𝑆 ) ( 𝑗 ‘ 𝑦 ) = 𝑥 → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) )
58 17 57 mpd ⊢ ( ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ∧ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) )
59 58 ralrimiva ⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ) ∧ ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) → ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) )
60 13 59 jca ⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( 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 ‘ 𝑇 ) ‘ 𝑥 ) ) ) )
61 f1oeq1 ⊢ ( 𝑓 = ◡ 𝑗 → ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ↔ ◡ 𝑗 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ) )
62 fveq1 ⊢ ( 𝑓 = ◡ 𝑗 → ( 𝑓 ‘ 𝑥 ) = ( ◡ 𝑗 ‘ 𝑥 ) )
63 62 fveqeq2d ⊢ ( 𝑓 = ◡ 𝑗 → ( ( ( iEdg ‘ 𝑆 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ↔ ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) )
64 63 ralbidv ⊢ ( 𝑓 = ◡ 𝑗 → ( ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑆 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) )
65 61 64 anbi12d ⊢ ( 𝑓 = ◡ 𝑗 → ( ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑆 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ↔ ( ◡ 𝑗 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑆 ) ‘ ( ◡ 𝑗 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) )
66 11 60 65 spcedv ⊢ ( ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( 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 ‘ 𝑇 ) ‘ 𝑥 ) ) ) )
67 66 ex ⊢ ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( 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 ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) )
68 67 exlimdv ⊢ ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ 𝐹 : ( 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 ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) )
69 68 impr ⊢ ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ ( 𝐹 : ( 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 ‘ 𝑇 ) ‘ 𝑥 ) ) ) )
70 grimdmrel ⊢ Rel dom GraphIso
71 70 ovrcl ⊢ ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → ( 𝑆 ∈ V ∧ 𝑇 ∈ V ) )
72 71 simprd ⊢ ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → 𝑇 ∈ V )
73 71 simpld ⊢ ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → 𝑆 ∈ V )
74 cnvexg ⊢ ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → ◡ 𝐹 ∈ V )
75 2 1 4 3 isgrim ⊢ ( ( 𝑇 ∈ V ∧ 𝑆 ∈ V ∧ ◡ 𝐹 ∈ V ) → ( ◡ 𝐹 ∈ ( 𝑇 GraphIso 𝑆 ) ↔ ( ◡ 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∃ 𝑓 ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑆 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) )
76 72 73 74 75 syl3anc ⊢ ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → ( ◡ 𝐹 ∈ ( 𝑇 GraphIso 𝑆 ) ↔ ( ◡ 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∃ 𝑓 ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑆 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) )
77 76 ad2antlr ⊢ ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ) → ( ◡ 𝐹 ∈ ( 𝑇 GraphIso 𝑆 ) ↔ ( ◡ 𝐹 : ( Vtx ‘ 𝑇 ) –1-1-onto→ ( Vtx ‘ 𝑆 ) ∧ ∃ 𝑓 ( 𝑓 : dom ( iEdg ‘ 𝑇 ) –1-1-onto→ dom ( iEdg ‘ 𝑆 ) ∧ ∀ 𝑥 ∈ dom ( iEdg ‘ 𝑇 ) ( ( iEdg ‘ 𝑆 ) ‘ ( 𝑓 ‘ 𝑥 ) ) = ( ◡ 𝐹 “ ( ( iEdg ‘ 𝑇 ) ‘ 𝑥 ) ) ) ) ) )
78 8 69 77 mpbir2and ⊢ ( ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) ∧ ( 𝐹 : ( Vtx ‘ 𝑆 ) –1-1-onto→ ( Vtx ‘ 𝑇 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝑆 ) –1-1-onto→ dom ( iEdg ‘ 𝑇 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑆 ) ( ( iEdg ‘ 𝑇 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝑆 ) ‘ 𝑖 ) ) ) ) ) → ◡ 𝐹 ∈ ( 𝑇 GraphIso 𝑆 ) )
79 6 78 mpdan ⊢ ( ( 𝑆 ∈ UHGraph ∧ 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) ) → ◡ 𝐹 ∈ ( 𝑇 GraphIso 𝑆 ) )
80 79 ex ⊢ ( 𝑆 ∈ UHGraph → ( 𝐹 ∈ ( 𝑆 GraphIso 𝑇 ) → ◡ 𝐹 ∈ ( 𝑇 GraphIso 𝑆 ) ) )