This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 }