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

Metamath Proof Explorer

Theorem dfgric2

Description: Alternate, explicit definition of the "is isomorphic to" relation for two graphs. (Contributed by AV, 11-Nov-2022) (Revised by AV, 5-May-2025)

Ref Expression
Hypotheses dfgric2.v ⊢ 𝑉 = ( Vtx ‘ 𝐴 )
dfgric2.w ⊢ 𝑊 = ( Vtx ‘ 𝐵 )
dfgric2.i ⊢ 𝐼 = ( iEdg ‘ 𝐴 )
dfgric2.j ⊢ 𝐽 = ( iEdg ‘ 𝐵 )
Assertion dfgric2 ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 ≃𝑔𝑟 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfgric2.v ⊢ 𝑉 = ( Vtx ‘ 𝐴 )
2 dfgric2.w ⊢ 𝑊 = ( Vtx ‘ 𝐵 )
3 dfgric2.i ⊢ 𝐼 = ( iEdg ‘ 𝐴 )
4 dfgric2.j ⊢ 𝐽 = ( iEdg ‘ 𝐵 )
5 brgric ⊢ ( 𝐴 ≃𝑔𝑟 𝐵 ↔ ( 𝐴 GraphIso 𝐵 ) ≠ ∅ )
6 n0 ⊢ ( ( 𝐴 GraphIso 𝐵 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐴 GraphIso 𝐵 ) )
7 5 6 bitri ⊢ ( 𝐴 ≃𝑔𝑟 𝐵 ↔ ∃ 𝑓 𝑓 ∈ ( 𝐴 GraphIso 𝐵 ) )
8 vex ⊢ 𝑓 ∈ V
9 1 2 3 4 isgrim ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑓 ∈ V ) → ( 𝑓 ∈ ( 𝐴 GraphIso 𝐵 ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) ) ) ) )
10 eqcom ⊢ ( ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) ↔ ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) )
11 10 ralbii ⊢ ( ∀ 𝑖 ∈ dom 𝐼 ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) ↔ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) )
12 11 anbi2i ⊢ ( ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) ) ↔ ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
13 12 exbii ⊢ ( ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) ) ↔ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) )
14 13 anbi2i ⊢ ( ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) ) ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) )
15 9 14 bitrdi ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ∧ 𝑓 ∈ V ) → ( 𝑓 ∈ ( 𝐴 GraphIso 𝐵 ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
16 8 15 mp3an3 ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( 𝑓 ∈ ( 𝐴 GraphIso 𝐵 ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
17 16 exbidv ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( ∃ 𝑓 𝑓 ∈ ( 𝐴 GraphIso 𝐵 ) ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )
18 7 17 bitrid ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 ≃𝑔𝑟 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑔 ( 𝑔 : dom 𝐼 –1-1-onto→ dom 𝐽 ∧ ∀ 𝑖 ∈ dom 𝐼 ( 𝑓 “ ( 𝐼 ‘ 𝑖 ) ) = ( 𝐽 ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) ) )