Metamath Proof Explorer

Theorem pr2pwpr

Description: The set of subsets of a pair having length 2 is the set of the pair as singleton. (Contributed by AV, 9-Dec-2018)

Ref Expression
Assertion pr2pwpr 
|- ( ( A e. V /\ B e. W /\ A =/= B ) -> { p e. ~P { A , B } | p ~~ 2o } = { { A , B } } )

Proof

Step Hyp Ref Expression
1 elpwi 
 |-  ( s e. ~P { A , B } -> s C_ { A , B } )
2 prfi 
 |-  { A , B } e. Fin
3 ssfi 
 |-  ( ( { A , B } e. Fin /\ s C_ { A , B } ) -> s e. Fin )
4 2 3 mpan 
 |-  ( s C_ { A , B } -> s e. Fin )
5 hash2 
 |-  ( # ` 2o ) = 2
6 5 eqcomi 
 |-  2 = ( # ` 2o )
7 6 a1i 
 |-  ( s e. Fin -> 2 = ( # ` 2o ) )
8 7 eqeq2d 
 |-  ( s e. Fin -> ( ( # ` s ) = 2 <-> ( # ` s ) = ( # ` 2o ) ) )
9 2onn 
 |-  2o e. _om
10 nnfi 
 |-  ( 2o e. _om -> 2o e. Fin )
11 9 10 ax-mp 
 |-  2o e. Fin
12 hashen 
 |-  ( ( s e. Fin /\ 2o e. Fin ) -> ( ( # ` s ) = ( # ` 2o ) <-> s ~~ 2o ) )
13 11 12 mpan2 
 |-  ( s e. Fin -> ( ( # ` s ) = ( # ` 2o ) <-> s ~~ 2o ) )
14 8 13 bitrd 
 |-  ( s e. Fin -> ( ( # ` s ) = 2 <-> s ~~ 2o ) )
15 hash2pwpr 
 |-  ( ( ( # ` s ) = 2 /\ s e. ~P { A , B } ) -> s = { A , B } )
16 15 a1d 
 |-  ( ( ( # ` s ) = 2 /\ s e. ~P { A , B } ) -> ( ( A e. V /\ B e. W /\ A =/= B ) -> s = { A , B } ) )
17 16 ex 
 |-  ( ( # ` s ) = 2 -> ( s e. ~P { A , B } -> ( ( A e. V /\ B e. W /\ A =/= B ) -> s = { A , B } ) ) )
18 14 17 syl6bir 
 |-  ( s e. Fin -> ( s ~~ 2o -> ( s e. ~P { A , B } -> ( ( A e. V /\ B e. W /\ A =/= B ) -> s = { A , B } ) ) ) )
19 18 com23 
 |-  ( s e. Fin -> ( s e. ~P { A , B } -> ( s ~~ 2o -> ( ( A e. V /\ B e. W /\ A =/= B ) -> s = { A , B } ) ) ) )
20 4 19 syl 
 |-  ( s C_ { A , B } -> ( s e. ~P { A , B } -> ( s ~~ 2o -> ( ( A e. V /\ B e. W /\ A =/= B ) -> s = { A , B } ) ) ) )
21 1 20 mpcom 
 |-  ( s e. ~P { A , B } -> ( s ~~ 2o -> ( ( A e. V /\ B e. W /\ A =/= B ) -> s = { A , B } ) ) )
22 21 imp 
 |-  ( ( s e. ~P { A , B } /\ s ~~ 2o ) -> ( ( A e. V /\ B e. W /\ A =/= B ) -> s = { A , B } ) )
23 22 com12 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( ( s e. ~P { A , B } /\ s ~~ 2o ) -> s = { A , B } ) )
24 prex 
 |-  { A , B } e. _V
25 24 prid2 
 |-  { A , B } e. { { B } , { A , B } }
26 25 a1i 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> { A , B } e. { { B } , { A , B } } )
27 26 olcd 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( { A , B } e. { (/) , { A } } \/ { A , B } e. { { B } , { A , B } } ) )
28 elun 
 |-  ( { A , B } e. ( { (/) , { A } } u. { { B } , { A , B } } ) <-> ( { A , B } e. { (/) , { A } } \/ { A , B } e. { { B } , { A , B } } ) )
29 27 28 sylibr 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> { A , B } e. ( { (/) , { A } } u. { { B } , { A , B } } ) )
30 pwpr 
 |-  ~P { A , B } = ( { (/) , { A } } u. { { B } , { A , B } } )
31 29 30 eleqtrrdi 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> { A , B } e. ~P { A , B } )
32 31 adantr 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ s = { A , B } ) -> { A , B } e. ~P { A , B } )
33 eleq1 
 |-  ( s = { A , B } -> ( s e. ~P { A , B } <-> { A , B } e. ~P { A , B } ) )
34 33 adantl 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ s = { A , B } ) -> ( s e. ~P { A , B } <-> { A , B } e. ~P { A , B } ) )
35 32 34 mpbird 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ s = { A , B } ) -> s e. ~P { A , B } )
36 pr2nelem 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> { A , B } ~~ 2o )
37 36 adantr 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ s = { A , B } ) -> { A , B } ~~ 2o )
38 breq1 
 |-  ( s = { A , B } -> ( s ~~ 2o <-> { A , B } ~~ 2o ) )
39 38 adantl 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ s = { A , B } ) -> ( s ~~ 2o <-> { A , B } ~~ 2o ) )
40 37 39 mpbird 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ s = { A , B } ) -> s ~~ 2o )
41 35 40 jca 
 |-  ( ( ( A e. V /\ B e. W /\ A =/= B ) /\ s = { A , B } ) -> ( s e. ~P { A , B } /\ s ~~ 2o ) )
42 41 ex 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( s = { A , B } -> ( s e. ~P { A , B } /\ s ~~ 2o ) ) )
43 23 42 impbid 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( ( s e. ~P { A , B } /\ s ~~ 2o ) <-> s = { A , B } ) )
44 breq1 
 |-  ( p = s -> ( p ~~ 2o <-> s ~~ 2o ) )
45 44 elrab 
 |-  ( s e. { p e. ~P { A , B } | p ~~ 2o } <-> ( s e. ~P { A , B } /\ s ~~ 2o ) )
46 velsn 
 |-  ( s e. { { A , B } } <-> s = { A , B } )
47 43 45 46 3bitr4g 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> ( s e. { p e. ~P { A , B } | p ~~ 2o } <-> s e. { { A , B } } ) )
48 47 eqrdv 
 |-  ( ( A e. V /\ B e. W /\ A =/= B ) -> { p e. ~P { A , B } | p ~~ 2o } = { { A , B } } )