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

Metamath Proof Explorer

Theorem gricuspgr

Description: The "is isomorphic to" relation for two simple pseudographs. This corresponds to the definition in Bollobas p. 3. (Contributed by AV, 1-Dec-2022) (Proof shortened by AV, 5-May-2025)

Ref Expression
Hypotheses gricushgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐴 )
gricushgr.w ⊢ 𝑊 = ( Vtx ‘ 𝐵 )
gricushgr.e ⊢ 𝐸 = ( Edg ‘ 𝐴 )
gricushgr.k ⊢ 𝐾 = ( Edg ‘ 𝐵 )
Assertion gricuspgr ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) → ( 𝐴 ≃𝑔𝑟 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) ) )

Proof

Step Hyp Ref Expression
1 gricushgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐴 )
2 gricushgr.w ⊢ 𝑊 = ( Vtx ‘ 𝐵 )
3 gricushgr.e ⊢ 𝐸 = ( Edg ‘ 𝐴 )
4 gricushgr.k ⊢ 𝐾 = ( Edg ‘ 𝐵 )
5 brgric ⊢ ( 𝐴 ≃𝑔𝑟 𝐵 ↔ ( 𝐴 GraphIso 𝐵 ) ≠ ∅ )
6 n0 ⊢ ( ( 𝐴 GraphIso 𝐵 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐴 GraphIso 𝐵 ) )
7 5 6 bitri ⊢ ( 𝐴 ≃𝑔𝑟 𝐵 ↔ ∃ 𝑓 𝑓 ∈ ( 𝐴 GraphIso 𝐵 ) )
8 7 a1i ⊢ ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) → ( 𝐴 ≃𝑔𝑟 𝐵 ↔ ∃ 𝑓 𝑓 ∈ ( 𝐴 GraphIso 𝐵 ) ) )
9 1 2 3 4 isuspgrim ⊢ ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) → ( 𝑓 ∈ ( 𝐴 GraphIso 𝐵 ) ↔ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) ) )
10 9 exbidv ⊢ ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) → ( ∃ 𝑓 𝑓 ∈ ( 𝐴 GraphIso 𝐵 ) ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) ) )
11 8 10 bitrd ⊢ ( ( 𝐴 ∈ USPGraph ∧ 𝐵 ∈ USPGraph ) → ( 𝐴 ≃𝑔𝑟 𝐵 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) ) )