Step | Hyp | Ref
| Expression |
1 | | fveq2 6717 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (𝐹‘𝑎) = (𝐹‘𝐴)) |
2 | 1 | sseq2d 3933 |
. . . . 5
⊢ (𝑎 = 𝐴 → ((𝐹‘𝐴) ⊆ (𝐹‘𝑎) ↔ (𝐹‘𝐴) ⊆ (𝐹‘𝐴))) |
3 | 2 | imbi2d 344 |
. . . 4
⊢ (𝑎 = 𝐴 → (((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0) → (𝐹‘𝐴) ⊆ (𝐹‘𝑎)) ↔ ((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0) → (𝐹‘𝐴) ⊆ (𝐹‘𝐴)))) |
4 | | fveq2 6717 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (𝐹‘𝑎) = (𝐹‘𝑏)) |
5 | 4 | sseq2d 3933 |
. . . . 5
⊢ (𝑎 = 𝑏 → ((𝐹‘𝐴) ⊆ (𝐹‘𝑎) ↔ (𝐹‘𝐴) ⊆ (𝐹‘𝑏))) |
6 | 5 | imbi2d 344 |
. . . 4
⊢ (𝑎 = 𝑏 → (((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0) → (𝐹‘𝐴) ⊆ (𝐹‘𝑎)) ↔ ((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0) → (𝐹‘𝐴) ⊆ (𝐹‘𝑏)))) |
7 | | fveq2 6717 |
. . . . . 6
⊢ (𝑎 = (𝑏 + 1) → (𝐹‘𝑎) = (𝐹‘(𝑏 + 1))) |
8 | 7 | sseq2d 3933 |
. . . . 5
⊢ (𝑎 = (𝑏 + 1) → ((𝐹‘𝐴) ⊆ (𝐹‘𝑎) ↔ (𝐹‘𝐴) ⊆ (𝐹‘(𝑏 + 1)))) |
9 | 8 | imbi2d 344 |
. . . 4
⊢ (𝑎 = (𝑏 + 1) → (((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0) → (𝐹‘𝐴) ⊆ (𝐹‘𝑎)) ↔ ((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0) → (𝐹‘𝐴) ⊆ (𝐹‘(𝑏 + 1))))) |
10 | | fveq2 6717 |
. . . . . 6
⊢ (𝑎 = 𝐵 → (𝐹‘𝑎) = (𝐹‘𝐵)) |
11 | 10 | sseq2d 3933 |
. . . . 5
⊢ (𝑎 = 𝐵 → ((𝐹‘𝐴) ⊆ (𝐹‘𝑎) ↔ (𝐹‘𝐴) ⊆ (𝐹‘𝐵))) |
12 | 11 | imbi2d 344 |
. . . 4
⊢ (𝑎 = 𝐵 → (((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0) → (𝐹‘𝐴) ⊆ (𝐹‘𝑎)) ↔ ((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)))) |
13 | | ssid 3923 |
. . . . 5
⊢ (𝐹‘𝐴) ⊆ (𝐹‘𝐴) |
14 | 13 | 2a1i 12 |
. . . 4
⊢ (𝐴 ∈ ℤ →
((∀𝑥 ∈
ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0) → (𝐹‘𝐴) ⊆ (𝐹‘𝐴))) |
15 | | eluznn0 12513 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℕ0
∧ 𝑏 ∈
(ℤ≥‘𝐴)) → 𝑏 ∈ ℕ0) |
16 | 15 | ancoms 462 |
. . . . . . . . 9
⊢ ((𝑏 ∈
(ℤ≥‘𝐴) ∧ 𝐴 ∈ ℕ0) → 𝑏 ∈
ℕ0) |
17 | | fveq2 6717 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑏 → (𝐹‘𝑥) = (𝐹‘𝑏)) |
18 | | fvoveq1 7236 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑏 → (𝐹‘(𝑥 + 1)) = (𝐹‘(𝑏 + 1))) |
19 | 17, 18 | sseq12d 3934 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑏 → ((𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ↔ (𝐹‘𝑏) ⊆ (𝐹‘(𝑏 + 1)))) |
20 | 19 | rspcv 3532 |
. . . . . . . . 9
⊢ (𝑏 ∈ ℕ0
→ (∀𝑥 ∈
ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑏 + 1)))) |
21 | 16, 20 | syl 17 |
. . . . . . . 8
⊢ ((𝑏 ∈
(ℤ≥‘𝐴) ∧ 𝐴 ∈ ℕ0) →
(∀𝑥 ∈
ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑏 + 1)))) |
22 | 21 | expimpd 457 |
. . . . . . 7
⊢ (𝑏 ∈
(ℤ≥‘𝐴) → ((𝐴 ∈ ℕ0 ∧
∀𝑥 ∈
ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1))) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑏 + 1)))) |
23 | 22 | ancomsd 469 |
. . . . . 6
⊢ (𝑏 ∈
(ℤ≥‘𝐴) → ((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0) → (𝐹‘𝑏) ⊆ (𝐹‘(𝑏 + 1)))) |
24 | | sstr2 3908 |
. . . . . . 7
⊢ ((𝐹‘𝐴) ⊆ (𝐹‘𝑏) → ((𝐹‘𝑏) ⊆ (𝐹‘(𝑏 + 1)) → (𝐹‘𝐴) ⊆ (𝐹‘(𝑏 + 1)))) |
25 | 24 | com12 32 |
. . . . . 6
⊢ ((𝐹‘𝑏) ⊆ (𝐹‘(𝑏 + 1)) → ((𝐹‘𝐴) ⊆ (𝐹‘𝑏) → (𝐹‘𝐴) ⊆ (𝐹‘(𝑏 + 1)))) |
26 | 23, 25 | syl6 35 |
. . . . 5
⊢ (𝑏 ∈
(ℤ≥‘𝐴) → ((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0) → ((𝐹‘𝐴) ⊆ (𝐹‘𝑏) → (𝐹‘𝐴) ⊆ (𝐹‘(𝑏 + 1))))) |
27 | 26 | a2d 29 |
. . . 4
⊢ (𝑏 ∈
(ℤ≥‘𝐴) → (((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0) → (𝐹‘𝐴) ⊆ (𝐹‘𝑏)) → ((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0) → (𝐹‘𝐴) ⊆ (𝐹‘(𝑏 + 1))))) |
28 | 3, 6, 9, 12, 14, 27 | uzind4 12502 |
. . 3
⊢ (𝐵 ∈
(ℤ≥‘𝐴) → ((∀𝑥 ∈ ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵))) |
29 | 28 | com12 32 |
. 2
⊢
((∀𝑥 ∈
ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0) → (𝐵 ∈
(ℤ≥‘𝐴) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵))) |
30 | 29 | 3impia 1119 |
1
⊢
((∀𝑥 ∈
ℕ0 (𝐹‘𝑥) ⊆ (𝐹‘(𝑥 + 1)) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈
(ℤ≥‘𝐴)) → (𝐹‘𝐴) ⊆ (𝐹‘𝐵)) |