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