Step | Hyp | Ref
| Expression |
1 | | sdc.12 |
. . 3
⊢
Ⅎ𝑘𝜑 |
2 | | sdc.13 |
. . . . . . . 8
⊢ (𝜑 → 𝐺:𝑍⟶𝐽) |
3 | 2 | ffvelrnda 6267 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) ∈ 𝐽) |
4 | | sdc.10 |
. . . . . . . . 9
⊢ 𝐽 = {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} |
5 | 4 | eleq2i 2680 |
. . . . . . . 8
⊢ ((𝐺‘𝑘) ∈ 𝐽 ↔ (𝐺‘𝑘) ∈ {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)}) |
6 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑔𝑍 |
7 | | nfv 1830 |
. . . . . . . . . . 11
⊢
Ⅎ𝑔(𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 |
8 | | nfsbc1v 3422 |
. . . . . . . . . . 11
⊢
Ⅎ𝑔[(𝐺‘𝑘) / 𝑔]𝜓 |
9 | 7, 8 | nfan 1816 |
. . . . . . . . . 10
⊢
Ⅎ𝑔((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) |
10 | 6, 9 | nfrex 2990 |
. . . . . . . . 9
⊢
Ⅎ𝑔∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) |
11 | | fvex 6113 |
. . . . . . . . 9
⊢ (𝐺‘𝑘) ∈ V |
12 | | feq1 5939 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝐺‘𝑘) → (𝑔:(𝑀...𝑛)⟶𝐴 ↔ (𝐺‘𝑘):(𝑀...𝑛)⟶𝐴)) |
13 | | sbceq1a 3413 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝐺‘𝑘) → (𝜓 ↔ [(𝐺‘𝑘) / 𝑔]𝜓)) |
14 | 12, 13 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑔 = (𝐺‘𝑘) → ((𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) ↔ ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓))) |
15 | 14 | rexbidv 3034 |
. . . . . . . . 9
⊢ (𝑔 = (𝐺‘𝑘) → (∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) ↔ ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓))) |
16 | 10, 11, 15 | elabf 3318 |
. . . . . . . 8
⊢ ((𝐺‘𝑘) ∈ {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} ↔ ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)) |
17 | 5, 16 | bitri 263 |
. . . . . . 7
⊢ ((𝐺‘𝑘) ∈ 𝐽 ↔ ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)) |
18 | 3, 17 | sylib 207 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓)) |
19 | | fdm 5964 |
. . . . . . . . . 10
⊢ ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 → dom (𝐺‘𝑘) = (𝑀...𝑛)) |
20 | 19 | adantr 480 |
. . . . . . . . 9
⊢ (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → dom (𝐺‘𝑘) = (𝑀...𝑛)) |
21 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑀 → (𝐺‘𝑥) = (𝐺‘𝑀)) |
22 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑀 → (𝑀...𝑥) = (𝑀...𝑀)) |
23 | 22 | mpteq1d 4666 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑀 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))) |
24 | 21, 23 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑀 → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)))) |
25 | 24 | imbi2d 329 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑀 → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))))) |
26 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑤 → (𝐺‘𝑥) = (𝐺‘𝑤)) |
27 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑤 → (𝑀...𝑥) = (𝑀...𝑤)) |
28 | 27 | mpteq1d 4666 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑤 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))) |
29 | 26, 28 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑤 → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) |
30 | 29 | imbi2d 329 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑤 → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))))) |
31 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑤 + 1) → (𝐺‘𝑥) = (𝐺‘(𝑤 + 1))) |
32 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = (𝑤 + 1) → (𝑀...𝑥) = (𝑀...(𝑤 + 1))) |
33 | 32 | mpteq1d 4666 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = (𝑤 + 1) → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))) |
34 | 31, 33 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = (𝑤 + 1) → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))) |
35 | 34 | imbi2d 329 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (𝑤 + 1) → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))) |
36 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑘 → (𝐺‘𝑥) = (𝐺‘𝑘)) |
37 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑘 → (𝑀...𝑥) = (𝑀...𝑘)) |
38 | 37 | mpteq1d 4666 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑘 → (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚))) |
39 | 36, 38 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑘 → ((𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))) |
40 | 39 | imbi2d 329 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑘 → ((𝜑 → (𝐺‘𝑥) = (𝑚 ∈ (𝑀...𝑥) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (𝜑 → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚))))) |
41 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 = 𝑘 → (𝐺‘𝑚) = (𝐺‘𝑘)) |
42 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑚 = 𝑘 → 𝑚 = 𝑘) |
43 | 41, 42 | fveq12d 6109 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 = 𝑘 → ((𝐺‘𝑚)‘𝑚) = ((𝐺‘𝑘)‘𝑘)) |
44 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) |
45 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐺‘𝑘)‘𝑘) ∈ V |
46 | 43, 44, 45 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ (𝑀...𝑀) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘) = ((𝐺‘𝑘)‘𝑘)) |
47 | 46 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘) = ((𝐺‘𝑘)‘𝑘)) |
48 | | elfz1eq 12223 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 ∈ (𝑀...𝑀) → 𝑘 = 𝑀) |
49 | 48 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → 𝑘 = 𝑀) |
50 | 49 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → (𝐺‘𝑘) = (𝐺‘𝑀)) |
51 | 50 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → ((𝐺‘𝑘)‘𝑘) = ((𝐺‘𝑀)‘𝑘)) |
52 | 47, 51 | eqtr2d 2645 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ (𝑀...𝑀)) → ((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘)) |
53 | 52 | ex 449 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑘 ∈ (𝑀...𝑀) → ((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘))) |
54 | 1, 53 | ralrimi 2940 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑘 ∈ (𝑀...𝑀)((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘)) |
55 | | sdc.14 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝐺‘𝑀):(𝑀...𝑀)⟶𝐴) |
56 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺‘𝑀):(𝑀...𝑀)⟶𝐴 → (𝐺‘𝑀) Fn (𝑀...𝑀)) |
57 | 55, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐺‘𝑀) Fn (𝑀...𝑀)) |
58 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺‘𝑚)‘𝑚) ∈ V |
59 | 58, 44 | fnmpti 5935 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑀) |
60 | | eqfnfv 6219 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐺‘𝑀) Fn (𝑀...𝑀) ∧ (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑀)) → ((𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘))) |
61 | 57, 59, 60 | sylancl 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ∀𝑘 ∈ (𝑀...𝑀)((𝐺‘𝑀)‘𝑘) = ((𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑘))) |
62 | 54, 61 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚))) |
63 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑀 ∈ ℤ → (𝜑 → (𝐺‘𝑀) = (𝑚 ∈ (𝑀...𝑀) ↦ ((𝐺‘𝑚)‘𝑚)))) |
64 | | sdc.1 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑍 =
(ℤ≥‘𝑀) |
65 | 64 | eleq2i 2680 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ 𝑍 ↔ 𝑤 ∈ (ℤ≥‘𝑀)) |
66 | 2 | ffvelrnda 6267 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘𝑤) ∈ 𝐽) |
67 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ 𝑍) |
68 | | 3simpa 1051 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) → (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))) |
69 | 68 | reximi 2994 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
(∃𝑘 ∈
𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) → ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))) |
70 | 69 | ss2abi 3637 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} |
71 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(ℤ≥‘𝑀) ∈ V |
72 | 64, 71 | eqeltri 2684 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 𝑍 ∈ V |
73 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
Ⅎ𝑘 𝑤 ∈ 𝑍 |
74 | 1, 73 | nfan 1816 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
Ⅎ𝑘(𝜑 ∧ 𝑤 ∈ 𝑍) |
75 | | sdc.6 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
76 | 75 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝐴 ∈ 𝑉) |
77 | | simpl 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) → ℎ:(𝑀...(𝑘 + 1))⟶𝐴) |
78 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑀...(𝑘 + 1)) ∈ V |
79 | | elmapg 7757 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑀...(𝑘 + 1)) ∈ V) → (ℎ ∈ (𝐴 ↑𝑚 (𝑀...(𝑘 + 1))) ↔ ℎ:(𝑀...(𝑘 + 1))⟶𝐴)) |
80 | 78, 79 | mpan2 703 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝐴 ∈ 𝑉 → (ℎ ∈ (𝐴 ↑𝑚 (𝑀...(𝑘 + 1))) ↔ ℎ:(𝑀...(𝑘 + 1))⟶𝐴)) |
81 | 77, 80 | syl5ibr 235 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐴 ∈ 𝑉 → ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) → ℎ ∈ (𝐴 ↑𝑚 (𝑀...(𝑘 + 1))))) |
82 | 81 | abssdv 3639 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐴 ∈ 𝑉 → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ⊆ (𝐴 ↑𝑚 (𝑀...(𝑘 + 1)))) |
83 | 76, 82 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ⊆ (𝐴 ↑𝑚 (𝑀...(𝑘 + 1)))) |
84 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐴 ↑𝑚
(𝑀...(𝑘 + 1))) ∈ V |
85 | | ssexg 4732 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (({ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ⊆ (𝐴 ↑𝑚 (𝑀...(𝑘 + 1))) ∧ (𝐴 ↑𝑚 (𝑀...(𝑘 + 1))) ∈ V) → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V) |
86 | 83, 84, 85 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V) |
87 | 86 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑘 ∈ 𝑍 → {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V)) |
88 | 74, 87 | ralrimi 2940 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ∀𝑘 ∈ 𝑍 {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V) |
89 | | abrexex2g 7036 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑍 ∈ V ∧ ∀𝑘 ∈ 𝑍 {ℎ ∣ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V) |
90 | 72, 88, 89 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V) |
91 | | ssexg 4732 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∧ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ∈ V) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) |
92 | 70, 90, 91 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) |
93 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥 = (𝐺‘𝑤) → (𝑥 = (ℎ ↾ (𝑀...𝑘)) ↔ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))) |
94 | 93 | 3anbi2d 1396 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 = (𝐺‘𝑤) → ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) |
95 | 94 | rexbidv 3034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑥 = (𝐺‘𝑤) → (∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) |
96 | 95 | abbidv 2728 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = (𝐺‘𝑤) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) |
97 | 96 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 = (𝐺‘𝑤) → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V ↔ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V)) |
98 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = (𝐺‘𝑤) → (𝑤𝐹𝑥) = (𝑤𝐹(𝐺‘𝑤))) |
99 | 98, 96 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 = (𝐺‘𝑤) → ((𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ↔ (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})) |
100 | 97, 99 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑥 = (𝐺‘𝑤) → (({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) ↔ ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}))) |
101 | 100 | imbi2d 329 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 = (𝐺‘𝑤) → ((𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})) ↔ (𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)})))) |
102 | | sdc.11 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ 𝐹 = (𝑤 ∈ 𝑍, 𝑥 ∈ 𝐽 ↦ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) |
103 | 102 | ovmpt4g 6681 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑤 ∈ 𝑍 ∧ 𝑥 ∈ 𝐽 ∧ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) |
104 | 103 | 3com12 1261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ 𝐽 ∧ 𝑤 ∈ 𝑍 ∧ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V) → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) |
105 | 104 | 3exp 1256 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ 𝐽 → (𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹𝑥) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}))) |
106 | 101, 105 | vtoclga 3245 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺‘𝑤) ∈ 𝐽 → (𝑤 ∈ 𝑍 → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ V → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}))) |
107 | 66, 67, 92, 106 | syl3c 64 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤𝐹(𝐺‘𝑤)) = {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) |
108 | 107, 70 | syl6eqss 3618 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑤𝐹(𝐺‘𝑤)) ⊆ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))}) |
109 | | sdc.15 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘(𝑤 + 1)) ∈ (𝑤𝐹(𝐺‘𝑤))) |
110 | 108, 109 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝐺‘(𝑤 + 1)) ∈ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))}) |
111 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐺‘(𝑤 + 1)) ∈ V |
112 | | feq1 5939 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ = (𝐺‘(𝑤 + 1)) → (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ↔ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴)) |
113 | | reseq1 5311 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ℎ = (𝐺‘(𝑤 + 1)) → (ℎ ↾ (𝑀...𝑘)) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) |
114 | 113 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ = (𝐺‘(𝑤 + 1)) → ((𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)) ↔ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))) |
115 | 112, 114 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ℎ = (𝐺‘(𝑤 + 1)) → ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) ↔ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))) |
116 | 115 | rexbidv 3034 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ = (𝐺‘(𝑤 + 1)) → (∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘))) ↔ ∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))))) |
117 | 111, 116 | elab 3319 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐺‘(𝑤 + 1)) ∈ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = (ℎ ↾ (𝑀...𝑘)))} ↔ ∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))) |
118 | 110, 117 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)))) |
119 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑘((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))) |
120 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) |
121 | | fzssp1 12255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1)) |
122 | | fssres 5983 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝑀...𝑘) ⊆ (𝑀...(𝑘 + 1))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴) |
123 | 120, 121,
122 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴) |
124 | | fdm 5964 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)):(𝑀...𝑘)⟶𝐴 → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑘)) |
125 | 123, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑘)) |
126 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) |
127 | 58, 126 | fnmpti 5935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑤) |
128 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))) |
129 | 128 | fneq1d 5895 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤) ↔ (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...𝑤))) |
130 | 127, 129 | mpbiri 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤)) |
131 | | fndm 5904 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) Fn (𝑀...𝑤) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑤)) |
132 | 130, 131 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → dom ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑀...𝑤)) |
133 | 125, 132 | eqtr3d 2646 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑀...𝑘) = (𝑀...𝑤)) |
134 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑘 ∈ 𝑍) |
135 | 134, 64 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑘 ∈ (ℤ≥‘𝑀)) |
136 | | fzopth 12249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑤))) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑀...𝑘) = (𝑀...𝑤) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑤))) |
138 | 133, 137 | mpbid 221 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑀 = 𝑀 ∧ 𝑘 = 𝑤)) |
139 | 138 | simprd 478 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑘 = 𝑤) |
140 | 139 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑘 + 1) = (𝑤 + 1)) |
141 | 140 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1))) |
142 | | elfzp1 12261 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1)))) |
143 | 135, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) ↔ (𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1)))) |
144 | 133 | reseq2d 5317 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑤))) |
145 | | fzssp1 12255 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1)) |
146 | | resmpt 5369 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑀...𝑤) ⊆ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))) |
147 | 145, 146 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑤)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) |
148 | 144, 147 | syl6req 2661 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘))) |
149 | 128, 148 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘))) |
150 | 149 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥)) |
151 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥 ∈ (𝑀...𝑘) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = ((𝐺‘(𝑤 + 1))‘𝑥)) |
152 | | fvres 6117 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥 ∈ (𝑀...𝑘) → (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)) |
153 | 151, 152 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑥 ∈ (𝑀...𝑘) → ((((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))‘𝑥) = (((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑘))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))) |
154 | 150, 153 | syl5ibcom 234 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...𝑘) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))) |
155 | 140 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) ↔ 𝑥 = (𝑤 + 1))) |
156 | 139, 135 | eqeltrrd 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → 𝑤 ∈ (ℤ≥‘𝑀)) |
157 | | peano2uz 11617 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑤 ∈
(ℤ≥‘𝑀) → (𝑤 + 1) ∈
(ℤ≥‘𝑀)) |
158 | | eluzfz2 12220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑤 + 1) ∈
(ℤ≥‘𝑀) → (𝑤 + 1) ∈ (𝑀...(𝑤 + 1))) |
159 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑚 = (𝑤 + 1) → (𝐺‘𝑚) = (𝐺‘(𝑤 + 1))) |
160 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑚 = (𝑤 + 1) → 𝑚 = (𝑤 + 1)) |
161 | 159, 160 | fveq12d 6109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑚 = (𝑤 + 1) → ((𝐺‘𝑚)‘𝑚) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1))) |
162 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) |
163 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) ∈ V |
164 | 161, 162,
163 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑤 + 1) ∈ (𝑀...(𝑤 + 1)) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1))) |
165 | 156, 157,
158, 164 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1)) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1))) |
166 | 165 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1))) |
167 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝐺‘(𝑤 + 1))‘(𝑤 + 1))) |
168 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑥 = (𝑤 + 1) → ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1))) |
169 | 167, 168 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑥 = (𝑤 + 1) → (((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥) ↔ ((𝐺‘(𝑤 + 1))‘(𝑤 + 1)) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘(𝑤 + 1)))) |
170 | 166, 169 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 = (𝑤 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))) |
171 | 155, 170 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 = (𝑘 + 1) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))) |
172 | 154, 171 | jaod 394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝑥 ∈ (𝑀...𝑘) ∨ 𝑥 = (𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))) |
173 | 143, 172 | sylbid 229 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝑥 ∈ (𝑀...(𝑘 + 1)) → ((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥))) |
174 | 173 | ralrimiv 2948 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)) |
175 | | ffn 5958 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1))) |
176 | 175 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1))) |
177 | 58, 162 | fnmpti 5935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1)) |
178 | | eqfnfv2 6220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝐺‘(𝑤 + 1)) Fn (𝑀...(𝑘 + 1)) ∧ (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) Fn (𝑀...(𝑤 + 1))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))) |
179 | 176, 177,
178 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → ((𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ((𝑀...(𝑘 + 1)) = (𝑀...(𝑤 + 1)) ∧ ∀𝑥 ∈ (𝑀...(𝑘 + 1))((𝐺‘(𝑤 + 1))‘𝑥) = ((𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))‘𝑥)))) |
180 | 141, 174,
179 | mpbir2and 959 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))) |
181 | 180 | expr 641 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))) |
182 | | eqeq1 2614 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) ↔ ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)))) |
183 | 182 | imbi1d 330 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → (((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))) ↔ (((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))) |
184 | 181, 183 | syl5ibrcom 236 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) ∧ (𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴) → ((𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘)) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))) |
185 | 184 | expimpd 627 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑍) ∧ 𝑘 ∈ 𝑍) → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))) |
186 | 185 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (𝑘 ∈ 𝑍 → (((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))))) |
187 | 74, 119, 186 | rexlimd 3008 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → (∃𝑘 ∈ 𝑍 ((𝐺‘(𝑤 + 1)):(𝑀...(𝑘 + 1))⟶𝐴 ∧ (𝐺‘𝑤) = ((𝐺‘(𝑤 + 1)) ↾ (𝑀...𝑘))) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))) |
188 | 118, 187 | mpd 15 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚)))) |
189 | 188 | expcom 450 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 ∈ 𝑍 → (𝜑 → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))) |
190 | 65, 189 | sylbir 224 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈
(ℤ≥‘𝑀) → (𝜑 → ((𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚)) → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))) |
191 | 190 | a2d 29 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈
(ℤ≥‘𝑀) → ((𝜑 → (𝐺‘𝑤) = (𝑚 ∈ (𝑀...𝑤) ↦ ((𝐺‘𝑚)‘𝑚))) → (𝜑 → (𝐺‘(𝑤 + 1)) = (𝑚 ∈ (𝑀...(𝑤 + 1)) ↦ ((𝐺‘𝑚)‘𝑚))))) |
192 | 25, 30, 35, 40, 63, 191 | uzind4 11622 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → (𝜑 → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))) |
193 | 192, 64 | eleq2s 2706 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ 𝑍 → (𝜑 → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)))) |
194 | 193 | impcom 445 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚))) |
195 | 194 | dmeqd 5248 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom (𝐺‘𝑘) = dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚))) |
196 | | dmmptg 5549 |
. . . . . . . . . . . . . 14
⊢
(∀𝑚 ∈
(𝑀...𝑘)((𝐺‘𝑚)‘𝑚) ∈ V → dom (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑀...𝑘)) |
197 | 58 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ (𝑀...𝑘) → ((𝐺‘𝑚)‘𝑚) ∈ V) |
198 | 196, 197 | mprg 2910 |
. . . . . . . . . . . . 13
⊢ dom
(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑀...𝑘) |
199 | 195, 198 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → dom (𝐺‘𝑘) = (𝑀...𝑘)) |
200 | 199 | eqeq1d 2612 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (dom (𝐺‘𝑘) = (𝑀...𝑛) ↔ (𝑀...𝑘) = (𝑀...𝑛))) |
201 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ 𝑍) |
202 | 201, 64 | syl6eleq 2698 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (ℤ≥‘𝑀)) |
203 | | fzopth 12249 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑛))) |
204 | 202, 203 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑀...𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑛))) |
205 | 200, 204 | bitrd 267 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (dom (𝐺‘𝑘) = (𝑀...𝑛) ↔ (𝑀 = 𝑀 ∧ 𝑘 = 𝑛))) |
206 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑀 = 𝑀 ∧ 𝑘 = 𝑛) → 𝑘 = 𝑛) |
207 | 205, 206 | syl6bi 242 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (dom (𝐺‘𝑘) = (𝑀...𝑛) → 𝑘 = 𝑛)) |
208 | 20, 207 | syl5 33 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → 𝑘 = 𝑛)) |
209 | | oveq2 6557 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (𝑀...𝑛) = (𝑀...𝑘)) |
210 | 209 | feq2d 5944 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ↔ (𝐺‘𝑘):(𝑀...𝑘)⟶𝐴)) |
211 | | sdc.4 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → (𝜓 ↔ 𝜃)) |
212 | 211 | sbcbidv 3457 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑘 → ([(𝐺‘𝑘) / 𝑔]𝜓 ↔ [(𝐺‘𝑘) / 𝑔]𝜃)) |
213 | 210, 212 | anbi12d 743 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) ↔ ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃))) |
214 | 213 | equcoms 1934 |
. . . . . . . . 9
⊢ (𝑘 = 𝑛 → (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) ↔ ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃))) |
215 | 214 | biimpcd 238 |
. . . . . . . 8
⊢ (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → (𝑘 = 𝑛 → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃))) |
216 | 208, 215 | sylcom 30 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃))) |
217 | 216 | rexlimdvw 3016 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (∃𝑛 ∈ 𝑍 ((𝐺‘𝑘):(𝑀...𝑛)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜓) → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃))) |
218 | 18, 217 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑘):(𝑀...𝑘)⟶𝐴 ∧ [(𝐺‘𝑘) / 𝑔]𝜃)) |
219 | 218 | simpld 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐺‘𝑘):(𝑀...𝑘)⟶𝐴) |
220 | | eluzfz2 12220 |
. . . . 5
⊢ (𝑘 ∈
(ℤ≥‘𝑀) → 𝑘 ∈ (𝑀...𝑘)) |
221 | 202, 220 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → 𝑘 ∈ (𝑀...𝑘)) |
222 | 219, 221 | ffvelrnd 6268 |
. . 3
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝐺‘𝑘)‘𝑘) ∈ 𝐴) |
223 | 43 | cbvmptv 4678 |
. . 3
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑘 ∈ 𝑍 ↦ ((𝐺‘𝑘)‘𝑘)) |
224 | 1, 222, 223 | fmptdf 6294 |
. 2
⊢ (𝜑 → (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴) |
225 | 218 | simprd 478 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → [(𝐺‘𝑘) / 𝑔]𝜃) |
226 | 194, 225 | sbceq1dd 3408 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃) |
227 | 226 | ex 449 |
. . . 4
⊢ (𝜑 → (𝑘 ∈ 𝑍 → [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃)) |
228 | 1, 227 | ralrimi 2940 |
. . 3
⊢ (𝜑 → ∀𝑘 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃) |
229 | | mpteq1 4665 |
. . . . . 6
⊢ ((𝑀...𝑛) = (𝑀...𝑘) → (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚))) |
230 | | dfsbcq 3404 |
. . . . . 6
⊢ ((𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) = (𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓)) |
231 | 209, 229,
230 | 3syl 18 |
. . . . 5
⊢ (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓)) |
232 | 211 | sbcbidv 3457 |
. . . . 5
⊢ (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃)) |
233 | 231, 232 | bitrd 267 |
. . . 4
⊢ (𝑛 = 𝑘 → ([(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃)) |
234 | 233 | cbvralv 3147 |
. . 3
⊢
(∀𝑛 ∈
𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓 ↔ ∀𝑘 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑘) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜃) |
235 | 228, 234 | sylibr 223 |
. 2
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓) |
236 | 72 | mptex 6390 |
. . 3
⊢ (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ∈ V |
237 | | feq1 5939 |
. . . 4
⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝑓:𝑍⟶𝐴 ↔ (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴)) |
238 | | vex 3176 |
. . . . . . . 8
⊢ 𝑓 ∈ V |
239 | 238 | resex 5363 |
. . . . . . 7
⊢ (𝑓 ↾ (𝑀...𝑛)) ∈ V |
240 | | sdc.2 |
. . . . . . 7
⊢ (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓 ↔ 𝜒)) |
241 | 239, 240 | sbcie 3437 |
. . . . . 6
⊢
([(𝑓 ↾
(𝑀...𝑛)) / 𝑔]𝜓 ↔ 𝜒) |
242 | | reseq1 5311 |
. . . . . . . 8
⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑛))) |
243 | | fzssuz 12253 |
. . . . . . . . . 10
⊢ (𝑀...𝑛) ⊆ (ℤ≥‘𝑀) |
244 | 243, 64 | sseqtr4i 3601 |
. . . . . . . . 9
⊢ (𝑀...𝑛) ⊆ 𝑍 |
245 | | resmpt 5369 |
. . . . . . . . 9
⊢ ((𝑀...𝑛) ⊆ 𝑍 → ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚))) |
246 | 244, 245 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) |
247 | 242, 246 | syl6eq 2660 |
. . . . . . 7
⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝑓 ↾ (𝑀...𝑛)) = (𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚))) |
248 | 247 | sbceq1d 3407 |
. . . . . 6
⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → ([(𝑓 ↾ (𝑀...𝑛)) / 𝑔]𝜓 ↔ [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓)) |
249 | 241, 248 | syl5bbr 273 |
. . . . 5
⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (𝜒 ↔ [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓)) |
250 | 249 | ralbidv 2969 |
. . . 4
⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → (∀𝑛 ∈ 𝑍 𝜒 ↔ ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓)) |
251 | 237, 250 | anbi12d 743 |
. . 3
⊢ (𝑓 = (𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)) → ((𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒) ↔ ((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓))) |
252 | 236, 251 | spcev 3273 |
. 2
⊢ (((𝑚 ∈ 𝑍 ↦ ((𝐺‘𝑚)‘𝑚)):𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 [(𝑚 ∈ (𝑀...𝑛) ↦ ((𝐺‘𝑚)‘𝑚)) / 𝑔]𝜓) → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒)) |
253 | 224, 235,
252 | syl2anc 691 |
1
⊢ (𝜑 → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒)) |