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 
|- V = ( Vtx ` A )
gricushgr.w 
|- W = ( Vtx ` B )
gricushgr.e 
|- E = ( Edg ` A )
gricushgr.k 
|- K = ( Edg ` B )
Assertion gricuspgr 
|- ( ( A e. USPGraph /\ B e. USPGraph ) -> ( A ~=gr B <-> E. f ( f : V -1-1-onto-> W /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) ) )

Proof

Step Hyp Ref Expression
1 gricushgr.v 
 |-  V = ( Vtx ` A )
2 gricushgr.w 
 |-  W = ( Vtx ` B )
3 gricushgr.e 
 |-  E = ( Edg ` A )
4 gricushgr.k 
 |-  K = ( Edg ` B )
5 brgric 
 |-  ( A ~=gr B <-> ( A GraphIso B ) =/= (/) )
6 n0 
 |-  ( ( A GraphIso B ) =/= (/) <-> E. f f e. ( A GraphIso B ) )
7 5 6 bitri 
 |-  ( A ~=gr B <-> E. f f e. ( A GraphIso B ) )
8 7 a1i 
 |-  ( ( A e. USPGraph /\ B e. USPGraph ) -> ( A ~=gr B <-> E. f f e. ( A GraphIso B ) ) )
9 1 2 3 4 isuspgrim 
 |-  ( ( A e. USPGraph /\ B e. USPGraph ) -> ( f e. ( A GraphIso B ) <-> ( f : V -1-1-onto-> W /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) ) )
10 9 exbidv 
 |-  ( ( A e. USPGraph /\ B e. USPGraph ) -> ( E. f f e. ( A GraphIso B ) <-> E. f ( f : V -1-1-onto-> W /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) ) )
11 8 10 bitrd 
 |-  ( ( A e. USPGraph /\ B e. USPGraph ) -> ( A ~=gr B <-> E. f ( f : V -1-1-onto-> W /\ A. a e. V A. b e. V ( { a , b } e. E <-> { ( f ` a ) , ( f ` b ) } e. K ) ) ) )