Theorem umgrbi

Description: Show that an unordered pair is a valid edge in a multigraph. (Contributed by AV, 9-Mar-2021)

	Ref	Expression
Hypotheses	umgrbi.x	|- X e. V
	umgrbi.y	|- Y e. V
	umgrbi.n	|- X =/= Y
Assertion	umgrbi	|- { X , Y } e. { x e. ~P V | ( # ` x ) = 2 }

Proof

Step	Hyp	Ref	Expression
1		umgrbi.x	|- X e. V
2		umgrbi.y	|- Y e. V
3		umgrbi.n	|- X =/= Y
4		prssi	|- ( ( X e. V /\ Y e. V ) -> { X , Y } C_ V )
5	1 2 4	mp2an	|- { X , Y } C_ V
6		prex	|- { X , Y } e. _V
7	6	elpw	|- ( { X , Y } e. ~P V <-> { X , Y } C_ V )
8	5 7	mpbir	|- { X , Y } e. ~P V
9		hashprg	|- ( ( X e. V /\ Y e. V ) -> ( X =/= Y <-> ( # ` { X , Y } ) = 2 ) )
10	3 9	mpbii	|- ( ( X e. V /\ Y e. V ) -> ( # ` { X , Y } ) = 2 )
11	1 2 10	mp2an	|- ( # ` { X , Y } ) = 2
12		fveqeq2	|- ( x = { X , Y } -> ( ( # ` x ) = 2 <-> ( # ` { X , Y } ) = 2 ) )
13	12	elrab	|- ( { X , Y } e. { x e. ~P V | ( # ` x ) = 2 } <-> ( { X , Y } e. ~P V /\ ( # ` { X , Y } ) = 2 ) )
14	8 11 13	mpbir2an	|- { X , Y } e. { x e. ~P V | ( # ` x ) = 2 }