Theorem upgrbi

Description: Show that an unordered pair is a valid edge in a pseudograph. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 28-Feb-2016) (Revised by AV, 28-Feb-2021)

	Ref	Expression
Hypotheses	upgrbi.x	|- X e. V
	upgrbi.y	|- Y e. V
Assertion	upgrbi	|- { X , Y } e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 }

Proof

Step	Hyp	Ref	Expression
1		upgrbi.x	|- X e. V
2		upgrbi.y	|- Y e. V
3		prssi	|- ( ( X e. V /\ Y e. V ) -> { X , Y } C_ V )
4	1 2 3	mp2an	|- { X , Y } C_ V
5		prex	|- { X , Y } e. _V
6	5	elpw	|- ( { X , Y } e. ~P V <-> { X , Y } C_ V )
7	4 6	mpbir	|- { X , Y } e. ~P V
8	1	elexi	|- X e. _V
9	8	prnz	|- { X , Y } =/= (/)
10		eldifsn	|- ( { X , Y } e. ( ~P V \ { (/) } ) <-> ( { X , Y } e. ~P V /\ { X , Y } =/= (/) ) )
11	7 9 10	mpbir2an	|- { X , Y } e. ( ~P V \ { (/) } )
12		hashprlei	|- ( { X , Y } e. Fin /\ ( # ` { X , Y } ) <_ 2 )
13	12	simpri	|- ( # ` { X , Y } ) <_ 2
14		fveq2	|- ( x = { X , Y } -> ( # ` x ) = ( # ` { X , Y } ) )
15	14	breq1d	|- ( x = { X , Y } -> ( ( # ` x ) <_ 2 <-> ( # ` { X , Y } ) <_ 2 ) )
16	15	elrab	|- ( { X , Y } e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } <-> ( { X , Y } e. ( ~P V \ { (/) } ) /\ ( # ` { X , Y } ) <_ 2 ) )
17	11 13 16	mpbir2an	|- { X , Y } e. { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 }