Proof of Theorem hashgt12el2
Step | Hyp | Ref
| Expression |
1 | | hash0 13019 |
. . . 4
⊢
(#‘∅) = 0 |
2 | | fveq2 6103 |
. . . 4
⊢ (∅
= 𝑉 →
(#‘∅) = (#‘𝑉)) |
3 | 1, 2 | syl5eqr 2658 |
. . 3
⊢ (∅
= 𝑉 → 0 =
(#‘𝑉)) |
4 | | breq2 4587 |
. . . . . . 7
⊢
((#‘𝑉) = 0
→ (1 < (#‘𝑉)
↔ 1 < 0)) |
5 | 4 | biimpd 218 |
. . . . . 6
⊢
((#‘𝑉) = 0
→ (1 < (#‘𝑉)
→ 1 < 0)) |
6 | 5 | eqcoms 2618 |
. . . . 5
⊢ (0 =
(#‘𝑉) → (1 <
(#‘𝑉) → 1 <
0)) |
7 | | 0le1 10430 |
. . . . . 6
⊢ 0 ≤
1 |
8 | | 0re 9919 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
9 | | 1re 9918 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
10 | 8, 9 | lenlti 10036 |
. . . . . . 7
⊢ (0 ≤ 1
↔ ¬ 1 < 0) |
11 | | pm2.21 119 |
. . . . . . 7
⊢ (¬ 1
< 0 → (1 < 0 → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
12 | 10, 11 | sylbi 206 |
. . . . . 6
⊢ (0 ≤ 1
→ (1 < 0 → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
13 | 7, 12 | ax-mp 5 |
. . . . 5
⊢ (1 < 0
→ ∃𝑏 ∈
𝑉 𝐴 ≠ 𝑏) |
14 | 6, 13 | syl6com 36 |
. . . 4
⊢ (1 <
(#‘𝑉) → (0 =
(#‘𝑉) →
∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
15 | 14 | 3ad2ant2 1076 |
. . 3
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (#‘𝑉) ∧ 𝐴 ∈ 𝑉) → (0 = (#‘𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
16 | 3, 15 | syl5com 31 |
. 2
⊢ (∅
= 𝑉 → ((𝑉 ∈ 𝑊 ∧ 1 < (#‘𝑉) ∧ 𝐴 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
17 | | df-ne 2782 |
. . . 4
⊢ (∅
≠ 𝑉 ↔ ¬ ∅
= 𝑉) |
18 | | necom 2835 |
. . . 4
⊢ (∅
≠ 𝑉 ↔ 𝑉 ≠ ∅) |
19 | 17, 18 | bitr3i 265 |
. . 3
⊢ (¬
∅ = 𝑉 ↔ 𝑉 ≠ ∅) |
20 | | ralnex 2975 |
. . . . . . . . . 10
⊢
(∀𝑏 ∈
𝑉 ¬ 𝐴 ≠ 𝑏 ↔ ¬ ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏) |
21 | | nne 2786 |
. . . . . . . . . . . 12
⊢ (¬
𝐴 ≠ 𝑏 ↔ 𝐴 = 𝑏) |
22 | | eqcom 2617 |
. . . . . . . . . . . 12
⊢ (𝐴 = 𝑏 ↔ 𝑏 = 𝐴) |
23 | 21, 22 | bitri 263 |
. . . . . . . . . . 11
⊢ (¬
𝐴 ≠ 𝑏 ↔ 𝑏 = 𝐴) |
24 | 23 | ralbii 2963 |
. . . . . . . . . 10
⊢
(∀𝑏 ∈
𝑉 ¬ 𝐴 ≠ 𝑏 ↔ ∀𝑏 ∈ 𝑉 𝑏 = 𝐴) |
25 | 20, 24 | bitr3i 265 |
. . . . . . . . 9
⊢ (¬
∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ↔ ∀𝑏 ∈ 𝑉 𝑏 = 𝐴) |
26 | | eqsn 4301 |
. . . . . . . . . . . . . 14
⊢ (𝑉 ≠ ∅ → (𝑉 = {𝐴} ↔ ∀𝑏 ∈ 𝑉 𝑏 = 𝐴)) |
27 | 26 | bicomd 212 |
. . . . . . . . . . . . 13
⊢ (𝑉 ≠ ∅ →
(∀𝑏 ∈ 𝑉 𝑏 = 𝐴 ↔ 𝑉 = {𝐴})) |
28 | 27 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) → (∀𝑏 ∈ 𝑉 𝑏 = 𝐴 ↔ 𝑉 = {𝐴})) |
29 | 28 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) → (∀𝑏 ∈ 𝑉 𝑏 = 𝐴 ↔ 𝑉 = {𝐴})) |
30 | | hashsnle1 13066 |
. . . . . . . . . . . . 13
⊢
(#‘{𝐴}) ≤
1 |
31 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 = {𝐴} → (#‘𝑉) = (#‘{𝐴})) |
32 | 31 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ (𝑉 = {𝐴} → ((#‘𝑉) ≤ 1 ↔ (#‘{𝐴}) ≤ 1)) |
33 | 32 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) ∧ 𝑉 = {𝐴}) → ((#‘𝑉) ≤ 1 ↔ (#‘{𝐴}) ≤ 1)) |
34 | 30, 33 | mpbiri 247 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) ∧ 𝑉 = {𝐴}) → (#‘𝑉) ≤ 1) |
35 | 34 | ex 449 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) → (𝑉 = {𝐴} → (#‘𝑉) ≤ 1)) |
36 | 29, 35 | sylbid 229 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) → (∀𝑏 ∈ 𝑉 𝑏 = 𝐴 → (#‘𝑉) ≤ 1)) |
37 | | hashxrcl 13010 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ 𝑊 → (#‘𝑉) ∈
ℝ*) |
38 | 37 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) → (#‘𝑉) ∈
ℝ*) |
39 | 38 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) → (#‘𝑉) ∈
ℝ*) |
40 | 9 | rexri 9976 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ* |
41 | | xrlenlt 9982 |
. . . . . . . . . . 11
⊢
(((#‘𝑉) ∈
ℝ* ∧ 1 ∈ ℝ*) → ((#‘𝑉) ≤ 1 ↔ ¬ 1 <
(#‘𝑉))) |
42 | 39, 40, 41 | sylancl 693 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) → ((#‘𝑉) ≤ 1 ↔ ¬ 1 < (#‘𝑉))) |
43 | 36, 42 | sylibd 228 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) → (∀𝑏 ∈ 𝑉 𝑏 = 𝐴 → ¬ 1 < (#‘𝑉))) |
44 | 25, 43 | syl5bi 231 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) → (¬ ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 → ¬ 1 < (#‘𝑉))) |
45 | 44 | con4d 113 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) → (1 < (#‘𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
46 | 45 | exp31 628 |
. . . . . 6
⊢ (𝑉 ∈ 𝑊 → (𝑉 ≠ ∅ → (𝐴 ∈ 𝑉 → (1 < (#‘𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)))) |
47 | 46 | com24 93 |
. . . . 5
⊢ (𝑉 ∈ 𝑊 → (1 < (#‘𝑉) → (𝐴 ∈ 𝑉 → (𝑉 ≠ ∅ → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)))) |
48 | 47 | 3imp 1249 |
. . . 4
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (#‘𝑉) ∧ 𝐴 ∈ 𝑉) → (𝑉 ≠ ∅ → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
49 | 48 | com12 32 |
. . 3
⊢ (𝑉 ≠ ∅ → ((𝑉 ∈ 𝑊 ∧ 1 < (#‘𝑉) ∧ 𝐴 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
50 | 19, 49 | sylbi 206 |
. 2
⊢ (¬
∅ = 𝑉 → ((𝑉 ∈ 𝑊 ∧ 1 < (#‘𝑉) ∧ 𝐴 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
51 | 16, 50 | pm2.61i 175 |
1
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (#‘𝑉) ∧ 𝐴 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏) |