Proof of Theorem hash2pwpr
Step | Hyp | Ref
| Expression |
1 | | pwpr 4430 |
. . . . 5
⊢ 𝒫
{𝑋, 𝑌} = ({∅, {𝑋}} ∪ {{𝑌}, {𝑋, 𝑌}}) |
2 | 1 | eleq2i 2693 |
. . . 4
⊢ (𝑃 ∈ 𝒫 {𝑋, 𝑌} ↔ 𝑃 ∈ ({∅, {𝑋}} ∪ {{𝑌}, {𝑋, 𝑌}})) |
3 | | elun 3753 |
. . . 4
⊢ (𝑃 ∈ ({∅, {𝑋}} ∪ {{𝑌}, {𝑋, 𝑌}}) ↔ (𝑃 ∈ {∅, {𝑋}} ∨ 𝑃 ∈ {{𝑌}, {𝑋, 𝑌}})) |
4 | 2, 3 | bitri 264 |
. . 3
⊢ (𝑃 ∈ 𝒫 {𝑋, 𝑌} ↔ (𝑃 ∈ {∅, {𝑋}} ∨ 𝑃 ∈ {{𝑌}, {𝑋, 𝑌}})) |
5 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑃 = ∅ → (#‘𝑃) =
(#‘∅)) |
6 | | hash0 13158 |
. . . . . . . . 9
⊢
(#‘∅) = 0 |
7 | 6 | eqeq2i 2634 |
. . . . . . . 8
⊢
((#‘𝑃) =
(#‘∅) ↔ (#‘𝑃) = 0) |
8 | | eqeq1 2626 |
. . . . . . . . 9
⊢
((#‘𝑃) = 0
→ ((#‘𝑃) = 2
↔ 0 = 2)) |
9 | | 0ne2 11239 |
. . . . . . . . . 10
⊢ 0 ≠
2 |
10 | | eqneqall 2805 |
. . . . . . . . . 10
⊢ (0 = 2
→ (0 ≠ 2 → 𝑃 =
{𝑋, 𝑌})) |
11 | 9, 10 | mpi 20 |
. . . . . . . . 9
⊢ (0 = 2
→ 𝑃 = {𝑋, 𝑌}) |
12 | 8, 11 | syl6bi 243 |
. . . . . . . 8
⊢
((#‘𝑃) = 0
→ ((#‘𝑃) = 2
→ 𝑃 = {𝑋, 𝑌})) |
13 | 7, 12 | sylbi 207 |
. . . . . . 7
⊢
((#‘𝑃) =
(#‘∅) → ((#‘𝑃) = 2 → 𝑃 = {𝑋, 𝑌})) |
14 | 5, 13 | syl 17 |
. . . . . 6
⊢ (𝑃 = ∅ →
((#‘𝑃) = 2 →
𝑃 = {𝑋, 𝑌})) |
15 | | hashsng 13159 |
. . . . . . . 8
⊢ (𝑋 ∈ V → (#‘{𝑋}) = 1) |
16 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ ({𝑋} = 𝑃 → (#‘{𝑋}) = (#‘𝑃)) |
17 | 16 | eqcoms 2630 |
. . . . . . . . . 10
⊢ (𝑃 = {𝑋} → (#‘{𝑋}) = (#‘𝑃)) |
18 | 17 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑃 = {𝑋} → ((#‘{𝑋}) = 1 ↔ (#‘𝑃) = 1)) |
19 | | eqeq1 2626 |
. . . . . . . . . 10
⊢
((#‘𝑃) = 1
→ ((#‘𝑃) = 2
↔ 1 = 2)) |
20 | | 1ne2 11240 |
. . . . . . . . . . 11
⊢ 1 ≠
2 |
21 | | eqneqall 2805 |
. . . . . . . . . . 11
⊢ (1 = 2
→ (1 ≠ 2 → 𝑃 =
{𝑋, 𝑌})) |
22 | 20, 21 | mpi 20 |
. . . . . . . . . 10
⊢ (1 = 2
→ 𝑃 = {𝑋, 𝑌}) |
23 | 19, 22 | syl6bi 243 |
. . . . . . . . 9
⊢
((#‘𝑃) = 1
→ ((#‘𝑃) = 2
→ 𝑃 = {𝑋, 𝑌})) |
24 | 18, 23 | syl6bi 243 |
. . . . . . . 8
⊢ (𝑃 = {𝑋} → ((#‘{𝑋}) = 1 → ((#‘𝑃) = 2 → 𝑃 = {𝑋, 𝑌}))) |
25 | 15, 24 | syl5com 31 |
. . . . . . 7
⊢ (𝑋 ∈ V → (𝑃 = {𝑋} → ((#‘𝑃) = 2 → 𝑃 = {𝑋, 𝑌}))) |
26 | | snprc 4253 |
. . . . . . . 8
⊢ (¬
𝑋 ∈ V ↔ {𝑋} = ∅) |
27 | | eqeq2 2633 |
. . . . . . . . 9
⊢ ({𝑋} = ∅ → (𝑃 = {𝑋} ↔ 𝑃 = ∅)) |
28 | 5, 6 | syl6eq 2672 |
. . . . . . . . . . 11
⊢ (𝑃 = ∅ → (#‘𝑃) = 0) |
29 | 28 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑃 = ∅ →
((#‘𝑃) = 2 ↔ 0 =
2)) |
30 | 29, 11 | syl6bi 243 |
. . . . . . . . 9
⊢ (𝑃 = ∅ →
((#‘𝑃) = 2 →
𝑃 = {𝑋, 𝑌})) |
31 | 27, 30 | syl6bi 243 |
. . . . . . . 8
⊢ ({𝑋} = ∅ → (𝑃 = {𝑋} → ((#‘𝑃) = 2 → 𝑃 = {𝑋, 𝑌}))) |
32 | 26, 31 | sylbi 207 |
. . . . . . 7
⊢ (¬
𝑋 ∈ V → (𝑃 = {𝑋} → ((#‘𝑃) = 2 → 𝑃 = {𝑋, 𝑌}))) |
33 | 25, 32 | pm2.61i 176 |
. . . . . 6
⊢ (𝑃 = {𝑋} → ((#‘𝑃) = 2 → 𝑃 = {𝑋, 𝑌})) |
34 | 14, 33 | jaoi 394 |
. . . . 5
⊢ ((𝑃 = ∅ ∨ 𝑃 = {𝑋}) → ((#‘𝑃) = 2 → 𝑃 = {𝑋, 𝑌})) |
35 | | hashsng 13159 |
. . . . . . . 8
⊢ (𝑌 ∈ V → (#‘{𝑌}) = 1) |
36 | | fveq2 6191 |
. . . . . . . . . . 11
⊢ ({𝑌} = 𝑃 → (#‘{𝑌}) = (#‘𝑃)) |
37 | 36 | eqcoms 2630 |
. . . . . . . . . 10
⊢ (𝑃 = {𝑌} → (#‘{𝑌}) = (#‘𝑃)) |
38 | 37 | eqeq1d 2624 |
. . . . . . . . 9
⊢ (𝑃 = {𝑌} → ((#‘{𝑌}) = 1 ↔ (#‘𝑃) = 1)) |
39 | 38, 23 | syl6bi 243 |
. . . . . . . 8
⊢ (𝑃 = {𝑌} → ((#‘{𝑌}) = 1 → ((#‘𝑃) = 2 → 𝑃 = {𝑋, 𝑌}))) |
40 | 35, 39 | syl5com 31 |
. . . . . . 7
⊢ (𝑌 ∈ V → (𝑃 = {𝑌} → ((#‘𝑃) = 2 → 𝑃 = {𝑋, 𝑌}))) |
41 | | snprc 4253 |
. . . . . . . 8
⊢ (¬
𝑌 ∈ V ↔ {𝑌} = ∅) |
42 | | eqeq2 2633 |
. . . . . . . . 9
⊢ ({𝑌} = ∅ → (𝑃 = {𝑌} ↔ 𝑃 = ∅)) |
43 | 5 | eqeq1d 2624 |
. . . . . . . . . 10
⊢ (𝑃 = ∅ →
((#‘𝑃) = 2 ↔
(#‘∅) = 2)) |
44 | 6 | eqeq1i 2627 |
. . . . . . . . . . 11
⊢
((#‘∅) = 2 ↔ 0 = 2) |
45 | 44, 11 | sylbi 207 |
. . . . . . . . . 10
⊢
((#‘∅) = 2 → 𝑃 = {𝑋, 𝑌}) |
46 | 43, 45 | syl6bi 243 |
. . . . . . . . 9
⊢ (𝑃 = ∅ →
((#‘𝑃) = 2 →
𝑃 = {𝑋, 𝑌})) |
47 | 42, 46 | syl6bi 243 |
. . . . . . . 8
⊢ ({𝑌} = ∅ → (𝑃 = {𝑌} → ((#‘𝑃) = 2 → 𝑃 = {𝑋, 𝑌}))) |
48 | 41, 47 | sylbi 207 |
. . . . . . 7
⊢ (¬
𝑌 ∈ V → (𝑃 = {𝑌} → ((#‘𝑃) = 2 → 𝑃 = {𝑋, 𝑌}))) |
49 | 40, 48 | pm2.61i 176 |
. . . . . 6
⊢ (𝑃 = {𝑌} → ((#‘𝑃) = 2 → 𝑃 = {𝑋, 𝑌})) |
50 | | ax-1 6 |
. . . . . 6
⊢ (𝑃 = {𝑋, 𝑌} → ((#‘𝑃) = 2 → 𝑃 = {𝑋, 𝑌})) |
51 | 49, 50 | jaoi 394 |
. . . . 5
⊢ ((𝑃 = {𝑌} ∨ 𝑃 = {𝑋, 𝑌}) → ((#‘𝑃) = 2 → 𝑃 = {𝑋, 𝑌})) |
52 | 34, 51 | jaoi 394 |
. . . 4
⊢ (((𝑃 = ∅ ∨ 𝑃 = {𝑋}) ∨ (𝑃 = {𝑌} ∨ 𝑃 = {𝑋, 𝑌})) → ((#‘𝑃) = 2 → 𝑃 = {𝑋, 𝑌})) |
53 | | elpri 4197 |
. . . . 5
⊢ (𝑃 ∈ {∅, {𝑋}} → (𝑃 = ∅ ∨ 𝑃 = {𝑋})) |
54 | | elpri 4197 |
. . . . 5
⊢ (𝑃 ∈ {{𝑌}, {𝑋, 𝑌}} → (𝑃 = {𝑌} ∨ 𝑃 = {𝑋, 𝑌})) |
55 | 53, 54 | orim12i 538 |
. . . 4
⊢ ((𝑃 ∈ {∅, {𝑋}} ∨ 𝑃 ∈ {{𝑌}, {𝑋, 𝑌}}) → ((𝑃 = ∅ ∨ 𝑃 = {𝑋}) ∨ (𝑃 = {𝑌} ∨ 𝑃 = {𝑋, 𝑌}))) |
56 | 52, 55 | syl11 33 |
. . 3
⊢
((#‘𝑃) = 2
→ ((𝑃 ∈ {∅,
{𝑋}} ∨ 𝑃 ∈ {{𝑌}, {𝑋, 𝑌}}) → 𝑃 = {𝑋, 𝑌})) |
57 | 4, 56 | syl5bi 232 |
. 2
⊢
((#‘𝑃) = 2
→ (𝑃 ∈ 𝒫
{𝑋, 𝑌} → 𝑃 = {𝑋, 𝑌})) |
58 | 57 | imp 445 |
1
⊢
(((#‘𝑃) = 2
∧ 𝑃 ∈ 𝒫
{𝑋, 𝑌}) → 𝑃 = {𝑋, 𝑌}) |