Metamath Proof Explorer

Theorem prpair

Description: Characterization of a proper pair: A class is a proper pair iff it consists of exactly two different sets. (Contributed by AV, 11-Mar-2023)

Ref Expression
Hypothesis prpair.p 
|- P = { x e. ~P V | ( # ` x ) = 2 }
Assertion prpair 
|- ( X e. P <-> E. a e. V E. b e. V ( X = { a , b } /\ a =/= b ) )

Proof

Step Hyp Ref Expression
1 prpair.p 
 |-  P = { x e. ~P V | ( # ` x ) = 2 }
2 1 eleq2i 
 |-  ( X e. P <-> X e. { x e. ~P V | ( # ` x ) = 2 } )
3 fveqeq2 
 |-  ( x = X -> ( ( # ` x ) = 2 <-> ( # ` X ) = 2 ) )
4 3 elrab 
 |-  ( X e. { x e. ~P V | ( # ` x ) = 2 } <-> ( X e. ~P V /\ ( # ` X ) = 2 ) )
5 hash2prb 
 |-  ( X e. ~P V -> ( ( # ` X ) = 2 <-> E. a e. X E. b e. X ( a =/= b /\ X = { a , b } ) ) )
6 elpwi 
 |-  ( X e. ~P V -> X C_ V )
7 ancom 
 |-  ( ( a =/= b /\ X = { a , b } ) <-> ( X = { a , b } /\ a =/= b ) )
8 7 2rexbii 
 |-  ( E. a e. X E. b e. X ( a =/= b /\ X = { a , b } ) <-> E. a e. X E. b e. X ( X = { a , b } /\ a =/= b ) )
9 8 biimpi 
 |-  ( E. a e. X E. b e. X ( a =/= b /\ X = { a , b } ) -> E. a e. X E. b e. X ( X = { a , b } /\ a =/= b ) )
10 ss2rexv 
 |-  ( X C_ V -> ( E. a e. X E. b e. X ( X = { a , b } /\ a =/= b ) -> E. a e. V E. b e. V ( X = { a , b } /\ a =/= b ) ) )
11 6 9 10 syl2im 
 |-  ( X e. ~P V -> ( E. a e. X E. b e. X ( a =/= b /\ X = { a , b } ) -> E. a e. V E. b e. V ( X = { a , b } /\ a =/= b ) ) )
12 5 11 sylbid 
 |-  ( X e. ~P V -> ( ( # ` X ) = 2 -> E. a e. V E. b e. V ( X = { a , b } /\ a =/= b ) ) )
13 12 imp 
 |-  ( ( X e. ~P V /\ ( # ` X ) = 2 ) -> E. a e. V E. b e. V ( X = { a , b } /\ a =/= b ) )
14 prelpwi 
 |-  ( ( a e. V /\ b e. V ) -> { a , b } e. ~P V )
15 14 adantr 
 |-  ( ( ( a e. V /\ b e. V ) /\ ( X = { a , b } /\ a =/= b ) ) -> { a , b } e. ~P V )
16 hashprg 
 |-  ( ( a e. V /\ b e. V ) -> ( a =/= b <-> ( # ` { a , b } ) = 2 ) )
17 16 biimpd 
 |-  ( ( a e. V /\ b e. V ) -> ( a =/= b -> ( # ` { a , b } ) = 2 ) )
18 17 adantld 
 |-  ( ( a e. V /\ b e. V ) -> ( ( X = { a , b } /\ a =/= b ) -> ( # ` { a , b } ) = 2 ) )
19 18 imp 
 |-  ( ( ( a e. V /\ b e. V ) /\ ( X = { a , b } /\ a =/= b ) ) -> ( # ` { a , b } ) = 2 )
20 eleq1 
 |-  ( X = { a , b } -> ( X e. ~P V <-> { a , b } e. ~P V ) )
21 fveqeq2 
 |-  ( X = { a , b } -> ( ( # ` X ) = 2 <-> ( # ` { a , b } ) = 2 ) )
22 20 21 anbi12d 
 |-  ( X = { a , b } -> ( ( X e. ~P V /\ ( # ` X ) = 2 ) <-> ( { a , b } e. ~P V /\ ( # ` { a , b } ) = 2 ) ) )
23 22 adantr 
 |-  ( ( X = { a , b } /\ a =/= b ) -> ( ( X e. ~P V /\ ( # ` X ) = 2 ) <-> ( { a , b } e. ~P V /\ ( # ` { a , b } ) = 2 ) ) )
24 23 adantl 
 |-  ( ( ( a e. V /\ b e. V ) /\ ( X = { a , b } /\ a =/= b ) ) -> ( ( X e. ~P V /\ ( # ` X ) = 2 ) <-> ( { a , b } e. ~P V /\ ( # ` { a , b } ) = 2 ) ) )
25 15 19 24 mpbir2and 
 |-  ( ( ( a e. V /\ b e. V ) /\ ( X = { a , b } /\ a =/= b ) ) -> ( X e. ~P V /\ ( # ` X ) = 2 ) )
26 25 ex 
 |-  ( ( a e. V /\ b e. V ) -> ( ( X = { a , b } /\ a =/= b ) -> ( X e. ~P V /\ ( # ` X ) = 2 ) ) )
27 26 rexlimivv 
 |-  ( E. a e. V E. b e. V ( X = { a , b } /\ a =/= b ) -> ( X e. ~P V /\ ( # ` X ) = 2 ) )
28 13 27 impbii 
 |-  ( ( X e. ~P V /\ ( # ` X ) = 2 ) <-> E. a e. V E. b e. V ( X = { a , b } /\ a =/= b ) )
29 2 4 28 3bitri 
 |-  ( X e. P <-> E. a e. V E. b e. V ( X = { a , b } /\ a =/= b ) )