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

Proof

Step Hyp Ref Expression
1 pwpr ⊢ 𝒫 X Y = ∅ X ∪ Y X Y
2 1 eleq2i ⊢ P ∈ 𝒫 X Y ↔ P ∈ ∅ X ∪ Y X Y
3 elun ⊢ P ∈ ∅ X ∪ Y X Y ↔ P ∈ ∅ X ∨ P ∈ Y X Y
4 2 3 bitri ⊢ P ∈ 𝒫 X Y ↔ P ∈ ∅ X ∨ P ∈ 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 syl6bi ⊢ 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 ∈ 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 syl6bi ⊢ P = 1 → P = 2 → P = X Y
24 18 23 syl6bi ⊢ P = X → X = 1 → P = 2 → P = X Y
25 15 24 syl5com ⊢ X ∈ V → P = X → P = 2 → P = X Y
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 = X Y
31 27 30 syl6bi ⊢ X = ∅ → P = X → P = 2 → P = X Y
32 26 31 sylbi ⊢ ¬ X ∈ 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 ∈ 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 = X Y
40 35 39 syl5com ⊢ Y ∈ V → P = Y → P = 2 → P = X Y
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 = X Y
46 43 45 syl6bi ⊢ P = ∅ → P = 2 → P = X Y
47 42 46 syl6bi ⊢ Y = ∅ → P = Y → P = 2 → P = X Y
48 41 47 sylbi ⊢ ¬ Y ∈ 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 ∈ ∅ X → P = ∅ ∨ P = X
54 elpri ⊢ P ∈ Y X Y → P = Y ∨ P = X Y
55 53 54 orim12i ⊢ P ∈ ∅ X ∨ P ∈ Y X Y → P = ∅ ∨ P = X ∨ P = Y ∨ P = X Y
56 52 55 syl11 ⊢ P = 2 → P ∈ ∅ X ∨ P ∈ Y X Y → P = X Y
57 4 56 syl5bi ⊢ P = 2 → P ∈ 𝒫 X Y → P = X Y
58 57 imp ⊢ P = 2 ∧ P ∈ 𝒫 X Y → P = X Y