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∈𝒫XY→P=XY

Proof

Step Hyp Ref Expression
1 pwpr ⊢𝒫XY=∅X∪YXY
2 1 eleq2i ⊢P∈𝒫XY↔P∈∅X∪YXY
3 elun ⊢P∈∅X∪YXY↔P∈∅X∨P∈YXY
4 2 3 bitri ⊢P∈𝒫XY↔P∈∅X∨P∈YXY
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=XY
11 9 10 mpi ⊢0=2→P=XY
12 8 11 syl6bi ⊢P=0→P=2→P=XY
13 7 12 sylbi ⊢P=∅→P=2→P=XY
14 5 13 syl ⊢P=∅→P=2→P=XY
15 hashsng ⊢X∈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=XY
22 20 21 mpi ⊢1=2→P=XY
23 19 22 syl6bi ⊢P=1→P=2→P=XY
24 18 23 syl6bi ⊢P=X→X=1→P=2→P=XY
25 15 24 syl5com ⊢X∈V→P=X→P=2→P=XY
26 snprc ⊢¬X∈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 syl6bi ⊢P=∅→P=2→P=XY
31 27 30 syl6bi ⊢X=∅→P=X→P=2→P=XY
32 26 31 sylbi ⊢¬X∈V→P=X→P=2→P=XY
33 25 32 pm2.61i ⊢P=X→P=2→P=XY
34 14 33 jaoi ⊢P=∅∨P=X→P=2→P=XY
35 hashsng ⊢Y∈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 syl6bi ⊢P=Y→Y=1→P=2→P=XY
40 35 39 syl5com ⊢Y∈V→P=Y→P=2→P=XY
41 snprc ⊢¬Y∈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=XY
46 43 45 syl6bi ⊢P=∅→P=2→P=XY
47 42 46 syl6bi ⊢Y=∅→P=Y→P=2→P=XY
48 41 47 sylbi ⊢¬Y∈V→P=Y→P=2→P=XY
49 40 48 pm2.61i ⊢P=Y→P=2→P=XY
50 ax-1 ⊢P=XY→P=2→P=XY
51 49 50 jaoi ⊢P=Y∨P=XY→P=2→P=XY
52 34 51 jaoi ⊢P=∅∨P=X∨P=Y∨P=XY→P=2→P=XY
53 elpri ⊢P∈∅X→P=∅∨P=X
54 elpri ⊢P∈YXY→P=Y∨P=XY
55 53 54 orim12i ⊢P∈∅X∨P∈YXY→P=∅∨P=X∨P=Y∨P=XY
56 52 55 syl11 ⊢P=2→P∈∅X∨P∈YXY→P=XY
57 4 56 biimtrid ⊢P=2→P∈𝒫XY→P=XY
58 57 imp ⊢P=2∧P∈𝒫XY→P=XY