Metamath Proof Explorer

Theorem prprelprb

Description: A set is an element of the set of all proper unordered pairs over a given set X iff it is a pair of different elements of the set X . (Contributed by AV, 7-May-2023)

Ref Expression
Assertion prprelprb 
|- ( P e. ( PrPairs ` X ) <-> ( X e. _V /\ E. a e. X E. b e. X ( P = { a , b } /\ a =/= b ) ) )

Proof

Step Hyp Ref Expression
1 prprvalpw 
 |-  ( X e. _V -> ( PrPairs ` X ) = { p e. ~P X | E. a e. X E. b e. X ( a =/= b /\ p = { a , b } ) } )
2 1 eleq2d 
 |-  ( X e. _V -> ( P e. ( PrPairs ` X ) <-> P e. { p e. ~P X | E. a e. X E. b e. X ( a =/= b /\ p = { a , b } ) } ) )
3 eqeq1 
 |-  ( p = P -> ( p = { a , b } <-> P = { a , b } ) )
4 3 anbi2d 
 |-  ( p = P -> ( ( a =/= b /\ p = { a , b } ) <-> ( a =/= b /\ P = { a , b } ) ) )
5 4 2rexbidv 
 |-  ( p = P -> ( E. a e. X E. b e. X ( a =/= b /\ p = { a , b } ) <-> E. a e. X E. b e. X ( a =/= b /\ P = { a , b } ) ) )
6 5 elrab 
 |-  ( P e. { p e. ~P X | E. a e. X E. b e. X ( a =/= b /\ p = { a , b } ) } <-> ( P e. ~P X /\ E. a e. X E. b e. X ( a =/= b /\ P = { a , b } ) ) )
7 2 6 bitrdi 
 |-  ( X e. _V -> ( P e. ( PrPairs ` X ) <-> ( P e. ~P X /\ E. a e. X E. b e. X ( a =/= b /\ P = { a , b } ) ) ) )
8 pm3.22 
 |-  ( ( a =/= b /\ P = { a , b } ) -> ( P = { a , b } /\ a =/= b ) )
9 8 a1i 
 |-  ( ( P e. ~P X /\ ( a e. X /\ b e. X ) ) -> ( ( a =/= b /\ P = { a , b } ) -> ( P = { a , b } /\ a =/= b ) ) )
10 9 reximdvva 
 |-  ( P e. ~P X -> ( E. a e. X E. b e. X ( a =/= b /\ P = { a , b } ) -> E. a e. X E. b e. X ( P = { a , b } /\ a =/= b ) ) )
11 10 imp 
 |-  ( ( P e. ~P X /\ E. a e. X E. b e. X ( a =/= b /\ P = { a , b } ) ) -> E. a e. X E. b e. X ( P = { a , b } /\ a =/= b ) )
12 11 anim2i 
 |-  ( ( X e. _V /\ ( P e. ~P X /\ E. a e. X E. b e. X ( a =/= b /\ P = { a , b } ) ) ) -> ( X e. _V /\ E. a e. X E. b e. X ( P = { a , b } /\ a =/= b ) ) )
13 12 ex 
 |-  ( X e. _V -> ( ( P e. ~P X /\ E. a e. X E. b e. X ( a =/= b /\ P = { a , b } ) ) -> ( X e. _V /\ E. a e. X E. b e. X ( P = { a , b } /\ a =/= b ) ) ) )
14 simpr 
 |-  ( ( ( X e. _V /\ ( a e. X /\ b e. X ) ) /\ ( P = { a , b } /\ a =/= b ) ) -> ( P = { a , b } /\ a =/= b ) )
15 14 ancomd 
 |-  ( ( ( X e. _V /\ ( a e. X /\ b e. X ) ) /\ ( P = { a , b } /\ a =/= b ) ) -> ( a =/= b /\ P = { a , b } ) )
16 prelpwi 
 |-  ( ( a e. X /\ b e. X ) -> { a , b } e. ~P X )
17 16 adantl 
 |-  ( ( X e. _V /\ ( a e. X /\ b e. X ) ) -> { a , b } e. ~P X )
18 17 adantr 
 |-  ( ( ( X e. _V /\ ( a e. X /\ b e. X ) ) /\ ( P = { a , b } /\ a =/= b ) ) -> { a , b } e. ~P X )
19 eleq1 
 |-  ( P = { a , b } -> ( P e. ~P X <-> { a , b } e. ~P X ) )
20 19 adantr 
 |-  ( ( P = { a , b } /\ a =/= b ) -> ( P e. ~P X <-> { a , b } e. ~P X ) )
