Metamath Proof Explorer

Theorem hash2pwpr

Description: If the size of a subset of an unordered pair is 2, the subset is the pair itself. (Contributed by Alexander van der Vekens, 9-Dec-2018)

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

Proof

Step Hyp Ref Expression
1 pwpr 
 |-  ~P { X , Y } = ( { (/) , { X } } u. { { Y } , { X , Y } } )
2 1 eleq2i 
 |-  ( P e. ~P { X , Y } <-> P e. ( { (/) , { X } } u. { { Y } , { X , Y } } ) )
3 elun 
 |-  ( P e. ( { (/) , { X } } u. { { Y } , { X , Y } } ) <-> ( P e. { (/) , { X } } \/ P e. { { Y } , { X , Y } } ) )
4 2 3 bitri 
 |-  ( P e. ~P { X , Y } <-> ( P e. { (/) , { X } } \/ P e. { { Y } , { X , Y } } ) )
5 fveq2 
 |-  ( P = (/) -> ( # ` P ) = ( # ` (/) ) )
6 hash0 
 |-  ( # ` (/) ) = 0
7 6 eqeq2i 
 |-  ( ( # ` P ) = ( # ` (/) ) <-> ( # ` P ) = 0 )
8 eqeq1 
 |-  ( ( # ` P ) = 0 -> ( ( # ` P ) = 2 <-> 0 = 2 ) )
9 0ne2 
 |-  0 =/= 2
10 eqneqall 
 |-  ( 0 = 2 -> ( 0 =/= 2 -> P = { X , Y } ) )
11 9 10 mpi 
 |-  ( 0 = 2 -> P = { X , Y } )
12 8 11 biimtrdi 
 |-  ( ( # ` P ) = 0 -> ( ( # ` P ) = 2 -> P = { X , Y } ) )
13 7 12 sylbi 
 |-  ( ( # ` P ) = ( # ` (/) ) -> ( ( # ` P ) = 2 -> P = { X , Y } ) )
14 5 13 syl 
 |-  ( P = (/) -> ( ( # ` P ) = 2 -> P = { X , Y } ) )
15 hashsng 
 |-  ( X e. _V -> ( # ` { X } ) = 1 )
16 fveq2 
 |-  ( { X } = P -> ( # ` { X } ) = ( # ` P ) )
17 16 eqcoms 
 |-  ( P = { X } -> ( # ` { X } ) = ( # ` P ) )
18 17 eqeq1d 
 |-  ( P = { X } -> ( ( # ` { X } ) = 1 <-> ( # ` P ) = 1 ) )
19 eqeq1 
 |-  ( ( # ` P ) = 1 -> ( ( # ` P ) = 2 <-> 1 = 2 ) )
20 1ne2 
 |-  1 =/= 2
21 eqneqall 
 |-  ( 1 = 2 -> ( 1 =/= 2 -> P = { X , Y } ) )
22 20 21 mpi 
 |-  ( 1 = 2 -> P = { X , Y } )
23 19 22 biimtrdi 
 |-  ( ( # ` P ) = 1 -> ( ( # ` P ) = 2 -> P = { X , Y } ) )
24 18 23 biimtrdi 
 |-  ( P = { X } -> ( ( # ` { X } ) = 1 -> ( ( # ` P ) = 2 -> P = { X , Y } ) ) )
25 15 24 syl5com 
 |-  ( X e. _V -> ( P = { X } -> ( ( # ` P ) = 2 -> P = { X , Y } ) ) )
26 snprc 
 |-  ( -. X e. _V <-> { X } = (/) )
27 eqeq2 
 |-  ( { X } = (/) -> ( P = { X } <-> P = (/) ) )
28 5 6 eqtrdi 
 |-  ( P = (/) -> ( # ` P ) = 0 )
29 28 eqeq1d 
 |-  ( P = (/) -> ( ( # ` P ) = 2 <-> 0 = 2 ) )
30 29 11 biimtrdi 
 |-  ( P = (/) -> ( ( # ` P ) = 2 -> P = { X , Y } ) )
31 27 30 biimtrdi 
 |-  ( { X } = (/) -> ( P = { X } -> ( ( # ` P ) = 2 -> P = { X , Y } ) ) )
32 26 31 sylbi 
 |-  ( -. X e. _V -> ( P = { X } -> ( ( # ` P ) = 2 -> P = { X , Y } ) ) )
33 25 32 pm2.61i 
 |-  ( P = { X } -> ( ( # ` P ) = 2 -> P = { X , Y } ) )
34 14 33 jaoi 
 |-  ( ( P = (/) \/ P = { X } ) -> ( ( # ` P ) = 2 -> P = { X , Y } ) )
35 hashsng 
 |-  ( Y e. _V -> ( # ` { Y } ) = 1 )
36 fveq2 
 |-  ( { Y } = P -> ( # ` { Y } ) = ( # ` P ) )
37 36 eqcoms 
 |-  ( P = { Y } -> ( # ` { Y } ) = ( # ` P ) )
38 37 eqeq1d 
 |-  ( P = { Y } -> ( ( # ` { Y } ) = 1 <-> ( # ` P ) = 1 ) )
39 38 23 biimtrdi 
 |-  ( P = { Y } -> ( ( # ` { Y } ) = 1 -> ( ( # ` P ) = 2 -> P = { X , Y } ) ) )
40 35 39 syl5com 
 |-  ( Y e. _V -> ( P = { Y } -> ( ( # ` P ) = 2 -> P = { X , Y } ) ) )
41 snprc 
 |-  ( -. Y e. _V <-> { Y } = (/) )
42 eqeq2 
 |-  ( { Y } = (/) -> ( P = { Y } <-> P = (/) ) )
43 5 eqeq1d 
 |-  ( P = (/) -> ( ( # ` P ) = 2 <-> ( # ` (/) ) = 2 ) )
44 6 eqeq1i 
 |-  ( ( # ` (/) ) = 2 <-> 0 = 2 )
45 44 11 sylbi 
 |-  ( ( # ` (/) ) = 2 -> P = { X , Y } )
46 43 45 biimtrdi 
 |-  ( P = (/) -> ( ( # ` P ) = 2 -> P = { X , Y } ) )
47 42 46 biimtrdi 
 |-  ( { Y } = (/) -> ( P = { Y } -> ( ( # ` P ) = 2 -> P = { X , Y } ) ) )
48 41 47 sylbi 
 |-  ( -. Y e. _V -> ( P = { Y } -> ( ( # ` P ) = 2 -> P = { X , Y } ) ) )
49 40 48 pm2.61i 
 |-  ( P = { Y } -> ( ( # ` P ) = 2 -> P = { X , Y } ) )
50 ax-1 
 |-  ( P = { X , Y } -> ( ( # ` P ) = 2 -> P = { X , Y } ) )
51 49 50 jaoi 
 |-  ( ( P = { Y } \/ P = { X , Y } ) -> ( ( # ` P ) = 2 -> P = { X , Y } ) )
52 34 51 jaoi 
 |-  ( ( ( P = (/) \/ P = { X } ) \/ ( P = { Y } \/ P = { X , Y } ) ) -> ( ( # ` P ) = 2 -> P = { X , Y } ) )
53 elpri 
 |-  ( P e. { (/) , { X } } -> ( P = (/) \/ P = { X } ) )
54 elpri 
 |-  ( P e. { { Y } , { X , Y } } -> ( P = { Y } \/ P = { X , Y } ) )
55 53 54 orim12i 
 |-  ( ( P e. { (/) , { X } } \/ P e. { { Y } , { X , Y } } ) -> ( ( P = (/) \/ P = { X } ) \/ ( P = { Y } \/ P = { X , Y } ) ) )
56 52 55 syl11 
 |-  ( ( # ` P ) = 2 -> ( ( P e. { (/) , { X } } \/ P e. { { Y } , { X , Y } } ) -> P = { X , Y } ) )
57 4 56 biimtrid 
 |-  ( ( # ` P ) = 2 -> ( P e. ~P { X , Y } -> P = { X , Y } ) )
58 57 imp 
 |-  ( ( ( # ` P ) = 2 /\ P e. ~P { X , Y } ) -> P = { X , Y } )