Step |
Hyp |
Ref |
Expression |
1 |
|
eq0 |
⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } = ∅ ↔ ∀ 𝑦 ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } ) |
2 |
|
breq2 |
⊢ ( 𝑥 = 𝑦 → ( 𝐵 < 𝑥 ↔ 𝐵 < 𝑦 ) ) |
3 |
2
|
elrab |
⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } ↔ ( 𝑦 ∈ 𝐴 ∧ 𝐵 < 𝑦 ) ) |
4 |
3
|
notbii |
⊢ ( ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } ↔ ¬ ( 𝑦 ∈ 𝐴 ∧ 𝐵 < 𝑦 ) ) |
5 |
|
imnan |
⊢ ( ( 𝑦 ∈ 𝐴 → ¬ 𝐵 < 𝑦 ) ↔ ¬ ( 𝑦 ∈ 𝐴 ∧ 𝐵 < 𝑦 ) ) |
6 |
4 5
|
sylbb2 |
⊢ ( ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } → ( 𝑦 ∈ 𝐴 → ¬ 𝐵 < 𝑦 ) ) |
7 |
6
|
alimi |
⊢ ( ∀ 𝑦 ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } → ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ¬ 𝐵 < 𝑦 ) ) |
8 |
|
df-ral |
⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝐵 < 𝑦 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → ¬ 𝐵 < 𝑦 ) ) |
9 |
7 8
|
sylibr |
⊢ ( ∀ 𝑦 ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } → ∀ 𝑦 ∈ 𝐴 ¬ 𝐵 < 𝑦 ) |
10 |
|
ssel2 |
⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℕ ) |
11 |
10
|
nnred |
⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ ) |
12 |
11
|
adantlr |
⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ ) |
13 |
|
nnre |
⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℝ ) |
14 |
13
|
ad2antlr |
⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) → 𝐵 ∈ ℝ ) |
15 |
|
lenlt |
⊢ ( ( 𝑦 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑦 ≤ 𝐵 ↔ ¬ 𝐵 < 𝑦 ) ) |
16 |
15
|
biimprd |
⊢ ( ( 𝑦 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ¬ 𝐵 < 𝑦 → 𝑦 ≤ 𝐵 ) ) |
17 |
12 14 16
|
syl2anc |
⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝐵 < 𝑦 → 𝑦 ≤ 𝐵 ) ) |
18 |
17
|
ralimdva |
⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝐵 < 𝑦 → ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝐵 ) ) |
19 |
|
fzfi |
⊢ ( 0 ... 𝐵 ) ∈ Fin |
20 |
10
|
nnnn0d |
⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℕ0 ) |
21 |
20
|
adantlr |
⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℕ0 ) |
22 |
21
|
adantr |
⊢ ( ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 ≤ 𝐵 ) → 𝑦 ∈ ℕ0 ) |
23 |
|
nnnn0 |
⊢ ( 𝐵 ∈ ℕ → 𝐵 ∈ ℕ0 ) |
24 |
23
|
ad3antlr |
⊢ ( ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 ≤ 𝐵 ) → 𝐵 ∈ ℕ0 ) |
25 |
|
simpr |
⊢ ( ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 ≤ 𝐵 ) → 𝑦 ≤ 𝐵 ) |
26 |
22 24 25
|
3jca |
⊢ ( ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑦 ≤ 𝐵 ) → ( 𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑦 ≤ 𝐵 ) ) |
27 |
26
|
ex |
⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ≤ 𝐵 → ( 𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑦 ≤ 𝐵 ) ) ) |
28 |
|
elfz2nn0 |
⊢ ( 𝑦 ∈ ( 0 ... 𝐵 ) ↔ ( 𝑦 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0 ∧ 𝑦 ≤ 𝐵 ) ) |
29 |
27 28
|
syl6ibr |
⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ≤ 𝐵 → 𝑦 ∈ ( 0 ... 𝐵 ) ) ) |
30 |
29
|
ralimdva |
⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝐵 → ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ( 0 ... 𝐵 ) ) ) |
31 |
30
|
imp |
⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝐵 ) → ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ( 0 ... 𝐵 ) ) |
32 |
|
dfss3 |
⊢ ( 𝐴 ⊆ ( 0 ... 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐴 𝑦 ∈ ( 0 ... 𝐵 ) ) |
33 |
31 32
|
sylibr |
⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝐵 ) → 𝐴 ⊆ ( 0 ... 𝐵 ) ) |
34 |
|
ssfi |
⊢ ( ( ( 0 ... 𝐵 ) ∈ Fin ∧ 𝐴 ⊆ ( 0 ... 𝐵 ) ) → 𝐴 ∈ Fin ) |
35 |
19 33 34
|
sylancr |
⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝐵 ) → 𝐴 ∈ Fin ) |
36 |
35
|
ex |
⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑦 ∈ 𝐴 𝑦 ≤ 𝐵 → 𝐴 ∈ Fin ) ) |
37 |
18 36
|
syld |
⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝐵 < 𝑦 → 𝐴 ∈ Fin ) ) |
38 |
9 37
|
syl5 |
⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ∀ 𝑦 ¬ 𝑦 ∈ { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } → 𝐴 ∈ Fin ) ) |
39 |
1 38
|
syl5bi |
⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } = ∅ → 𝐴 ∈ Fin ) ) |
40 |
39
|
necon3bd |
⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) → ( ¬ 𝐴 ∈ Fin → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } ≠ ∅ ) ) |
41 |
40
|
imp |
⊢ ( ( ( 𝐴 ⊆ ℕ ∧ 𝐵 ∈ ℕ ) ∧ ¬ 𝐴 ∈ Fin ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } ≠ ∅ ) |
42 |
41
|
an32s |
⊢ ( ( ( 𝐴 ⊆ ℕ ∧ ¬ 𝐴 ∈ Fin ) ∧ 𝐵 ∈ ℕ ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } ≠ ∅ ) |
43 |
42
|
3impa |
⊢ ( ( 𝐴 ⊆ ℕ ∧ ¬ 𝐴 ∈ Fin ∧ 𝐵 ∈ ℕ ) → { 𝑥 ∈ 𝐴 ∣ 𝐵 < 𝑥 } ≠ ∅ ) |