21 20 adantl 
 |-  ( ( ( X e. _V /\ ( a e. X /\ b e. X ) ) /\ ( P = { a , b } /\ a =/= b ) ) -> ( P e. ~P X <-> { a , b } e. ~P X ) )
22 18 21 mpbird 
 |-  ( ( ( X e. _V /\ ( a e. X /\ b e. X ) ) /\ ( P = { a , b } /\ a =/= b ) ) -> P e. ~P X )
23 15 22 jca 
 |-  ( ( ( X e. _V /\ ( a e. X /\ b e. X ) ) /\ ( P = { a , b } /\ a =/= b ) ) -> ( ( a =/= b /\ P = { a , b } ) /\ P e. ~P X ) )
24 23 ex 
 |-  ( ( X e. _V /\ ( a e. X /\ b e. X ) ) -> ( ( P = { a , b } /\ a =/= b ) -> ( ( a =/= b /\ P = { a , b } ) /\ P e. ~P X ) ) )
25 24 reximdvva 
 |-  ( X e. _V -> ( E. a e. X E. b e. X ( P = { a , b } /\ a =/= b ) -> E. a e. X E. b e. X ( ( a =/= b /\ P = { a , b } ) /\ P e. ~P X ) ) )
26 25 imp 
 |-  ( ( X e. _V /\ E. a e. X E. b e. X ( P = { a , b } /\ a =/= b ) ) -> E. a e. X E. b e. X ( ( a =/= b /\ P = { a , b } ) /\ P e. ~P X ) )
27 r19.41vv 
 |-  ( E. a e. X E. b e. X ( ( a =/= b /\ P = { a , b } ) /\ P e. ~P X ) <-> ( E. a e. X E. b e. X ( a =/= b /\ P = { a , b } ) /\ P e. ~P X ) )
28 27 biancomi 
 |-  ( E. a e. X E. b e. X ( ( a =/= b /\ P = { a , b } ) /\ P e. ~P X ) <-> ( P e. ~P X /\ E. a e. X E. b e. X ( a =/= b /\ P = { a , b } ) ) )
29 26 28 sylib 
 |-  ( ( X e. _V /\ E. a e. X E. b e. X ( P = { a , b } /\ a =/= b ) ) -> ( P e. ~P X /\ E. a e. X E. b e. X ( a =/= b /\ P = { a , b } ) ) )
30 13 29 impbid1 
 |-  ( X e. _V -> ( ( P e. ~P X /\ E. a e. X E. b e. X ( a =/= b /\ P = { a , b } ) ) <-> ( X e. _V /\ E. a e. X E. b e. X ( P = { a , b } /\ a =/= b ) ) ) )
31 7 30 bitrd 
 |-  ( X e. _V -> ( P e. ( PrPairs ` X ) <-> ( X e. _V /\ E. a e. X E. b e. X ( P = { a , b } /\ a =/= b ) ) ) )
32 fvprc 
 |-  ( -. X e. _V -> ( PrPairs ` X ) = (/) )
33 32 eleq2d 
 |-  ( -. X e. _V -> ( P e. ( PrPairs ` X ) <-> P e. (/) ) )
34 noel 
 |-  -. P e. (/)
35 pm2.21 
 |-  ( -. P e. (/) -> ( P e. (/) -> ( X e. _V /\ E. a e. X E. b e. X ( P = { a , b } /\ a =/= b ) ) ) )
36 34 35 mp1i 
 |-  ( -. X e. _V -> ( P e. (/) -> ( X e. _V /\ E. a e. X E. b e. X ( P = { a , b } /\ a =/= b ) ) ) )
37 pm2.21 
 |-  ( -. X e. _V -> ( X e. _V -> ( E. a e. X E. b e. X ( P = { a , b } /\ a =/= b ) -> P e. (/) ) ) )
38 37 impd 
 |-  ( -. X e. _V -> ( ( X e. _V /\ E. a e. X E. b e. X ( P = { a , b } /\ a =/= b ) ) -> P e. (/) ) )
39 36 38 impbid 
 |-  ( -. X e. _V -> ( P e. (/) <-> ( X e. _V /\ E. a e. X E. b e. X ( P = { a , b } /\ a =/= b ) ) ) )
40 33 39 bitrd 
 |-  ( -. X e. _V -> ( P e. ( PrPairs ` X ) <-> ( X e. _V /\ E. a e. X E. b e. X ( P = { a , b } /\ a =/= b ) ) ) )
41 31 40 pm2.61i 
 |-  ( P e. ( PrPairs ` X ) <-> ( X e. _V /\ E. a e. X E. b e. X ( P = { a , b } /\ a =/= b ) ) )