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→ 𝑊 ∧ ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { ( 𝑓 ‘ 𝑎 ) , ( 𝑓 ‘ 𝑏 ) } ∈ 𝐾 ) ) ) )