Step | Hyp | Ref
| Expression |
1 | | sdc.8 |
. 2
⊢ (𝜑 → ∃𝑔(𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) |
2 | | sdc.10 |
. . . . . 6
⊢ 𝐽 = {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} |
3 | | sdc.1 |
. . . . . . . 8
⊢ 𝑍 =
(ℤ≥‘𝑀) |
4 | | fvex 6113 |
. . . . . . . 8
⊢
(ℤ≥‘𝑀) ∈ V |
5 | 3, 4 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑍 ∈ V |
6 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) → 𝑔:(𝑀...𝑛)⟶𝐴) |
7 | | sdc.6 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
8 | | ovex 6577 |
. . . . . . . . . . . 12
⊢ (𝑀...𝑛) ∈ V |
9 | | elmapg 7757 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ 𝑉 ∧ (𝑀...𝑛) ∈ V) → (𝑔 ∈ (𝐴 ↑𝑚 (𝑀...𝑛)) ↔ 𝑔:(𝑀...𝑛)⟶𝐴)) |
10 | 7, 8, 9 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑔 ∈ (𝐴 ↑𝑚 (𝑀...𝑛)) ↔ 𝑔:(𝑀...𝑛)⟶𝐴)) |
11 | 6, 10 | syl5ibr 235 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) → 𝑔 ∈ (𝐴 ↑𝑚 (𝑀...𝑛)))) |
12 | 11 | abssdv 3639 |
. . . . . . . . 9
⊢ (𝜑 → {𝑔 ∣ (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} ⊆ (𝐴 ↑𝑚 (𝑀...𝑛))) |
13 | | ovex 6577 |
. . . . . . . . 9
⊢ (𝐴 ↑𝑚
(𝑀...𝑛)) ∈ V |
14 | | ssexg 4732 |
. . . . . . . . 9
⊢ (({𝑔 ∣ (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} ⊆ (𝐴 ↑𝑚 (𝑀...𝑛)) ∧ (𝐴 ↑𝑚 (𝑀...𝑛)) ∈ V) → {𝑔 ∣ (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} ∈ V) |
15 | 12, 13, 14 | sylancl 693 |
. . . . . . . 8
⊢ (𝜑 → {𝑔 ∣ (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} ∈ V) |
16 | 15 | ralrimivw 2950 |
. . . . . . 7
⊢ (𝜑 → ∀𝑛 ∈ 𝑍 {𝑔 ∣ (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} ∈ V) |
17 | | abrexex2g 7036 |
. . . . . . 7
⊢ ((𝑍 ∈ V ∧ ∀𝑛 ∈ 𝑍 {𝑔 ∣ (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} ∈ V) → {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} ∈ V) |
18 | 5, 16, 17 | sylancr 694 |
. . . . . 6
⊢ (𝜑 → {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} ∈ V) |
19 | 2, 18 | syl5eqel 2692 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ V) |
20 | 19 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → 𝐽 ∈ V) |
21 | | sdc.7 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℤ) |
22 | 21 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → 𝑀 ∈ ℤ) |
23 | | uzid 11578 |
. . . . . . . 8
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
(ℤ≥‘𝑀)) |
24 | 22, 23 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → 𝑀 ∈ (ℤ≥‘𝑀)) |
25 | 24, 3 | syl6eleqr 2699 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → 𝑀 ∈ 𝑍) |
26 | | simprl 790 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → 𝑔:{𝑀}⟶𝐴) |
27 | | fzsn 12254 |
. . . . . . . . 9
⊢ (𝑀 ∈ ℤ → (𝑀...𝑀) = {𝑀}) |
28 | 22, 27 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → (𝑀...𝑀) = {𝑀}) |
29 | 28 | feq2d 5944 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → (𝑔:(𝑀...𝑀)⟶𝐴 ↔ 𝑔:{𝑀}⟶𝐴)) |
30 | 26, 29 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → 𝑔:(𝑀...𝑀)⟶𝐴) |
31 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → 𝜏) |
32 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑛 = 𝑀 → (𝑀...𝑛) = (𝑀...𝑀)) |
33 | 32 | feq2d 5944 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → (𝑔:(𝑀...𝑛)⟶𝐴 ↔ 𝑔:(𝑀...𝑀)⟶𝐴)) |
34 | | sdc.3 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → (𝜓 ↔ 𝜏)) |
35 | 33, 34 | anbi12d 743 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → ((𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) ↔ (𝑔:(𝑀...𝑀)⟶𝐴 ∧ 𝜏))) |
36 | 35 | rspcev 3282 |
. . . . . 6
⊢ ((𝑀 ∈ 𝑍 ∧ (𝑔:(𝑀...𝑀)⟶𝐴 ∧ 𝜏)) → ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)) |
37 | 25, 30, 31, 36 | syl12anc 1316 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)) |
38 | 2 | abeq2i 2722 |
. . . . 5
⊢ (𝑔 ∈ 𝐽 ↔ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)) |
39 | 37, 38 | sylibr 223 |
. . . 4
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → 𝑔 ∈ 𝐽) |
40 | 3 | peano2uzs 11618 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ 𝑍 → (𝑘 + 1) ∈ 𝑍) |
41 | 40 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)) → (𝑘 + 1) ∈ 𝑍) |
42 | | simpr1 1060 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)) → ℎ:(𝑀...(𝑘 + 1))⟶𝐴) |
43 | | simpr3 1062 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)) → 𝜎) |
44 | | vex 3176 |
. . . . . . . . . . . . . . . . . . 19
⊢ ℎ ∈ V |
45 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 + 1) ∈ V |
46 | | sdc.5 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑔 = ℎ ∧ 𝑛 = (𝑘 + 1)) → (𝜓 ↔ 𝜎)) |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑔 = ℎ ∧ 𝑛 = (𝑘 + 1)) → (𝜓 ↔ 𝜎))) |
48 | 44, 45, 47 | sbc2iedv 3473 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ([ℎ / 𝑔][(𝑘 + 1) / 𝑛]𝜓 ↔ 𝜎)) |
49 | 48 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)) → ([ℎ / 𝑔][(𝑘 + 1) / 𝑛]𝜓 ↔ 𝜎)) |
50 | 43, 49 | mpbird 246 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)) → [ℎ / 𝑔][(𝑘 + 1) / 𝑛]𝜓) |
51 | | nfv 1830 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑛 ℎ:(𝑀...(𝑘 + 1))⟶𝐴 |
52 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑛ℎ |
53 | | nfsbc1v 3422 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑛[(𝑘 + 1) / 𝑛]𝜓 |
54 | 52, 53 | nfsbc 3424 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑛[ℎ / 𝑔][(𝑘 + 1) / 𝑛]𝜓 |
55 | 51, 54 | nfan 1816 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑛(ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ [ℎ / 𝑔][(𝑘 + 1) / 𝑛]𝜓) |
56 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = (𝑘 + 1) → (𝑀...𝑛) = (𝑀...(𝑘 + 1))) |
57 | 56 | feq2d 5944 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = (𝑘 + 1) → (ℎ:(𝑀...𝑛)⟶𝐴 ↔ ℎ:(𝑀...(𝑘 + 1))⟶𝐴)) |
58 | | sbceq1a 3413 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = (𝑘 + 1) → (𝜓 ↔ [(𝑘 + 1) / 𝑛]𝜓)) |
59 | 58 | sbcbidv 3457 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = (𝑘 + 1) → ([ℎ / 𝑔]𝜓 ↔ [ℎ / 𝑔][(𝑘 + 1) / 𝑛]𝜓)) |
60 | 57, 59 | anbi12d 743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = (𝑘 + 1) → ((ℎ:(𝑀...𝑛)⟶𝐴 ∧ [ℎ / 𝑔]𝜓) ↔ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ [ℎ / 𝑔][(𝑘 + 1) / 𝑛]𝜓))) |
61 | 55, 60 | rspce 3277 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑘 + 1) ∈ 𝑍 ∧ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ [ℎ / 𝑔][(𝑘 + 1) / 𝑛]𝜓)) → ∃𝑛 ∈ 𝑍 (ℎ:(𝑀...𝑛)⟶𝐴 ∧ [ℎ / 𝑔]𝜓)) |
62 | 41, 42, 50, 61 | syl12anc 1316 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)) → ∃𝑛 ∈ 𝑍 (ℎ:(𝑀...𝑛)⟶𝐴 ∧ [ℎ / 𝑔]𝜓)) |
63 | 2 | eleq2i 2680 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ ∈ 𝐽 ↔ ℎ ∈ {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)}) |
64 | | nfcv 2751 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑔𝑍 |
65 | | nfv 1830 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑔 ℎ:(𝑀...𝑛)⟶𝐴 |
66 | | nfsbc1v 3422 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑔[ℎ / 𝑔]𝜓 |
67 | 65, 66 | nfan 1816 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑔(ℎ:(𝑀...𝑛)⟶𝐴 ∧ [ℎ / 𝑔]𝜓) |
68 | 64, 67 | nfrex 2990 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑔∃𝑛 ∈ 𝑍 (ℎ:(𝑀...𝑛)⟶𝐴 ∧ [ℎ / 𝑔]𝜓) |
69 | | feq1 5939 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = ℎ → (𝑔:(𝑀...𝑛)⟶𝐴 ↔ ℎ:(𝑀...𝑛)⟶𝐴)) |
70 | | sbceq1a 3413 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑔 = ℎ → (𝜓 ↔ [ℎ / 𝑔]𝜓)) |
71 | 69, 70 | anbi12d 743 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑔 = ℎ → ((𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) ↔ (ℎ:(𝑀...𝑛)⟶𝐴 ∧ [ℎ / 𝑔]𝜓))) |
72 | 71 | rexbidv 3034 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑔 = ℎ → (∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) ↔ ∃𝑛 ∈ 𝑍 (ℎ:(𝑀...𝑛)⟶𝐴 ∧ [ℎ / 𝑔]𝜓))) |
73 | 68, 44, 72 | elabf 3318 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ ∈ {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} ↔ ∃𝑛 ∈ 𝑍 (ℎ:(𝑀...𝑛)⟶𝐴 ∧ [ℎ / 𝑔]𝜓)) |
74 | 63, 73 | bitri 263 |
. . . . . . . . . . . . . . 15
⊢ (ℎ ∈ 𝐽 ↔ ∃𝑛 ∈ 𝑍 (ℎ:(𝑀...𝑛)⟶𝐴 ∧ [ℎ / 𝑔]𝜓)) |
75 | 62, 74 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ 𝑍) ∧ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)) → ℎ ∈ 𝐽) |
76 | 75 | ex 449 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) → ℎ ∈ 𝐽)) |
77 | 76 | rexlimdva 3013 |
. . . . . . . . . . . 12
⊢ (𝜑 → (∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) → ℎ ∈ 𝐽)) |
78 | 77 | abssdv 3639 |
. . . . . . . . . . 11
⊢ (𝜑 → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ 𝐽) |
79 | 78 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ 𝑥 ∈ 𝐽) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ 𝐽) |
80 | 19 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ 𝑥 ∈ 𝐽) → 𝐽 ∈ V) |
81 | | elpw2g 4754 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ V → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ 𝒫 𝐽 ↔ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ 𝐽)) |
82 | 80, 81 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ 𝑥 ∈ 𝐽) → ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ 𝒫 𝐽 ↔ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ⊆ 𝐽)) |
83 | 79, 82 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ 𝑥 ∈ 𝐽) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ 𝒫 𝐽) |
84 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑘 → (𝑀...𝑛) = (𝑀...𝑘)) |
85 | 84 | feq2d 5944 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → (𝑔:(𝑀...𝑛)⟶𝐴 ↔ 𝑔:(𝑀...𝑘)⟶𝐴)) |
86 | | sdc.4 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑘 → (𝜓 ↔ 𝜃)) |
87 | 85, 86 | anbi12d 743 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑘 → ((𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) ↔ (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃))) |
88 | 87 | cbvrexv 3148 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑛 ∈
𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) ↔ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)) |
89 | | sdc.9 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → ((𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃) → ∃ℎ(ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) |
90 | 89 | reximdva 3000 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃) → ∃𝑘 ∈ 𝑍 ∃ℎ(ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) |
91 | | rexcom4 3198 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑘 ∈
𝑍 ∃ℎ(ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ ∃ℎ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)) |
92 | 90, 91 | syl6ib 240 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃) → ∃ℎ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) |
93 | 88, 92 | syl5bi 231 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓) → ∃ℎ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) |
94 | 93 | ss2abdv 3638 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} ⊆ {𝑔 ∣ ∃ℎ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) |
95 | 2, 94 | syl5eqss 3612 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ⊆ {𝑔 ∣ ∃ℎ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) |
96 | 95 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → 𝑥 ∈ {𝑔 ∣ ∃ℎ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) |
97 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑥 ∈ V |
98 | | eqeq1 2614 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝑥 → (𝑔 = (ℎ ↾ (𝑀...𝑘)) ↔ 𝑥 = (ℎ ↾ (𝑀...𝑘)))) |
99 | 98 | 3anbi2d 1396 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = 𝑥 → ((ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) |
100 | 99 | rexbidv 3034 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = 𝑥 → (∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) |
101 | 100 | exbidv 1837 |
. . . . . . . . . . . . 13
⊢ (𝑔 = 𝑥 → (∃ℎ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) ↔ ∃ℎ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) |
102 | 97, 101 | elab 3319 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ {𝑔 ∣ ∃ℎ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ↔ ∃ℎ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)) |
103 | 96, 102 | sylib 207 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → ∃ℎ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)) |
104 | | abn0 3908 |
. . . . . . . . . . 11
⊢ ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ≠ ∅ ↔ ∃ℎ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)) |
105 | 103, 104 | sylibr 223 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ≠ ∅) |
106 | 105 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ 𝑥 ∈ 𝐽) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ≠ ∅) |
107 | | eldifsn 4260 |
. . . . . . . . 9
⊢ ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ (𝒫 𝐽 ∖ {∅}) ↔ ({ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ 𝒫 𝐽 ∧ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ≠ ∅)) |
108 | 83, 106, 107 | sylanbrc 695 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ 𝑥 ∈ 𝐽) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ (𝒫 𝐽 ∖ {∅})) |
109 | 108 | adantrl 748 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ (𝑤 ∈ 𝑍 ∧ 𝑥 ∈ 𝐽)) → {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ (𝒫 𝐽 ∖ {∅})) |
110 | 109 | ralrimivva 2954 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → ∀𝑤 ∈ 𝑍 ∀𝑥 ∈ 𝐽 {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ (𝒫 𝐽 ∖ {∅})) |
111 | | sdc.11 |
. . . . . . 7
⊢ 𝐹 = (𝑤 ∈ 𝑍, 𝑥 ∈ 𝐽 ↦ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) |
112 | 111 | fmpt2 7126 |
. . . . . 6
⊢
(∀𝑤 ∈
𝑍 ∀𝑥 ∈ 𝐽 {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} ∈ (𝒫 𝐽 ∖ {∅}) ↔ 𝐹:(𝑍 × 𝐽)⟶(𝒫 𝐽 ∖ {∅})) |
113 | 110, 112 | sylib 207 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → 𝐹:(𝑍 × 𝐽)⟶(𝒫 𝐽 ∖ {∅})) |
114 | 21 | iftrued 4044 |
. . . . . . . . . 10
⊢ (𝜑 → if(𝑀 ∈ ℤ, 𝑀, 0) = 𝑀) |
115 | 114 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝜑 →
(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0)) = (ℤ≥‘𝑀)) |
116 | 115, 3 | syl6eqr 2662 |
. . . . . . . 8
⊢ (𝜑 →
(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0)) = 𝑍) |
117 | 116 | xpeq1d 5062 |
. . . . . . 7
⊢ (𝜑 →
((ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0)) × 𝐽) = (𝑍 × 𝐽)) |
118 | 117 | feq2d 5944 |
. . . . . 6
⊢ (𝜑 → (𝐹:((ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0)) × 𝐽)⟶(𝒫 𝐽 ∖ {∅}) ↔ 𝐹:(𝑍 × 𝐽)⟶(𝒫 𝐽 ∖ {∅}))) |
119 | 118 | biimpar 501 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:(𝑍 × 𝐽)⟶(𝒫 𝐽 ∖ {∅})) → 𝐹:((ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0)) × 𝐽)⟶(𝒫 𝐽 ∖ {∅})) |
120 | 113, 119 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → 𝐹:((ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0)) × 𝐽)⟶(𝒫 𝐽 ∖ {∅})) |
121 | | 0z 11265 |
. . . . . 6
⊢ 0 ∈
ℤ |
122 | 121 | elimel 4100 |
. . . . 5
⊢ if(𝑀 ∈ ℤ, 𝑀, 0) ∈
ℤ |
123 | | eqid 2610 |
. . . . 5
⊢
(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0)) =
(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0)) |
124 | 122, 123 | axdc4uz 12645 |
. . . 4
⊢ ((𝐽 ∈ V ∧ 𝑔 ∈ 𝐽 ∧ 𝐹:((ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0)) × 𝐽)⟶(𝒫 𝐽 ∖ {∅})) → ∃𝑗(𝑗:(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0))⟶𝐽 ∧ (𝑗‘if(𝑀 ∈ ℤ, 𝑀, 0)) = 𝑔 ∧ ∀𝑚 ∈
(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0))(𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) |
125 | 20, 39, 120, 124 | syl3anc 1318 |
. . 3
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → ∃𝑗(𝑗:(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0))⟶𝐽 ∧ (𝑗‘if(𝑀 ∈ ℤ, 𝑀, 0)) = 𝑔 ∧ ∀𝑚 ∈
(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0))(𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) |
126 | 22 | iftrued 4044 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → if(𝑀 ∈ ℤ, 𝑀, 0) = 𝑀) |
127 | 126 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) →
(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0)) = (ℤ≥‘𝑀)) |
128 | 127, 3 | syl6eqr 2662 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) →
(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0)) = 𝑍) |
129 | 128 | feq2d 5944 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → (𝑗:(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0))⟶𝐽 ↔ 𝑗:𝑍⟶𝐽)) |
130 | 88 | abbii 2726 |
. . . . . . . . 9
⊢ {𝑔 ∣ ∃𝑛 ∈ 𝑍 (𝑔:(𝑀...𝑛)⟶𝐴 ∧ 𝜓)} = {𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} |
131 | 2, 130 | eqtri 2632 |
. . . . . . . 8
⊢ 𝐽 = {𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} |
132 | | feq3 5941 |
. . . . . . . 8
⊢ (𝐽 = {𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} → (𝑗:𝑍⟶𝐽 ↔ 𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)})) |
133 | 131, 132 | ax-mp 5 |
. . . . . . 7
⊢ (𝑗:𝑍⟶𝐽 ↔ 𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)}) |
134 | 129, 133 | syl6bb 275 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → (𝑗:(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0))⟶𝐽 ↔ 𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)})) |
135 | 126 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → (𝑗‘if(𝑀 ∈ ℤ, 𝑀, 0)) = (𝑗‘𝑀)) |
136 | 135 | eqeq1d 2612 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → ((𝑗‘if(𝑀 ∈ ℤ, 𝑀, 0)) = 𝑔 ↔ (𝑗‘𝑀) = 𝑔)) |
137 | 128 | raleqdv 3121 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → (∀𝑚 ∈
(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0))(𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)) ↔ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) |
138 | 134, 136,
137 | 3anbi123d 1391 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → ((𝑗:(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0))⟶𝐽 ∧ (𝑗‘if(𝑀 ∈ ℤ, 𝑀, 0)) = 𝑔 ∧ ∀𝑚 ∈
(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0))(𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚))) ↔ (𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚))))) |
139 | | sdc.2 |
. . . . . . 7
⊢ (𝑔 = (𝑓 ↾ (𝑀...𝑛)) → (𝜓 ↔ 𝜒)) |
140 | 7 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ (𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) → 𝐴 ∈ 𝑉) |
141 | 21 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ (𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) → 𝑀 ∈ ℤ) |
142 | 1 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ (𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) → ∃𝑔(𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) |
143 | | simpll 786 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ (𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) → 𝜑) |
144 | 143, 89 | sylan 487 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ (𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) ∧ 𝑘 ∈ 𝑍) → ((𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃) → ∃ℎ(ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑔 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎))) |
145 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) |
146 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑘𝑗 |
147 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑘𝑍 |
148 | | nfre1 2988 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃) |
149 | 148 | nfab 2755 |
. . . . . . . . . 10
⊢
Ⅎ𝑘{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} |
150 | 146, 147,
149 | nff 5954 |
. . . . . . . . 9
⊢
Ⅎ𝑘 𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} |
151 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑘(𝑗‘𝑀) = 𝑔 |
152 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘𝑚 |
153 | 131, 149 | nfcxfr 2749 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘𝐽 |
154 | | nfre1 2988 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎) |
155 | 154 | nfab 2755 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑘{ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)} |
156 | 147, 153,
155 | nfmpt2 6622 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑘(𝑤 ∈ 𝑍, 𝑥 ∈ 𝐽 ↦ {ℎ ∣ ∃𝑘 ∈ 𝑍 (ℎ:(𝑀...(𝑘 + 1))⟶𝐴 ∧ 𝑥 = (ℎ ↾ (𝑀...𝑘)) ∧ 𝜎)}) |
157 | 111, 156 | nfcxfr 2749 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘𝐹 |
158 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑘(𝑗‘𝑚) |
159 | 152, 157,
158 | nfov 6575 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝑚𝐹(𝑗‘𝑚)) |
160 | 159 | nfel2 2767 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)) |
161 | 147, 160 | nfral 2929 |
. . . . . . . . 9
⊢
Ⅎ𝑘∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)) |
162 | 150, 151,
161 | nf3an 1819 |
. . . . . . . 8
⊢
Ⅎ𝑘(𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚))) |
163 | 145, 162 | nfan 1816 |
. . . . . . 7
⊢
Ⅎ𝑘((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ (𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) |
164 | | simpr1 1060 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ (𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) → 𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)}) |
165 | 164, 133 | sylibr 223 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ (𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) → 𝑗:𝑍⟶𝐽) |
166 | 26 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ (𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) → 𝑔:{𝑀}⟶𝐴) |
167 | | simpr2 1061 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ (𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) → (𝑗‘𝑀) = 𝑔) |
168 | 141, 27 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ (𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) → (𝑀...𝑀) = {𝑀}) |
169 | 167, 168 | feq12d 5946 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ (𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) → ((𝑗‘𝑀):(𝑀...𝑀)⟶𝐴 ↔ 𝑔:{𝑀}⟶𝐴)) |
170 | 166, 169 | mpbird 246 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ (𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) → (𝑗‘𝑀):(𝑀...𝑀)⟶𝐴) |
171 | | simpr3 1062 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ (𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) → ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚))) |
172 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑤 → (𝑚 + 1) = (𝑤 + 1)) |
173 | 172 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑤 → (𝑗‘(𝑚 + 1)) = (𝑗‘(𝑤 + 1))) |
174 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑤 → 𝑚 = 𝑤) |
175 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑚 = 𝑤 → (𝑗‘𝑚) = (𝑗‘𝑤)) |
176 | 174, 175 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑤 → (𝑚𝐹(𝑗‘𝑚)) = (𝑤𝐹(𝑗‘𝑤))) |
177 | 173, 176 | eleq12d 2682 |
. . . . . . . . 9
⊢ (𝑚 = 𝑤 → ((𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)) ↔ (𝑗‘(𝑤 + 1)) ∈ (𝑤𝐹(𝑗‘𝑤)))) |
178 | 177 | rspccva 3281 |
. . . . . . . 8
⊢
((∀𝑚 ∈
𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)) ∧ 𝑤 ∈ 𝑍) → (𝑗‘(𝑤 + 1)) ∈ (𝑤𝐹(𝑗‘𝑤))) |
179 | 171, 178 | sylan 487 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ (𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) ∧ 𝑤 ∈ 𝑍) → (𝑗‘(𝑤 + 1)) ∈ (𝑤𝐹(𝑗‘𝑤))) |
180 | 3, 139, 34, 86, 46, 140, 141, 142, 144, 2, 111, 163, 165, 170, 179 | sdclem2 32708 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) ∧ (𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚)))) → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒)) |
181 | 180 | ex 449 |
. . . . 5
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → ((𝑗:𝑍⟶{𝑔 ∣ ∃𝑘 ∈ 𝑍 (𝑔:(𝑀...𝑘)⟶𝐴 ∧ 𝜃)} ∧ (𝑗‘𝑀) = 𝑔 ∧ ∀𝑚 ∈ 𝑍 (𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚))) → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒))) |
182 | 138, 181 | sylbid 229 |
. . . 4
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → ((𝑗:(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0))⟶𝐽 ∧ (𝑗‘if(𝑀 ∈ ℤ, 𝑀, 0)) = 𝑔 ∧ ∀𝑚 ∈
(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0))(𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚))) → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒))) |
183 | 182 | exlimdv 1848 |
. . 3
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → (∃𝑗(𝑗:(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0))⟶𝐽 ∧ (𝑗‘if(𝑀 ∈ ℤ, 𝑀, 0)) = 𝑔 ∧ ∀𝑚 ∈
(ℤ≥‘if(𝑀 ∈ ℤ, 𝑀, 0))(𝑗‘(𝑚 + 1)) ∈ (𝑚𝐹(𝑗‘𝑚))) → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒))) |
184 | 125, 183 | mpd 15 |
. 2
⊢ ((𝜑 ∧ (𝑔:{𝑀}⟶𝐴 ∧ 𝜏)) → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒)) |
185 | 1, 184 | exlimddv 1850 |
1
⊢ (𝜑 → ∃𝑓(𝑓:𝑍⟶𝐴 ∧ ∀𝑛 ∈ 𝑍 𝜒)) |