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

Metamath Proof Explorer

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 }