Metamath Proof Explorer

Theorem elss2prb

Description: An element of the set of subsets with two elements is a proper unordered pair. (Contributed by AV, 1-Nov-2020)

Ref Expression
Assertion elss2prb 
|- ( P e. { z e. ~P V | ( # ` z ) = 2 } <-> E. x e. V E. y e. V ( x =/= y /\ P = { x , y } ) )

Proof

Step Hyp Ref Expression
1 fveqeq2 
 |-  ( z = P -> ( ( # ` z ) = 2 <-> ( # ` P ) = 2 ) )
2 1 elrab 
 |-  ( P e. { z e. ~P V | ( # ` z ) = 2 } <-> ( P e. ~P V /\ ( # ` P ) = 2 ) )
3 hash2prb 
 |-  ( P e. ~P V -> ( ( # ` P ) = 2 <-> E. x e. P E. y e. P ( x =/= y /\ P = { x , y } ) ) )
4 elpwi 
 |-  ( P e. ~P V -> P C_ V )
5 ssrexv 
 |-  ( P C_ V -> ( E. x e. P E. y e. P ( x =/= y /\ P = { x , y } ) -> E. x e. V E. y e. P ( x =/= y /\ P = { x , y } ) ) )
6 4 5 syl 
 |-  ( P e. ~P V -> ( E. x e. P E. y e. P ( x =/= y /\ P = { x , y } ) -> E. x e. V E. y e. P ( x =/= y /\ P = { x , y } ) ) )
7 ssrexv 
 |-  ( P C_ V -> ( E. y e. P ( x =/= y /\ P = { x , y } ) -> E. y e. V ( x =/= y /\ P = { x , y } ) ) )
8 4 7 syl 
 |-  ( P e. ~P V -> ( E. y e. P ( x =/= y /\ P = { x , y } ) -> E. y e. V ( x =/= y /\ P = { x , y } ) ) )
9 8 reximdv 
 |-  ( P e. ~P V -> ( E. x e. V E. y e. P ( x =/= y /\ P = { x , y } ) -> E. x e. V E. y e. V ( x =/= y /\ P = { x , y } ) ) )
10 6 9 syld 
 |-  ( P e. ~P V -> ( E. x e. P E. y e. P ( x =/= y /\ P = { x , y } ) -> E. x e. V E. y e. V ( x =/= y /\ P = { x , y } ) ) )
11 3 10 sylbid 
 |-  ( P e. ~P V -> ( ( # ` P ) = 2 -> E. x e. V E. y e. V ( x =/= y /\ P = { x , y } ) ) )
12 11 imp 
 |-  ( ( P e. ~P V /\ ( # ` P ) = 2 ) -> E. x e. V E. y e. V ( x =/= y /\ P = { x , y } ) )
13 prelpwi 
 |-  ( ( x e. V /\ y e. V ) -> { x , y } e. ~P V )
14 13 adantr 
 |-  ( ( ( x e. V /\ y e. V ) /\ ( x =/= y /\ P = { x , y } ) ) -> { x , y } e. ~P V )
15 eleq1 
 |-  ( P = { x , y } -> ( P e. ~P V <-> { x , y } e. ~P V ) )
16 15 ad2antll 
 |-  ( ( ( x e. V /\ y e. V ) /\ ( x =/= y /\ P = { x , y } ) ) -> ( P e. ~P V <-> { x , y } e. ~P V ) )
17 14 16 mpbird 
 |-  ( ( ( x e. V /\ y e. V ) /\ ( x =/= y /\ P = { x , y } ) ) -> P e. ~P V )
18 fveq2 
 |-  ( P = { x , y } -> ( # ` P ) = ( # ` { x , y } ) )
19 18 ad2antll 
 |-  ( ( ( x e. V /\ y e. V ) /\ ( x =/= y /\ P = { x , y } ) ) -> ( # ` P ) = ( # ` { x , y } ) )
20 hashprg 
 |-  ( ( x e. V /\ y e. V ) -> ( x =/= y <-> ( # ` { x , y } ) = 2 ) )
21 20 biimpcd 
 |-  ( x =/= y -> ( ( x e. V /\ y e. V ) -> ( # ` { x , y } ) = 2 ) )
22 21 adantr 
 |-  ( ( x =/= y /\ P = { x , y } ) -> ( ( x e. V /\ y e. V ) -> ( # ` { x , y } ) = 2 ) )
23 22 impcom 
 |-  ( ( ( x e. V /\ y e. V ) /\ ( x =/= y /\ P = { x , y } ) ) -> ( # ` { x , y } ) = 2 )
24 19 23 eqtrd 
 |-  ( ( ( x e. V /\ y e. V ) /\ ( x =/= y /\ P = { x , y } ) ) -> ( # ` P ) = 2 )
25 17 24 jca 
 |-  ( ( ( x e. V /\ y e. V ) /\ ( x =/= y /\ P = { x , y } ) ) -> ( P e. ~P V /\ ( # ` P ) = 2 ) )
26 25 ex 
 |-  ( ( x e. V /\ y e. V ) -> ( ( x =/= y /\ P = { x , y } ) -> ( P e. ~P V /\ ( # ` P ) = 2 ) ) )
27 26 rexlimivv 
 |-  ( E. x e. V E. y e. V ( x =/= y /\ P = { x , y } ) -> ( P e. ~P V /\ ( # ` P ) = 2 ) )
28 12 27 impbii 
 |-  ( ( P e. ~P V /\ ( # ` P ) = 2 ) <-> E. x e. V E. y e. V ( x =/= y /\ P = { x , y } ) )
29 2 28 bitri 
 |-  ( P e. { z e. ~P V | ( # ` z ) = 2 } <-> E. x e. V E. y e. V ( x =/= y /\ P = { x , y } ) )