Step | Hyp | Ref
| Expression |
1 | | eq0 4232 |
. . . . . 6
⊢ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥}) |
2 | | breq2 5034 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝐵 < 𝑥 ↔ 𝐵 < 𝑦)) |
3 | 2 | elrab 3588 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} ↔ (𝑦 ∈ 𝐴 ∧ 𝐵 < 𝑦)) |
4 | 3 | notbii 323 |
. . . . . . . . . 10
⊢ (¬
𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} ↔ ¬ (𝑦 ∈ 𝐴 ∧ 𝐵 < 𝑦)) |
5 | | imnan 403 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐴 → ¬ 𝐵 < 𝑦) ↔ ¬ (𝑦 ∈ 𝐴 ∧ 𝐵 < 𝑦)) |
6 | 4, 5 | sylbb2 241 |
. . . . . . . . 9
⊢ (¬
𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} → (𝑦 ∈ 𝐴 → ¬ 𝐵 < 𝑦)) |
7 | 6 | alimi 1818 |
. . . . . . . 8
⊢
(∀𝑦 ¬
𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} → ∀𝑦(𝑦 ∈ 𝐴 → ¬ 𝐵 < 𝑦)) |
8 | | df-ral 3058 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝐴 ¬ 𝐵 < 𝑦 ↔ ∀𝑦(𝑦 ∈ 𝐴 → ¬ 𝐵 < 𝑦)) |
9 | 7, 8 | sylibr 237 |
. . . . . . 7
⊢
(∀𝑦 ¬
𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} → ∀𝑦 ∈ 𝐴 ¬ 𝐵 < 𝑦) |
10 | | ssel2 3872 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℕ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℕ) |
11 | 10 | nnred 11731 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℕ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ) |
12 | 11 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ) |
13 | | nnre 11723 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ) |
14 | 13 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ ℝ) |
15 | | lenlt 10797 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑦)) |
16 | 15 | biimprd 251 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (¬
𝐵 < 𝑦 → 𝑦 ≤ 𝐵)) |
17 | 12, 14, 16 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) → (¬ 𝐵 < 𝑦 → 𝑦 ≤ 𝐵)) |
18 | 17 | ralimdva 3091 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) →
(∀𝑦 ∈ 𝐴 ¬ 𝐵 < 𝑦 → ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵)) |
19 | | fzfi 13431 |
. . . . . . . . . 10
⊢
(0...𝐵) ∈
Fin |
20 | 10 | nnnn0d 12036 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ⊆ ℕ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℕ0) |
21 | 20 | adantlr 715 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℕ0) |
22 | 21 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ≤ 𝐵) → 𝑦 ∈ ℕ0) |
23 | | nnnn0 11983 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℕ0) |
24 | 23 | ad3antlr 731 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ≤ 𝐵) → 𝐵 ∈
ℕ0) |
25 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ≤ 𝐵) → 𝑦 ≤ 𝐵) |
26 | 22, 24, 25 | 3jca 1129 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ≤ 𝐵) → (𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0
∧ 𝑦 ≤ 𝐵)) |
27 | 26 | ex 416 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) → (𝑦 ≤ 𝐵 → (𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0
∧ 𝑦 ≤ 𝐵))) |
28 | | elfz2nn0 13089 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0...𝐵) ↔ (𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0
∧ 𝑦 ≤ 𝐵)) |
29 | 27, 28 | syl6ibr 255 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) → (𝑦 ≤ 𝐵 → 𝑦 ∈ (0...𝐵))) |
30 | 29 | ralimdva 3091 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) →
(∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵 → ∀𝑦 ∈ 𝐴 𝑦 ∈ (0...𝐵))) |
31 | 30 | imp 410 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧
∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → ∀𝑦 ∈ 𝐴 𝑦 ∈ (0...𝐵)) |
32 | | dfss3 3865 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ (0...𝐵) ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ (0...𝐵)) |
33 | 31, 32 | sylibr 237 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧
∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝐴 ⊆ (0...𝐵)) |
34 | | ssfi 8772 |
. . . . . . . . . 10
⊢
(((0...𝐵) ∈ Fin
∧ 𝐴 ⊆ (0...𝐵)) → 𝐴 ∈ Fin) |
35 | 19, 33, 34 | sylancr 590 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧
∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝐴 ∈ Fin) |
36 | 35 | ex 416 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) →
(∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵 → 𝐴 ∈ Fin)) |
37 | 18, 36 | syld 47 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) →
(∀𝑦 ∈ 𝐴 ¬ 𝐵 < 𝑦 → 𝐴 ∈ Fin)) |
38 | 9, 37 | syl5 34 |
. . . . . 6
⊢ ((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) →
(∀𝑦 ¬ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} → 𝐴 ∈ Fin)) |
39 | 1, 38 | syl5bi 245 |
. . . . 5
⊢ ((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) → ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} = ∅ → 𝐴 ∈ Fin)) |
40 | 39 | necon3bd 2948 |
. . . 4
⊢ ((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) → (¬
𝐴 ∈ Fin → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} ≠ ∅)) |
41 | 40 | imp 410 |
. . 3
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ ¬
𝐴 ∈ Fin) → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} ≠ ∅) |
42 | 41 | an32s 652 |
. 2
⊢ (((𝐴 ⊆ ℕ ∧ ¬
𝐴 ∈ Fin) ∧ 𝐵 ∈ ℕ) → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} ≠ ∅) |
43 | 42 | 3impa 1111 |
1
⊢ ((𝐴 ⊆ ℕ ∧ ¬
𝐴 ∈ Fin ∧ 𝐵 ∈ ℕ) → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} ≠ ∅) |