Metamath Proof Explorer

Theorem hash2prd

Description: A set of size two is an unordered pair if it contains two different elements. (Contributed by Alexander van der Vekens, 9-Dec-2018) (Proof shortened by AV, 16-Jun-2022)

Ref Expression
Assertion hash2prd 
|- ( ( P e. V /\ ( # ` P ) = 2 ) -> ( ( X e. P /\ Y e. P /\ X =/= Y ) -> P = { X , Y } ) )

Proof

Step Hyp Ref Expression
1 hash2prb 
 |-  ( P e. V -> ( ( # ` P ) = 2 <-> E. x e. P E. y e. P ( x =/= y /\ P = { x , y } ) ) )
2 simpr 
 |-  ( ( ( ( ( x e. P /\ y e. P ) /\ x =/= y ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ P = { x , y } ) -> P = { x , y } )
3 3simpa 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X e. P /\ Y e. P ) )
4 3 ad2antlr 
 |-  ( ( ( ( ( x e. P /\ y e. P ) /\ x =/= y ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ P = { x , y } ) -> ( X e. P /\ Y e. P ) )
5 eleq2 
 |-  ( P = { x , y } -> ( X e. P <-> X e. { x , y } ) )
6 eleq2 
 |-  ( P = { x , y } -> ( Y e. P <-> Y e. { x , y } ) )
7 5 6 anbi12d 
 |-  ( P = { x , y } -> ( ( X e. P /\ Y e. P ) <-> ( X e. { x , y } /\ Y e. { x , y } ) ) )
8 7 adantl 
 |-  ( ( ( ( ( x e. P /\ y e. P ) /\ x =/= y ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ P = { x , y } ) -> ( ( X e. P /\ Y e. P ) <-> ( X e. { x , y } /\ Y e. { x , y } ) ) )
9 4 8 mpbid 
 |-  ( ( ( ( ( x e. P /\ y e. P ) /\ x =/= y ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ P = { x , y } ) -> ( X e. { x , y } /\ Y e. { x , y } ) )
10 prel12g 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( { X , Y } = { x , y } <-> ( X e. { x , y } /\ Y e. { x , y } ) ) )
11 10 ad2antlr 
 |-  ( ( ( ( ( x e. P /\ y e. P ) /\ x =/= y ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ P = { x , y } ) -> ( { X , Y } = { x , y } <-> ( X e. { x , y } /\ Y e. { x , y } ) ) )
12 9 11 mpbird 
 |-  ( ( ( ( ( x e. P /\ y e. P ) /\ x =/= y ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ P = { x , y } ) -> { X , Y } = { x , y } )
13 2 12 eqtr4d 
 |-  ( ( ( ( ( x e. P /\ y e. P ) /\ x =/= y ) /\ ( X e. P /\ Y e. P /\ X =/= Y ) ) /\ P = { x , y } ) -> P = { X , Y } )
14 13 exp31 
 |-  ( ( ( x e. P /\ y e. P ) /\ x =/= y ) -> ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( P = { x , y } -> P = { X , Y } ) ) )
15 14 com23 
 |-  ( ( ( x e. P /\ y e. P ) /\ x =/= y ) -> ( P = { x , y } -> ( ( X e. P /\ Y e. P /\ X =/= Y ) -> P = { X , Y } ) ) )
16 15 expimpd 
 |-  ( ( x e. P /\ y e. P ) -> ( ( x =/= y /\ P = { x , y } ) -> ( ( X e. P /\ Y e. P /\ X =/= Y ) -> P = { X , Y } ) ) )
17 16 rexlimivv 
 |-  ( E. x e. P E. y e. P ( x =/= y /\ P = { x , y } ) -> ( ( X e. P /\ Y e. P /\ X =/= Y ) -> P = { X , Y } ) )
18 1 17 syl6bi 
 |-  ( P e. V -> ( ( # ` P ) = 2 -> ( ( X e. P /\ Y e. P /\ X =/= Y ) -> P = { X , Y } ) ) )
19 18 imp 
 |-  ( ( P e. V /\ ( # ` P ) = 2 ) -> ( ( X e. P /\ Y e. P /\ X =/= Y ) -> P = { X , Y } ) )