Step | Hyp | Ref
| Expression |
1 | | eq0 4277 |
. . . . . 6
⊢ ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥}) |
2 | | breq2 5078 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → (𝐵 < 𝑥 ↔ 𝐵 < 𝑦)) |
3 | 2 | elrab 3624 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} ↔ (𝑦 ∈ 𝐴 ∧ 𝐵 < 𝑦)) |
4 | 3 | notbii 320 |
. . . . . . . . . 10
⊢ (¬
𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} ↔ ¬ (𝑦 ∈ 𝐴 ∧ 𝐵 < 𝑦)) |
5 | | imnan 400 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐴 → ¬ 𝐵 < 𝑦) ↔ ¬ (𝑦 ∈ 𝐴 ∧ 𝐵 < 𝑦)) |
6 | 4, 5 | sylbb2 237 |
. . . . . . . . 9
⊢ (¬
𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} → (𝑦 ∈ 𝐴 → ¬ 𝐵 < 𝑦)) |
7 | 6 | alimi 1814 |
. . . . . . . 8
⊢
(∀𝑦 ¬
𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} → ∀𝑦(𝑦 ∈ 𝐴 → ¬ 𝐵 < 𝑦)) |
8 | | df-ral 3069 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝐴 ¬ 𝐵 < 𝑦 ↔ ∀𝑦(𝑦 ∈ 𝐴 → ¬ 𝐵 < 𝑦)) |
9 | 7, 8 | sylibr 233 |
. . . . . . 7
⊢
(∀𝑦 ¬
𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} → ∀𝑦 ∈ 𝐴 ¬ 𝐵 < 𝑦) |
10 | | ssel2 3916 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℕ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℕ) |
11 | 10 | nnred 11988 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℕ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ) |
12 | 11 | adantlr 712 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ) |
13 | | nnre 11980 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ) |
14 | 13 | ad2antlr 724 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) → 𝐵 ∈ ℝ) |
15 | | lenlt 11053 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝑦 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑦)) |
16 | 15 | biimprd 247 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (¬
𝐵 < 𝑦 → 𝑦 ≤ 𝐵)) |
17 | 12, 14, 16 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) → (¬ 𝐵 < 𝑦 → 𝑦 ≤ 𝐵)) |
18 | 17 | ralimdva 3108 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) →
(∀𝑦 ∈ 𝐴 ¬ 𝐵 < 𝑦 → ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵)) |
19 | | fzfi 13692 |
. . . . . . . . . 10
⊢
(0...𝐵) ∈
Fin |
20 | 10 | nnnn0d 12293 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐴 ⊆ ℕ ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℕ0) |
21 | 20 | adantlr 712 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℕ0) |
22 | 21 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ≤ 𝐵) → 𝑦 ∈ ℕ0) |
23 | | nnnn0 12240 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℕ0) |
24 | 23 | ad3antlr 728 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ≤ 𝐵) → 𝐵 ∈
ℕ0) |
25 | | simpr 485 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ≤ 𝐵) → 𝑦 ≤ 𝐵) |
26 | 22, 24, 25 | 3jca 1127 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) ∧ 𝑦 ≤ 𝐵) → (𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0
∧ 𝑦 ≤ 𝐵)) |
27 | 26 | ex 413 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) → (𝑦 ≤ 𝐵 → (𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0
∧ 𝑦 ≤ 𝐵))) |
28 | | elfz2nn0 13347 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (0...𝐵) ↔ (𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0
∧ 𝑦 ≤ 𝐵)) |
29 | 27, 28 | syl6ibr 251 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ 𝑦 ∈ 𝐴) → (𝑦 ≤ 𝐵 → 𝑦 ∈ (0...𝐵))) |
30 | 29 | ralimdva 3108 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) →
(∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵 → ∀𝑦 ∈ 𝐴 𝑦 ∈ (0...𝐵))) |
31 | 30 | imp 407 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧
∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → ∀𝑦 ∈ 𝐴 𝑦 ∈ (0...𝐵)) |
32 | | dfss3 3909 |
. . . . . . . . . . 11
⊢ (𝐴 ⊆ (0...𝐵) ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ (0...𝐵)) |
33 | 31, 32 | sylibr 233 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧
∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝐴 ⊆ (0...𝐵)) |
34 | | ssfi 8956 |
. . . . . . . . . 10
⊢
(((0...𝐵) ∈ Fin
∧ 𝐴 ⊆ (0...𝐵)) → 𝐴 ∈ Fin) |
35 | 19, 33, 34 | sylancr 587 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧
∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵) → 𝐴 ∈ Fin) |
36 | 35 | ex 413 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) →
(∀𝑦 ∈ 𝐴 𝑦 ≤ 𝐵 → 𝐴 ∈ Fin)) |
37 | 18, 36 | syld 47 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) →
(∀𝑦 ∈ 𝐴 ¬ 𝐵 < 𝑦 → 𝐴 ∈ Fin)) |
38 | 9, 37 | syl5 34 |
. . . . . 6
⊢ ((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) →
(∀𝑦 ¬ 𝑦 ∈ {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} → 𝐴 ∈ Fin)) |
39 | 1, 38 | syl5bi 241 |
. . . . 5
⊢ ((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) → ({𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} = ∅ → 𝐴 ∈ Fin)) |
40 | 39 | necon3bd 2957 |
. . . 4
⊢ ((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) → (¬
𝐴 ∈ Fin → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} ≠ ∅)) |
41 | 40 | imp 407 |
. . 3
⊢ (((𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ) ∧ ¬
𝐴 ∈ Fin) → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} ≠ ∅) |
42 | 41 | an32s 649 |
. 2
⊢ (((𝐴 ⊆ ℕ ∧ ¬
𝐴 ∈ Fin) ∧ 𝐵 ∈ ℕ) → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} ≠ ∅) |
43 | 42 | 3impa 1109 |
1
⊢ ((𝐴 ⊆ ℕ ∧ ¬
𝐴 ∈ Fin ∧ 𝐵 ∈ ℕ) → {𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥} ≠ ∅) |