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 ) ) ) )