Proof of Theorem hashgt12el2
| Step | Hyp | Ref
| Expression |
| 1 | | hash0 14406 |
. . . 4
⊢
(♯‘∅) = 0 |
| 2 | | fveq2 6906 |
. . . 4
⊢ (∅
= 𝑉 →
(♯‘∅) = (♯‘𝑉)) |
| 3 | 1, 2 | eqtr3id 2791 |
. . 3
⊢ (∅
= 𝑉 → 0 =
(♯‘𝑉)) |
| 4 | | breq2 5147 |
. . . . . . 7
⊢
((♯‘𝑉) =
0 → (1 < (♯‘𝑉) ↔ 1 < 0)) |
| 5 | 4 | biimpd 229 |
. . . . . 6
⊢
((♯‘𝑉) =
0 → (1 < (♯‘𝑉) → 1 < 0)) |
| 6 | 5 | eqcoms 2745 |
. . . . 5
⊢ (0 =
(♯‘𝑉) → (1
< (♯‘𝑉)
→ 1 < 0)) |
| 7 | | 0le1 11786 |
. . . . . 6
⊢ 0 ≤
1 |
| 8 | | 0re 11263 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
| 9 | | 1re 11261 |
. . . . . . . 8
⊢ 1 ∈
ℝ |
| 10 | 8, 9 | lenlti 11381 |
. . . . . . 7
⊢ (0 ≤ 1
↔ ¬ 1 < 0) |
| 11 | | pm2.21 123 |
. . . . . . 7
⊢ (¬ 1
< 0 → (1 < 0 → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
| 12 | 10, 11 | sylbi 217 |
. . . . . 6
⊢ (0 ≤ 1
→ (1 < 0 → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
| 13 | 7, 12 | ax-mp 5 |
. . . . 5
⊢ (1 < 0
→ ∃𝑏 ∈
𝑉 𝐴 ≠ 𝑏) |
| 14 | 6, 13 | syl6com 37 |
. . . 4
⊢ (1 <
(♯‘𝑉) → (0
= (♯‘𝑉) →
∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
| 15 | 14 | 3ad2ant2 1135 |
. . 3
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (♯‘𝑉) ∧ 𝐴 ∈ 𝑉) → (0 = (♯‘𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
| 16 | 3, 15 | syl5com 31 |
. 2
⊢ (∅
= 𝑉 → ((𝑉 ∈ 𝑊 ∧ 1 < (♯‘𝑉) ∧ 𝐴 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
| 17 | | df-ne 2941 |
. . . 4
⊢ (∅
≠ 𝑉 ↔ ¬ ∅
= 𝑉) |
| 18 | | necom 2994 |
. . . 4
⊢ (∅
≠ 𝑉 ↔ 𝑉 ≠ ∅) |
| 19 | 17, 18 | bitr3i 277 |
. . 3
⊢ (¬
∅ = 𝑉 ↔ 𝑉 ≠ ∅) |
| 20 | | ralnex 3072 |
. . . . . . . . . 10
⊢
(∀𝑏 ∈
𝑉 ¬ 𝐴 ≠ 𝑏 ↔ ¬ ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏) |
| 21 | | nne 2944 |
. . . . . . . . . . . 12
⊢ (¬
𝐴 ≠ 𝑏 ↔ 𝐴 = 𝑏) |
| 22 | | eqcom 2744 |
. . . . . . . . . . . 12
⊢ (𝐴 = 𝑏 ↔ 𝑏 = 𝐴) |
| 23 | 21, 22 | bitri 275 |
. . . . . . . . . . 11
⊢ (¬
𝐴 ≠ 𝑏 ↔ 𝑏 = 𝐴) |
| 24 | 23 | ralbii 3093 |
. . . . . . . . . 10
⊢
(∀𝑏 ∈
𝑉 ¬ 𝐴 ≠ 𝑏 ↔ ∀𝑏 ∈ 𝑉 𝑏 = 𝐴) |
| 25 | 20, 24 | bitr3i 277 |
. . . . . . . . 9
⊢ (¬
∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 ↔ ∀𝑏 ∈ 𝑉 𝑏 = 𝐴) |
| 26 | | eqsn 4829 |
. . . . . . . . . . . . . 14
⊢ (𝑉 ≠ ∅ → (𝑉 = {𝐴} ↔ ∀𝑏 ∈ 𝑉 𝑏 = 𝐴)) |
| 27 | 26 | bicomd 223 |
. . . . . . . . . . . . 13
⊢ (𝑉 ≠ ∅ →
(∀𝑏 ∈ 𝑉 𝑏 = 𝐴 ↔ 𝑉 = {𝐴})) |
| 28 | 27 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) → (∀𝑏 ∈ 𝑉 𝑏 = 𝐴 ↔ 𝑉 = {𝐴})) |
| 29 | 28 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) → (∀𝑏 ∈ 𝑉 𝑏 = 𝐴 ↔ 𝑉 = {𝐴})) |
| 30 | | hashsnle1 14456 |
. . . . . . . . . . . . 13
⊢
(♯‘{𝐴})
≤ 1 |
| 31 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 = {𝐴} → (♯‘𝑉) = (♯‘{𝐴})) |
| 32 | 31 | breq1d 5153 |
. . . . . . . . . . . . . 14
⊢ (𝑉 = {𝐴} → ((♯‘𝑉) ≤ 1 ↔ (♯‘{𝐴}) ≤ 1)) |
| 33 | 32 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) ∧ 𝑉 = {𝐴}) → ((♯‘𝑉) ≤ 1 ↔ (♯‘{𝐴}) ≤ 1)) |
| 34 | 30, 33 | mpbiri 258 |
. . . . . . . . . . . 12
⊢ ((((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) ∧ 𝑉 = {𝐴}) → (♯‘𝑉) ≤ 1) |
| 35 | 34 | ex 412 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) → (𝑉 = {𝐴} → (♯‘𝑉) ≤ 1)) |
| 36 | 29, 35 | sylbid 240 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) → (∀𝑏 ∈ 𝑉 𝑏 = 𝐴 → (♯‘𝑉) ≤ 1)) |
| 37 | | hashxrcl 14396 |
. . . . . . . . . . . . 13
⊢ (𝑉 ∈ 𝑊 → (♯‘𝑉) ∈
ℝ*) |
| 38 | 37 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) → (♯‘𝑉) ∈
ℝ*) |
| 39 | 38 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) → (♯‘𝑉) ∈
ℝ*) |
| 40 | | 1xr 11320 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ* |
| 41 | | xrlenlt 11326 |
. . . . . . . . . . 11
⊢
(((♯‘𝑉)
∈ ℝ* ∧ 1 ∈ ℝ*) →
((♯‘𝑉) ≤ 1
↔ ¬ 1 < (♯‘𝑉))) |
| 42 | 39, 40, 41 | sylancl 586 |
. . . . . . . . . 10
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) → ((♯‘𝑉) ≤ 1 ↔ ¬ 1 <
(♯‘𝑉))) |
| 43 | 36, 42 | sylibd 239 |
. . . . . . . . 9
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) → (∀𝑏 ∈ 𝑉 𝑏 = 𝐴 → ¬ 1 < (♯‘𝑉))) |
| 44 | 25, 43 | biimtrid 242 |
. . . . . . . 8
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) → (¬ ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏 → ¬ 1 < (♯‘𝑉))) |
| 45 | 44 | con4d 115 |
. . . . . . 7
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑉 ≠ ∅) ∧ 𝐴 ∈ 𝑉) → (1 < (♯‘𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
| 46 | 45 | exp31 419 |
. . . . . 6
⊢ (𝑉 ∈ 𝑊 → (𝑉 ≠ ∅ → (𝐴 ∈ 𝑉 → (1 < (♯‘𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)))) |
| 47 | 46 | com24 95 |
. . . . 5
⊢ (𝑉 ∈ 𝑊 → (1 < (♯‘𝑉) → (𝐴 ∈ 𝑉 → (𝑉 ≠ ∅ → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)))) |
| 48 | 47 | 3imp 1111 |
. . . 4
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (♯‘𝑉) ∧ 𝐴 ∈ 𝑉) → (𝑉 ≠ ∅ → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
| 49 | 48 | com12 32 |
. . 3
⊢ (𝑉 ≠ ∅ → ((𝑉 ∈ 𝑊 ∧ 1 < (♯‘𝑉) ∧ 𝐴 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
| 50 | 19, 49 | sylbi 217 |
. 2
⊢ (¬
∅ = 𝑉 → ((𝑉 ∈ 𝑊 ∧ 1 < (♯‘𝑉) ∧ 𝐴 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏)) |
| 51 | 16, 50 | pm2.61i 182 |
1
⊢ ((𝑉 ∈ 𝑊 ∧ 1 < (♯‘𝑉) ∧ 𝐴 ∈ 𝑉) → ∃𝑏 ∈ 𝑉 𝐴 ≠ 𝑏) |