Metamath Proof Explorer

Theorem isgrim

Description: An isomorphism of graphs is a bijection between their vertices that preserves adjacency. (Contributed by AV, 19-Apr-2025)

Ref Expression
Hypotheses isgrim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isgrim.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
isgrim.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
isgrim.d ⊢ 𝐷 = ( iEdg ‘ 𝐻 )
Assertion isgrim ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑗 ( 𝑗 : dom 𝐸 –1-1-onto→ dom 𝐷 ∧ ∀ 𝑖 ∈ dom 𝐸 ( 𝐷 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐸 ‘ 𝑖 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isgrim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isgrim.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3 isgrim.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
4 isgrim.d ⊢ 𝐷 = ( iEdg ‘ 𝐻 )
5 df-grim ⊢ GraphIso = ( 𝑔 ∈ V , ℎ ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∃ 𝑗 [ ( iEdg ‘ 𝑔 ) / 𝑒 ] [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ) } )
6 elex ⊢ ( 𝐺 ∈ 𝑋 → 𝐺 ∈ V )
7 6 3ad2ant1 ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → 𝐺 ∈ V )
8 elex ⊢ ( 𝐻 ∈ 𝑌 → 𝐻 ∈ V )
9 8 3ad2ant2 ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → 𝐻 ∈ V )
10 f1of ⊢ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → 𝑓 : ( Vtx ‘ 𝐺 ) ⟶ ( Vtx ‘ 𝐻 ) )
11 fvex ⊢ ( Vtx ‘ 𝐻 ) ∈ V
12 fvex ⊢ ( Vtx ‘ 𝐺 ) ∈ V
13 11 12 elmap ⊢ ( 𝑓 ∈ ( ( Vtx ‘ 𝐻 ) ↑m ( Vtx ‘ 𝐺 ) ) ↔ 𝑓 : ( Vtx ‘ 𝐺 ) ⟶ ( Vtx ‘ 𝐻 ) )
14 10 13 sylibr ⊢ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) → 𝑓 ∈ ( ( Vtx ‘ 𝐻 ) ↑m ( Vtx ‘ 𝐺 ) ) )
15 14 adantr ⊢ ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) → 𝑓 ∈ ( ( Vtx ‘ 𝐻 ) ↑m ( Vtx ‘ 𝐺 ) ) )
16 ovex ⊢ ( ( Vtx ‘ 𝐻 ) ↑m ( Vtx ‘ 𝐺 ) ) ∈ V
17 15 16 abex ⊢ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) } ∈ V
18 17 a1i ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) } ∈ V )
19 eqidd ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → 𝑓 = 𝑓 )
20 fveq2 ⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
21 20 adantr ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
22 fveq2 ⊢ ( ℎ = 𝐻 → ( Vtx ‘ ℎ ) = ( Vtx ‘ 𝐻 ) )
23 22 adantl ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( Vtx ‘ ℎ ) = ( Vtx ‘ 𝐻 ) )
24 19 21 23 f1oeq123d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ↔ 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ) )
25 fvexd ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( iEdg ‘ 𝑔 ) ∈ V )
26 fveq2 ⊢ ( 𝑔 = 𝐺 → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) )
27 26 adantr ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) )
28 fvexd ⊢ ( ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) ∧ 𝑒 = ( iEdg ‘ 𝐺 ) ) → ( iEdg ‘ ℎ ) ∈ V )
29 fveq2 ⊢ ( ℎ = 𝐻 → ( iEdg ‘ ℎ ) = ( iEdg ‘ 𝐻 ) )
30 29 adantl ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( iEdg ‘ ℎ ) = ( iEdg ‘ 𝐻 ) )
31 30 adantr ⊢ ( ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) ∧ 𝑒 = ( iEdg ‘ 𝐺 ) ) → ( iEdg ‘ ℎ ) = ( iEdg ‘ 𝐻 ) )
32 eqidd ⊢ ( ( 𝑒 = ( iEdg ‘ 𝐺 ) ∧ 𝑑 = ( iEdg ‘ 𝐻 ) ) → 𝑗 = 𝑗 )
33 dmeq ⊢ ( 𝑒 = ( iEdg ‘ 𝐺 ) → dom 𝑒 = dom ( iEdg ‘ 𝐺 ) )
34 33 adantr ⊢ ( ( 𝑒 = ( iEdg ‘ 𝐺 ) ∧ 𝑑 = ( iEdg ‘ 𝐻 ) ) → dom 𝑒 = dom ( iEdg ‘ 𝐺 ) )
35 dmeq ⊢ ( 𝑑 = ( iEdg ‘ 𝐻 ) → dom 𝑑 = dom ( iEdg ‘ 𝐻 ) )
36 35 adantl ⊢ ( ( 𝑒 = ( iEdg ‘ 𝐺 ) ∧ 𝑑 = ( iEdg ‘ 𝐻 ) ) → dom 𝑑 = dom ( iEdg ‘ 𝐻 ) )
37 32 34 36 f1oeq123d ⊢ ( ( 𝑒 = ( iEdg ‘ 𝐺 ) ∧ 𝑑 = ( iEdg ‘ 𝐻 ) ) → ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ↔ 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ) )
38 fveq1 ⊢ ( 𝑑 = ( iEdg ‘ 𝐻 ) → ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) )
39 fveq1 ⊢ ( 𝑒 = ( iEdg ‘ 𝐺 ) → ( 𝑒 ‘ 𝑖 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
40 39 imaeq2d ⊢ ( 𝑒 = ( iEdg ‘ 𝐺 ) → ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
41 38 40 eqeqan12rd ⊢ ( ( 𝑒 = ( iEdg ‘ 𝐺 ) ∧ 𝑑 = ( iEdg ‘ 𝐻 ) ) → ( ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ↔ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
42 34 41 raleqbidv ⊢ ( ( 𝑒 = ( iEdg ‘ 𝐺 ) ∧ 𝑑 = ( iEdg ‘ 𝐻 ) ) → ( ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) )
43 37 42 anbi12d ⊢ ( ( 𝑒 = ( iEdg ‘ 𝐺 ) ∧ 𝑑 = ( iEdg ‘ 𝐻 ) ) → ( ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ↔ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
44 43 adantll ⊢ ( ( ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) ∧ 𝑒 = ( iEdg ‘ 𝐺 ) ) ∧ 𝑑 = ( iEdg ‘ 𝐻 ) ) → ( ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ↔ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
45 28 31 44 sbcied2 ⊢ ( ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) ∧ 𝑒 = ( iEdg ‘ 𝐺 ) ) → ( [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ↔ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
46 25 27 45 sbcied2 ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( [ ( iEdg ‘ 𝑔 ) / 𝑒 ] [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ↔ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
47 biidd ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ↔ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
48 46 47 bitrd ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( [ ( iEdg ‘ 𝑔 ) / 𝑒 ] [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ↔ ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
49 48 exbidv ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ∃ 𝑗 [ ( iEdg ‘ 𝑔 ) / 𝑒 ] [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ↔ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
50 24 49 anbi12d ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → ( ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∃ 𝑗 [ ( iEdg ‘ 𝑔 ) / 𝑒 ] [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ) ↔ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ) )
51 50 abbidv ⊢ ( ( 𝑔 = 𝐺 ∧ ℎ = 𝐻 ) → { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∃ 𝑗 [ ( iEdg ‘ 𝑔 ) / 𝑒 ] [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ) } = { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) } )
52 5 7 9 18 51 elovmpod ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ↔ 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) } ) )
53 id ⊢ ( 𝑓 = 𝐹 → 𝑓 = 𝐹 )
54 1 eqcomi ⊢ ( Vtx ‘ 𝐺 ) = 𝑉
55 54 a1i ⊢ ( 𝑓 = 𝐹 → ( Vtx ‘ 𝐺 ) = 𝑉 )
56 2 eqcomi ⊢ ( Vtx ‘ 𝐻 ) = 𝑊
57 56 a1i ⊢ ( 𝑓 = 𝐹 → ( Vtx ‘ 𝐻 ) = 𝑊 )
58 53 55 57 f1oeq123d ⊢ ( 𝑓 = 𝐹 → ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ↔ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) )
59 eqidd ⊢ ( 𝑓 = 𝐹 → 𝑗 = 𝑗 )
60 3 eqcomi ⊢ ( iEdg ‘ 𝐺 ) = 𝐸
61 60 dmeqi ⊢ dom ( iEdg ‘ 𝐺 ) = dom 𝐸
62 61 a1i ⊢ ( 𝑓 = 𝐹 → dom ( iEdg ‘ 𝐺 ) = dom 𝐸 )
63 4 eqcomi ⊢ ( iEdg ‘ 𝐻 ) = 𝐷
64 63 dmeqi ⊢ dom ( iEdg ‘ 𝐻 ) = dom 𝐷
65 64 a1i ⊢ ( 𝑓 = 𝐹 → dom ( iEdg ‘ 𝐻 ) = dom 𝐷 )
66 59 62 65 f1oeq123d ⊢ ( 𝑓 = 𝐹 → ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ↔ 𝑗 : dom 𝐸 –1-1-onto→ dom 𝐷 ) )
67 63 fveq1i ⊢ ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐷 ‘ ( 𝑗 ‘ 𝑖 ) )
68 67 a1i ⊢ ( 𝑓 = 𝐹 → ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐷 ‘ ( 𝑗 ‘ 𝑖 ) ) )
69 60 fveq1i ⊢ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 )
70 69 a1i ⊢ ( 𝑓 = 𝐹 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = ( 𝐸 ‘ 𝑖 ) )
71 53 70 imaeq12d ⊢ ( 𝑓 = 𝐹 → ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐸 ‘ 𝑖 ) ) )
72 68 71 eqeq12d ⊢ ( 𝑓 = 𝐹 → ( ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ↔ ( 𝐷 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐸 ‘ 𝑖 ) ) ) )
73 62 72 raleqbidv ⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ dom 𝐸 ( 𝐷 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐸 ‘ 𝑖 ) ) ) )
74 66 73 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ↔ ( 𝑗 : dom 𝐸 –1-1-onto→ dom 𝐷 ∧ ∀ 𝑖 ∈ dom 𝐸 ( 𝐷 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐸 ‘ 𝑖 ) ) ) ) )
75 74 exbidv ⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ↔ ∃ 𝑗 ( 𝑗 : dom 𝐸 –1-1-onto→ dom 𝐷 ∧ ∀ 𝑖 ∈ dom 𝐸 ( 𝐷 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐸 ‘ 𝑖 ) ) ) ) )
76 58 75 anbi12d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑗 ( 𝑗 : dom 𝐸 –1-1-onto→ dom 𝐷 ∧ ∀ 𝑖 ∈ dom 𝐸 ( 𝐷 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐸 ‘ 𝑖 ) ) ) ) ) )
77 76 elabg ⊢ ( 𝐹 ∈ 𝑍 → ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) } ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑗 ( 𝑗 : dom 𝐸 –1-1-onto→ dom 𝐷 ∧ ∀ 𝑖 ∈ dom 𝐸 ( 𝐷 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐸 ‘ 𝑖 ) ) ) ) ) )
78 77 3ad2ant3 ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( 𝐹 ∈ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) } ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑗 ( 𝑗 : dom 𝐸 –1-1-onto→ dom 𝐷 ∧ ∀ 𝑖 ∈ dom 𝐸 ( 𝐷 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐸 ‘ 𝑖 ) ) ) ) ) )
79 52 78 bitrd ⊢ ( ( 𝐺 ∈ 𝑋 ∧ 𝐻 ∈ 𝑌 ∧ 𝐹 ∈ 𝑍 ) → ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑗 ( 𝑗 : dom 𝐸 –1-1-onto→ dom 𝐷 ∧ ∀ 𝑖 ∈ dom 𝐸 ( 𝐷 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( 𝐸 ‘ 𝑖 ) ) ) ) ) )