Step | Hyp | Ref
| Expression |
1 | | suppssfz.b |
. 2
⊢ (𝜑 → ∀𝑥 ∈ ℕ0 (𝑆 < 𝑥 → (𝐹‘𝑥) = 𝑍)) |
2 | | suppssfz.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (𝐵 ↑𝑚
ℕ0)) |
3 | | elmapfn 7880 |
. . . . . . . 8
⊢ (𝐹 ∈ (𝐵 ↑𝑚
ℕ0) → 𝐹 Fn ℕ0) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn ℕ0) |
5 | | nn0ex 11298 |
. . . . . . . 8
⊢
ℕ0 ∈ V |
6 | 5 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ℕ0 ∈
V) |
7 | | suppssfz.z |
. . . . . . 7
⊢ (𝜑 → 𝑍 ∈ 𝑉) |
8 | 4, 6, 7 | 3jca 1242 |
. . . . . 6
⊢ (𝜑 → (𝐹 Fn ℕ0 ∧
ℕ0 ∈ V ∧ 𝑍 ∈ 𝑉)) |
9 | 8 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℕ0 (𝑆 < 𝑥 → (𝐹‘𝑥) = 𝑍)) → (𝐹 Fn ℕ0 ∧
ℕ0 ∈ V ∧ 𝑍 ∈ 𝑉)) |
10 | | elsuppfn 7303 |
. . . . 5
⊢ ((𝐹 Fn ℕ0 ∧
ℕ0 ∈ V ∧ 𝑍 ∈ 𝑉) → (𝑛 ∈ (𝐹 supp 𝑍) ↔ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≠ 𝑍))) |
11 | 9, 10 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℕ0 (𝑆 < 𝑥 → (𝐹‘𝑥) = 𝑍)) → (𝑛 ∈ (𝐹 supp 𝑍) ↔ (𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≠ 𝑍))) |
12 | | breq2 4657 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑛 → (𝑆 < 𝑥 ↔ 𝑆 < 𝑛)) |
13 | | fveq2 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑛 → (𝐹‘𝑥) = (𝐹‘𝑛)) |
14 | 13 | eqeq1d 2624 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑛 → ((𝐹‘𝑥) = 𝑍 ↔ (𝐹‘𝑛) = 𝑍)) |
15 | 12, 14 | imbi12d 334 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑛 → ((𝑆 < 𝑥 → (𝐹‘𝑥) = 𝑍) ↔ (𝑆 < 𝑛 → (𝐹‘𝑛) = 𝑍))) |
16 | 15 | rspcva 3307 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑆 <
𝑥 → (𝐹‘𝑥) = 𝑍)) → (𝑆 < 𝑛 → (𝐹‘𝑛) = 𝑍)) |
17 | | simplr 792 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑆 < 𝑛) → 𝑛 ∈ ℕ0) |
18 | | suppssfz.s |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑆 ∈
ℕ0) |
19 | 18 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → 𝑆 ∈
ℕ0) |
20 | 19 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑆 < 𝑛) → 𝑆 ∈
ℕ0) |
21 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℕ0
→ 𝑛 ∈
ℝ) |
22 | | nn0re 11301 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑆 ∈ ℕ0
→ 𝑆 ∈
ℝ) |
23 | 18, 22 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝑆 ∈ ℝ) |
24 | | lenlt 10116 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 ∈ ℝ ∧ 𝑆 ∈ ℝ) → (𝑛 ≤ 𝑆 ↔ ¬ 𝑆 < 𝑛)) |
25 | 21, 23, 24 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝑛 ≤ 𝑆 ↔ ¬ 𝑆 < 𝑛)) |
26 | 25 | biimpar 502 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑆 < 𝑛) → 𝑛 ≤ 𝑆) |
27 | | elfz2nn0 12431 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈ (0...𝑆) ↔ (𝑛 ∈ ℕ0 ∧ 𝑆 ∈ ℕ0
∧ 𝑛 ≤ 𝑆)) |
28 | 17, 20, 26, 27 | syl3anbrc 1246 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑆 < 𝑛) → 𝑛 ∈ (0...𝑆)) |
29 | 28 | a1d 25 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑛 ∈ ℕ0) ∧ ¬
𝑆 < 𝑛) → ((𝐹‘𝑛) ≠ 𝑍 → 𝑛 ∈ (0...𝑆))) |
30 | 29 | ex 450 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (¬
𝑆 < 𝑛 → ((𝐹‘𝑛) ≠ 𝑍 → 𝑛 ∈ (0...𝑆)))) |
31 | | eqneqall 2805 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑛) = 𝑍 → ((𝐹‘𝑛) ≠ 𝑍 → 𝑛 ∈ (0...𝑆))) |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝐹‘𝑛) = 𝑍 → ((𝐹‘𝑛) ≠ 𝑍 → 𝑛 ∈ (0...𝑆)))) |
33 | 30, 32 | jad 174 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝑆 < 𝑛 → (𝐹‘𝑛) = 𝑍) → ((𝐹‘𝑛) ≠ 𝑍 → 𝑛 ∈ (0...𝑆)))) |
34 | 33 | com23 86 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → ((𝐹‘𝑛) ≠ 𝑍 → ((𝑆 < 𝑛 → (𝐹‘𝑛) = 𝑍) → 𝑛 ∈ (0...𝑆)))) |
35 | 34 | ex 450 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑛 ∈ ℕ0 → ((𝐹‘𝑛) ≠ 𝑍 → ((𝑆 < 𝑛 → (𝐹‘𝑛) = 𝑍) → 𝑛 ∈ (0...𝑆))))) |
36 | 35 | com14 96 |
. . . . . . . . . . 11
⊢ ((𝑆 < 𝑛 → (𝐹‘𝑛) = 𝑍) → (𝑛 ∈ ℕ0 → ((𝐹‘𝑛) ≠ 𝑍 → (𝜑 → 𝑛 ∈ (0...𝑆))))) |
37 | 16, 36 | syl 17 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ0
∧ ∀𝑥 ∈
ℕ0 (𝑆 <
𝑥 → (𝐹‘𝑥) = 𝑍)) → (𝑛 ∈ ℕ0 → ((𝐹‘𝑛) ≠ 𝑍 → (𝜑 → 𝑛 ∈ (0...𝑆))))) |
38 | 37 | ex 450 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ0
→ (∀𝑥 ∈
ℕ0 (𝑆 <
𝑥 → (𝐹‘𝑥) = 𝑍) → (𝑛 ∈ ℕ0 → ((𝐹‘𝑛) ≠ 𝑍 → (𝜑 → 𝑛 ∈ (0...𝑆)))))) |
39 | 38 | pm2.43a 54 |
. . . . . . . 8
⊢ (𝑛 ∈ ℕ0
→ (∀𝑥 ∈
ℕ0 (𝑆 <
𝑥 → (𝐹‘𝑥) = 𝑍) → ((𝐹‘𝑛) ≠ 𝑍 → (𝜑 → 𝑛 ∈ (0...𝑆))))) |
40 | 39 | com23 86 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ ((𝐹‘𝑛) ≠ 𝑍 → (∀𝑥 ∈ ℕ0 (𝑆 < 𝑥 → (𝐹‘𝑥) = 𝑍) → (𝜑 → 𝑛 ∈ (0...𝑆))))) |
41 | 40 | imp 445 |
. . . . . 6
⊢ ((𝑛 ∈ ℕ0
∧ (𝐹‘𝑛) ≠ 𝑍) → (∀𝑥 ∈ ℕ0 (𝑆 < 𝑥 → (𝐹‘𝑥) = 𝑍) → (𝜑 → 𝑛 ∈ (0...𝑆)))) |
42 | 41 | com13 88 |
. . . . 5
⊢ (𝜑 → (∀𝑥 ∈ ℕ0
(𝑆 < 𝑥 → (𝐹‘𝑥) = 𝑍) → ((𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≠ 𝑍) → 𝑛 ∈ (0...𝑆)))) |
43 | 42 | imp 445 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℕ0 (𝑆 < 𝑥 → (𝐹‘𝑥) = 𝑍)) → ((𝑛 ∈ ℕ0 ∧ (𝐹‘𝑛) ≠ 𝑍) → 𝑛 ∈ (0...𝑆))) |
44 | 11, 43 | sylbid 230 |
. . 3
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℕ0 (𝑆 < 𝑥 → (𝐹‘𝑥) = 𝑍)) → (𝑛 ∈ (𝐹 supp 𝑍) → 𝑛 ∈ (0...𝑆))) |
45 | 44 | ssrdv 3609 |
. 2
⊢ ((𝜑 ∧ ∀𝑥 ∈ ℕ0 (𝑆 < 𝑥 → (𝐹‘𝑥) = 𝑍)) → (𝐹 supp 𝑍) ⊆ (0...𝑆)) |
46 | 1, 45 | mpdan 702 |
1
⊢ (𝜑 → (𝐹 supp 𝑍) ⊆ (0...𝑆)) |