Step | Hyp | Ref
| Expression |
1 | | fveq2 6103 |
. . . . 5
⊢ (𝑚 = 𝑗 → (ℤ≥‘𝑚) =
(ℤ≥‘𝑗)) |
2 | 1 | sseq2d 3596 |
. . . 4
⊢ (𝑚 = 𝑗 → (𝐴 ⊆ (ℤ≥‘𝑚) ↔ 𝐴 ⊆ (ℤ≥‘𝑗))) |
3 | | seqeq1 12666 |
. . . . 5
⊢ (𝑚 = 𝑗 → seq𝑚( + , 𝐹) = seq𝑗( + , 𝐹)) |
4 | 3 | breq1d 4593 |
. . . 4
⊢ (𝑚 = 𝑗 → (seq𝑚( + , 𝐹) ⇝ 𝑥 ↔ seq𝑗( + , 𝐹) ⇝ 𝑥)) |
5 | 2, 4 | anbi12d 743 |
. . 3
⊢ (𝑚 = 𝑗 → ((𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ↔ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥))) |
6 | 5 | cbvrexv 3148 |
. 2
⊢
(∃𝑚 ∈
ℤ (𝐴 ⊆
(ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥) ↔ ∃𝑗 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) |
7 | | simplrr 797 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ (𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴)) → seq𝑗( + , 𝐹) ⇝ 𝑥) |
8 | | simplrl 796 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ (𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴)) → 𝐴 ⊆ (ℤ≥‘𝑗)) |
9 | | uzssz 11583 |
. . . . . . . . . . . . . 14
⊢
(ℤ≥‘𝑗) ⊆ ℤ |
10 | | zssre 11261 |
. . . . . . . . . . . . . 14
⊢ ℤ
⊆ ℝ |
11 | 9, 10 | sstri 3577 |
. . . . . . . . . . . . 13
⊢
(ℤ≥‘𝑗) ⊆ ℝ |
12 | 8, 11 | syl6ss 3580 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ (𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴)) → 𝐴 ⊆ ℝ) |
13 | | ltso 9997 |
. . . . . . . . . . . 12
⊢ < Or
ℝ |
14 | | soss 4977 |
. . . . . . . . . . . 12
⊢ (𝐴 ⊆ ℝ → ( <
Or ℝ → < Or 𝐴)) |
15 | 12, 13, 14 | mpisyl 21 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ (𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴)) → < Or 𝐴) |
16 | | fzfi 12633 |
. . . . . . . . . . . 12
⊢
(1...𝑚) ∈
Fin |
17 | | ovex 6577 |
. . . . . . . . . . . . . . 15
⊢
(1...𝑚) ∈
V |
18 | 17 | f1oen 7862 |
. . . . . . . . . . . . . 14
⊢ (𝑓:(1...𝑚)–1-1-onto→𝐴 → (1...𝑚) ≈ 𝐴) |
19 | 18 | ad2antll 761 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ (𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴)) → (1...𝑚) ≈ 𝐴) |
20 | 19 | ensymd 7893 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ (𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴)) → 𝐴 ≈ (1...𝑚)) |
21 | | enfii 8062 |
. . . . . . . . . . . 12
⊢
(((1...𝑚) ∈ Fin
∧ 𝐴 ≈ (1...𝑚)) → 𝐴 ∈ Fin) |
22 | 16, 20, 21 | sylancr 694 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ (𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴)) → 𝐴 ∈ Fin) |
23 | | fz1iso 13103 |
. . . . . . . . . . 11
⊢ (( <
Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃𝑔 𝑔 Isom < , < ((1...(#‘𝐴)), 𝐴)) |
24 | 15, 22, 23 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ (𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴)) → ∃𝑔 𝑔 Isom < , < ((1...(#‘𝐴)), 𝐴)) |
25 | | summo.1 |
. . . . . . . . . . . . 13
⊢ 𝐹 = (𝑘 ∈ ℤ ↦ if(𝑘 ∈ 𝐴, 𝐵, 0)) |
26 | | simplll 794 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑔 Isom < , < ((1...(#‘𝐴)), 𝐴))) → 𝜑) |
27 | | summo.2 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
28 | 26, 27 | sylan 487 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆
(ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑔 Isom < , < ((1...(#‘𝐴)), 𝐴))) ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
29 | | summo.3 |
. . . . . . . . . . . . 13
⊢ 𝐺 = (𝑛 ∈ ℕ ↦ ⦋(𝑓‘𝑛) / 𝑘⦌𝐵) |
30 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ ↦
⦋(𝑔‘𝑛) / 𝑘⦌𝐵) = (𝑛 ∈ ℕ ↦ ⦋(𝑔‘𝑛) / 𝑘⦌𝐵) |
31 | | simprll 798 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑔 Isom < , < ((1...(#‘𝐴)), 𝐴))) → 𝑚 ∈ ℕ) |
32 | | simpllr 795 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑔 Isom < , < ((1...(#‘𝐴)), 𝐴))) → 𝑗 ∈ ℤ) |
33 | | simplrl 796 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑔 Isom < , < ((1...(#‘𝐴)), 𝐴))) → 𝐴 ⊆ (ℤ≥‘𝑗)) |
34 | | simprlr 799 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑔 Isom < , < ((1...(#‘𝐴)), 𝐴))) → 𝑓:(1...𝑚)–1-1-onto→𝐴) |
35 | | simprr 792 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑔 Isom < , < ((1...(#‘𝐴)), 𝐴))) → 𝑔 Isom < , < ((1...(#‘𝐴)), 𝐴)) |
36 | 25, 28, 29, 30, 31, 32, 33, 34, 35 | summolem2a 14293 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ ((𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) ∧ 𝑔 Isom < , < ((1...(#‘𝐴)), 𝐴))) → seq𝑗( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑚)) |
37 | 36 | expr 641 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ (𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴)) → (𝑔 Isom < , < ((1...(#‘𝐴)), 𝐴) → seq𝑗( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑚))) |
38 | 37 | exlimdv 1848 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ (𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴)) → (∃𝑔 𝑔 Isom < , < ((1...(#‘𝐴)), 𝐴) → seq𝑗( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑚))) |
39 | 24, 38 | mpd 15 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ (𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴)) → seq𝑗( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑚)) |
40 | | climuni 14131 |
. . . . . . . . 9
⊢
((seq𝑗( + , 𝐹) ⇝ 𝑥 ∧ seq𝑗( + , 𝐹) ⇝ (seq1( + , 𝐺)‘𝑚)) → 𝑥 = (seq1( + , 𝐺)‘𝑚)) |
41 | 7, 39, 40 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ (𝑚 ∈ ℕ ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴)) → 𝑥 = (seq1( + , 𝐺)‘𝑚)) |
42 | 41 | anassrs 678 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆
(ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → 𝑥 = (seq1( + , 𝐺)‘𝑚)) |
43 | | eqeq2 2621 |
. . . . . . 7
⊢ (𝑦 = (seq1( + , 𝐺)‘𝑚) → (𝑥 = 𝑦 ↔ 𝑥 = (seq1( + , 𝐺)‘𝑚))) |
44 | 42, 43 | syl5ibrcom 236 |
. . . . . 6
⊢
(((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆
(ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ 𝑚 ∈ ℕ) ∧ 𝑓:(1...𝑚)–1-1-onto→𝐴) → (𝑦 = (seq1( + , 𝐺)‘𝑚) → 𝑥 = 𝑦)) |
45 | 44 | expimpd 627 |
. . . . 5
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ 𝑚 ∈ ℕ) → ((𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦)) |
46 | 45 | exlimdv 1848 |
. . . 4
⊢ ((((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) ∧ 𝑚 ∈ ℕ) → (∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦)) |
47 | 46 | rexlimdva 3013 |
. . 3
⊢ (((𝜑 ∧ 𝑗 ∈ ℤ) ∧ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦)) |
48 | 47 | r19.29an 3059 |
. 2
⊢ ((𝜑 ∧ ∃𝑗 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑗) ∧ seq𝑗( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦)) |
49 | 6, 48 | sylan2b 491 |
1
⊢ ((𝜑 ∧ ∃𝑚 ∈ ℤ (𝐴 ⊆ (ℤ≥‘𝑚) ∧ seq𝑚( + , 𝐹) ⇝ 𝑥)) → (∃𝑚 ∈ ℕ ∃𝑓(𝑓:(1...𝑚)–1-1-onto→𝐴 ∧ 𝑦 = (seq1( + , 𝐺)‘𝑚)) → 𝑥 = 𝑦)) |