Step | Hyp | Ref
| Expression |
1 | | df-rab 2921 |
. . . . . 6
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑏 ∈ ℕ0 [𝑏 / 𝑣][𝑎 / 𝑢]𝜓} = {𝑎 ∣ (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑏 ∈ ℕ0 [𝑏 / 𝑣][𝑎 / 𝑢]𝜓)} |
2 | | dfsbcq 3437 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝑐 → ([𝑏 / 𝑣][𝑎 / 𝑢]𝜓 ↔ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)) |
3 | 2 | cbvrexv 3172 |
. . . . . . . . . 10
⊢
(∃𝑏 ∈
ℕ0 [𝑏 / 𝑣][𝑎 / 𝑢]𝜓 ↔ ∃𝑐 ∈ ℕ0 [𝑐 / 𝑣][𝑎 / 𝑢]𝜓) |
4 | 3 | anbi2i 730 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑏 ∈ ℕ0 [𝑏 / 𝑣][𝑎 / 𝑢]𝜓) ↔ (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑐 ∈ ℕ0 [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)) |
5 | | r19.42v 3092 |
. . . . . . . . 9
⊢
(∃𝑐 ∈
ℕ0 (𝑎
∈ (ℕ0 ↑𝑚 (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓) ↔ (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑐 ∈ ℕ0 [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)) |
6 | 4, 5 | bitr4i 267 |
. . . . . . . 8
⊢ ((𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑏 ∈ ℕ0 [𝑏 / 𝑣][𝑎 / 𝑢]𝜓) ↔ ∃𝑐 ∈ ℕ0 (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)) |
7 | | simpll 790 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ 𝑐 ∈
ℕ0) ∧ 𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁))) → 𝑁 ∈
ℕ0) |
8 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ 𝑐 ∈
ℕ0) ∧ 𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁))) → 𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁))) |
9 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ 𝑐 ∈
ℕ0) ∧ 𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁))) → 𝑐 ∈ ℕ0) |
10 | | rexrabdioph.1 |
. . . . . . . . . . . . . . 15
⊢ 𝑀 = (𝑁 + 1) |
11 | 10 | mapfzcons 37279 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℕ0
∧ 𝑎 ∈
(ℕ0 ↑𝑚 (1...𝑁)) ∧ 𝑐 ∈ ℕ0) → (𝑎 ∪ {〈𝑀, 𝑐〉}) ∈ (ℕ0
↑𝑚 (1...𝑀))) |
12 | 7, 8, 9, 11 | syl3anc 1326 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑐 ∈
ℕ0) ∧ 𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁))) → (𝑎 ∪ {〈𝑀, 𝑐〉}) ∈ (ℕ0
↑𝑚 (1...𝑀))) |
13 | 12 | adantrr 753 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑐 ∈
ℕ0) ∧ (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)) → (𝑎 ∪ {〈𝑀, 𝑐〉}) ∈ (ℕ0
↑𝑚 (1...𝑀))) |
14 | 10 | mapfzcons2 37282 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ 𝑐 ∈ ℕ0) → ((𝑎 ∪ {〈𝑀, 𝑐〉})‘𝑀) = 𝑐) |
15 | 8, 9, 14 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ 𝑐 ∈
ℕ0) ∧ 𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁))) → ((𝑎 ∪ {〈𝑀, 𝑐〉})‘𝑀) = 𝑐) |
16 | 15 | eqcomd 2628 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ 𝑐 ∈
ℕ0) ∧ 𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁))) → 𝑐 = ((𝑎 ∪ {〈𝑀, 𝑐〉})‘𝑀)) |
17 | 10 | mapfzcons1 37280 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) → ((𝑎 ∪ {〈𝑀, 𝑐〉}) ↾ (1...𝑁)) = 𝑎) |
18 | 17 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑁 ∈ ℕ0
∧ 𝑐 ∈
ℕ0) ∧ 𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁))) → ((𝑎 ∪ {〈𝑀, 𝑐〉}) ↾ (1...𝑁)) = 𝑎) |
19 | 18 | eqcomd 2628 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑁 ∈ ℕ0
∧ 𝑐 ∈
ℕ0) ∧ 𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁))) → 𝑎 = ((𝑎 ∪ {〈𝑀, 𝑐〉}) ↾ (1...𝑁))) |
20 | 19 | sbceq1d 3440 |
. . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℕ0
∧ 𝑐 ∈
ℕ0) ∧ 𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁))) → ([𝑎 / 𝑢]𝜓 ↔ [((𝑎 ∪ {〈𝑀, 𝑐〉}) ↾ (1...𝑁)) / 𝑢]𝜓)) |
21 | 16, 20 | sbceqbid 3442 |
. . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℕ0
∧ 𝑐 ∈
ℕ0) ∧ 𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁))) → ([𝑐 / 𝑣][𝑎 / 𝑢]𝜓 ↔ [((𝑎 ∪ {〈𝑀, 𝑐〉})‘𝑀) / 𝑣][((𝑎 ∪ {〈𝑀, 𝑐〉}) ↾ (1...𝑁)) / 𝑢]𝜓)) |
22 | 21 | biimpd 219 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑐 ∈
ℕ0) ∧ 𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁))) → ([𝑐 / 𝑣][𝑎 / 𝑢]𝜓 → [((𝑎 ∪ {〈𝑀, 𝑐〉})‘𝑀) / 𝑣][((𝑎 ∪ {〈𝑀, 𝑐〉}) ↾ (1...𝑁)) / 𝑢]𝜓)) |
23 | 22 | impr 649 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑐 ∈
ℕ0) ∧ (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)) → [((𝑎 ∪ {〈𝑀, 𝑐〉})‘𝑀) / 𝑣][((𝑎 ∪ {〈𝑀, 𝑐〉}) ↾ (1...𝑁)) / 𝑢]𝜓) |
24 | 19 | adantrr 753 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑐 ∈
ℕ0) ∧ (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)) → 𝑎 = ((𝑎 ∪ {〈𝑀, 𝑐〉}) ↾ (1...𝑁))) |
25 | | fveq1 6190 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑎 ∪ {〈𝑀, 𝑐〉}) → (𝑏‘𝑀) = ((𝑎 ∪ {〈𝑀, 𝑐〉})‘𝑀)) |
26 | | reseq1 5390 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑎 ∪ {〈𝑀, 𝑐〉}) → (𝑏 ↾ (1...𝑁)) = ((𝑎 ∪ {〈𝑀, 𝑐〉}) ↾ (1...𝑁))) |
27 | 26 | sbceq1d 3440 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑎 ∪ {〈𝑀, 𝑐〉}) → ([(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ [((𝑎 ∪ {〈𝑀, 𝑐〉}) ↾ (1...𝑁)) / 𝑢]𝜓)) |
28 | 25, 27 | sbceqbid 3442 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑎 ∪ {〈𝑀, 𝑐〉}) → ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ [((𝑎 ∪ {〈𝑀, 𝑐〉})‘𝑀) / 𝑣][((𝑎 ∪ {〈𝑀, 𝑐〉}) ↾ (1...𝑁)) / 𝑢]𝜓)) |
29 | 26 | eqeq2d 2632 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑎 ∪ {〈𝑀, 𝑐〉}) → (𝑎 = (𝑏 ↾ (1...𝑁)) ↔ 𝑎 = ((𝑎 ∪ {〈𝑀, 𝑐〉}) ↾ (1...𝑁)))) |
30 | 28, 29 | anbi12d 747 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑎 ∪ {〈𝑀, 𝑐〉}) → (([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) ↔ ([((𝑎 ∪ {〈𝑀, 𝑐〉})‘𝑀) / 𝑣][((𝑎 ∪ {〈𝑀, 𝑐〉}) ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = ((𝑎 ∪ {〈𝑀, 𝑐〉}) ↾ (1...𝑁))))) |
31 | 30 | rspcev 3309 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∪ {〈𝑀, 𝑐〉}) ∈ (ℕ0
↑𝑚 (1...𝑀)) ∧ ([((𝑎 ∪ {〈𝑀, 𝑐〉})‘𝑀) / 𝑣][((𝑎 ∪ {〈𝑀, 𝑐〉}) ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = ((𝑎 ∪ {〈𝑀, 𝑐〉}) ↾ (1...𝑁)))) → ∃𝑏 ∈ (ℕ0
↑𝑚 (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) |
32 | 13, 23, 24, 31 | syl12anc 1324 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝑐 ∈
ℕ0) ∧ (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)) → ∃𝑏 ∈ (ℕ0
↑𝑚 (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) |
33 | 32 | ex 450 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑐 ∈
ℕ0) → ((𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓) → ∃𝑏 ∈ (ℕ0
↑𝑚 (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))))) |
34 | 33 | rexlimdva 3031 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (∃𝑐 ∈
ℕ0 (𝑎
∈ (ℕ0 ↑𝑚 (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓) → ∃𝑏 ∈ (ℕ0
↑𝑚 (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))))) |
35 | | elmapi 7879 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ (ℕ0
↑𝑚 (1...𝑀)) → 𝑏:(1...𝑀)⟶ℕ0) |
36 | | nn0p1nn 11332 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
37 | 10, 36 | syl5eqel 2705 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 𝑀 ∈
ℕ) |
38 | | elfz1end 12371 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈ ℕ ↔ 𝑀 ∈ (1...𝑀)) |
39 | 37, 38 | sylib 208 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ 𝑀 ∈ (1...𝑀)) |
40 | | ffvelrn 6357 |
. . . . . . . . . . . . . 14
⊢ ((𝑏:(1...𝑀)⟶ℕ0 ∧ 𝑀 ∈ (1...𝑀)) → (𝑏‘𝑀) ∈
ℕ0) |
41 | 35, 39, 40 | syl2anr 495 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℕ0
∧ 𝑏 ∈
(ℕ0 ↑𝑚 (1...𝑀))) → (𝑏‘𝑀) ∈
ℕ0) |
42 | 41 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑏 ∈
(ℕ0 ↑𝑚 (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → (𝑏‘𝑀) ∈
ℕ0) |
43 | | simprr 796 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑏 ∈
(ℕ0 ↑𝑚 (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → 𝑎 = (𝑏 ↾ (1...𝑁))) |
44 | 10 | mapfzcons1cl 37281 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ (ℕ0
↑𝑚 (1...𝑀)) → (𝑏 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁))) |
45 | 44 | ad2antlr 763 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑏 ∈
(ℕ0 ↑𝑚 (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → (𝑏 ↾ (1...𝑁)) ∈ (ℕ0
↑𝑚 (1...𝑁))) |
46 | 43, 45 | eqeltrd 2701 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑏 ∈
(ℕ0 ↑𝑚 (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → 𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁))) |
47 | | simprl 794 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑏 ∈
(ℕ0 ↑𝑚 (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → [(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓) |
48 | | dfsbcq 3437 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (𝑏 ↾ (1...𝑁)) → ([𝑎 / 𝑢]𝜓 ↔ [(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓)) |
49 | 48 | sbcbidv 3490 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝑏 ↾ (1...𝑁)) → ([(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓 ↔ [(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓)) |
50 | 49 | ad2antll 765 |
. . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℕ0
∧ 𝑏 ∈
(ℕ0 ↑𝑚 (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → ([(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓 ↔ [(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓)) |
51 | 47, 50 | mpbird 247 |
. . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℕ0
∧ 𝑏 ∈
(ℕ0 ↑𝑚 (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → [(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓) |
52 | | dfsbcq 3437 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = (𝑏‘𝑀) → ([𝑐 / 𝑣][𝑎 / 𝑢]𝜓 ↔ [(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓)) |
53 | 52 | anbi2d 740 |
. . . . . . . . . . . . 13
⊢ (𝑐 = (𝑏‘𝑀) → ((𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓) ↔ (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ [(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓))) |
54 | 53 | rspcev 3309 |
. . . . . . . . . . . 12
⊢ (((𝑏‘𝑀) ∈ ℕ0 ∧ (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ [(𝑏‘𝑀) / 𝑣][𝑎 / 𝑢]𝜓)) → ∃𝑐 ∈ ℕ0 (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)) |
55 | 42, 46, 51, 54 | syl12anc 1324 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℕ0
∧ 𝑏 ∈
(ℕ0 ↑𝑚 (1...𝑀))) ∧ ([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) → ∃𝑐 ∈ ℕ0 (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓)) |
56 | 55 | ex 450 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑏 ∈
(ℕ0 ↑𝑚 (1...𝑀))) → (([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) → ∃𝑐 ∈ ℕ0 (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓))) |
57 | 56 | rexlimdva 3031 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ (∃𝑏 ∈
(ℕ0 ↑𝑚 (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))) → ∃𝑐 ∈ ℕ0 (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓))) |
58 | 34, 57 | impbid 202 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ (∃𝑐 ∈
ℕ0 (𝑎
∈ (ℕ0 ↑𝑚 (1...𝑁)) ∧ [𝑐 / 𝑣][𝑎 / 𝑢]𝜓) ↔ ∃𝑏 ∈ (ℕ0
↑𝑚 (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))))) |
59 | 6, 58 | syl5bb 272 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ((𝑎 ∈
(ℕ0 ↑𝑚 (1...𝑁)) ∧ ∃𝑏 ∈ ℕ0 [𝑏 / 𝑣][𝑎 / 𝑢]𝜓) ↔ ∃𝑏 ∈ (ℕ0
↑𝑚 (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁))))) |
60 | 59 | abbidv 2741 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ {𝑎 ∣ (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∧ ∃𝑏 ∈ ℕ0 [𝑏 / 𝑣][𝑎 / 𝑢]𝜓)} = {𝑎 ∣ ∃𝑏 ∈ (ℕ0
↑𝑚 (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))}) |
61 | 1, 60 | syl5eq 2668 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ {𝑎 ∈
(ℕ0 ↑𝑚 (1...𝑁)) ∣ ∃𝑏 ∈ ℕ0 [𝑏 / 𝑣][𝑎 / 𝑢]𝜓} = {𝑎 ∣ ∃𝑏 ∈ (ℕ0
↑𝑚 (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))}) |
62 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑢(ℕ0
↑𝑚 (1...𝑁)) |
63 | | nfcv 2764 |
. . . . . 6
⊢
Ⅎ𝑎(ℕ0
↑𝑚 (1...𝑁)) |
64 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑎∃𝑣 ∈ ℕ0
𝜓 |
65 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑢ℕ0 |
66 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑢𝑏 |
67 | | nfsbc1v 3455 |
. . . . . . . 8
⊢
Ⅎ𝑢[𝑎 / 𝑢]𝜓 |
68 | 66, 67 | nfsbc 3457 |
. . . . . . 7
⊢
Ⅎ𝑢[𝑏 / 𝑣][𝑎 / 𝑢]𝜓 |
69 | 65, 68 | nfrex 3007 |
. . . . . 6
⊢
Ⅎ𝑢∃𝑏 ∈ ℕ0
[𝑏 / 𝑣][𝑎 / 𝑢]𝜓 |
70 | | sbceq1a 3446 |
. . . . . . . 8
⊢ (𝑢 = 𝑎 → (𝜓 ↔ [𝑎 / 𝑢]𝜓)) |
71 | 70 | rexbidv 3052 |
. . . . . . 7
⊢ (𝑢 = 𝑎 → (∃𝑣 ∈ ℕ0 𝜓 ↔ ∃𝑣 ∈ ℕ0 [𝑎 / 𝑢]𝜓)) |
72 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑏[𝑎 / 𝑢]𝜓 |
73 | | nfsbc1v 3455 |
. . . . . . . 8
⊢
Ⅎ𝑣[𝑏 / 𝑣][𝑎 / 𝑢]𝜓 |
74 | | sbceq1a 3446 |
. . . . . . . 8
⊢ (𝑣 = 𝑏 → ([𝑎 / 𝑢]𝜓 ↔ [𝑏 / 𝑣][𝑎 / 𝑢]𝜓)) |
75 | 72, 73, 74 | cbvrex 3168 |
. . . . . . 7
⊢
(∃𝑣 ∈
ℕ0 [𝑎 / 𝑢]𝜓 ↔ ∃𝑏 ∈ ℕ0 [𝑏 / 𝑣][𝑎 / 𝑢]𝜓) |
76 | 71, 75 | syl6bb 276 |
. . . . . 6
⊢ (𝑢 = 𝑎 → (∃𝑣 ∈ ℕ0 𝜓 ↔ ∃𝑏 ∈ ℕ0 [𝑏 / 𝑣][𝑎 / 𝑢]𝜓)) |
77 | 62, 63, 64, 69, 76 | cbvrab 3198 |
. . . . 5
⊢ {𝑢 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 𝜓} = {𝑎 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑏 ∈ ℕ0 [𝑏 / 𝑣][𝑎 / 𝑢]𝜓} |
78 | | fveq1 6190 |
. . . . . . . 8
⊢ (𝑡 = 𝑏 → (𝑡‘𝑀) = (𝑏‘𝑀)) |
79 | | reseq1 5390 |
. . . . . . . . 9
⊢ (𝑡 = 𝑏 → (𝑡 ↾ (1...𝑁)) = (𝑏 ↾ (1...𝑁))) |
80 | 79 | sbceq1d 3440 |
. . . . . . . 8
⊢ (𝑡 = 𝑏 → ([(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ [(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓)) |
81 | 78, 80 | sbceqbid 3442 |
. . . . . . 7
⊢ (𝑡 = 𝑏 → ([(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ [(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓)) |
82 | 81 | rexrab 3370 |
. . . . . 6
⊢
(∃𝑏 ∈
{𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁)) ↔ ∃𝑏 ∈ (ℕ0
↑𝑚 (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))) |
83 | 82 | abbii 2739 |
. . . . 5
⊢ {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁))} = {𝑎 ∣ ∃𝑏 ∈ (ℕ0
↑𝑚 (1...𝑀))([(𝑏‘𝑀) / 𝑣][(𝑏 ↾ (1...𝑁)) / 𝑢]𝜓 ∧ 𝑎 = (𝑏 ↾ (1...𝑁)))} |
84 | 61, 77, 83 | 3eqtr4g 2681 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ {𝑢 ∈
(ℕ0 ↑𝑚 (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 𝜓} = {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁))}) |
85 | | fvex 6201 |
. . . . . . . . 9
⊢ (𝑡‘𝑀) ∈ V |
86 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑡 ∈ V |
87 | 86 | resex 5443 |
. . . . . . . . 9
⊢ (𝑡 ↾ (1...𝑁)) ∈ V |
88 | | rexrabdioph.2 |
. . . . . . . . . 10
⊢ (𝑣 = (𝑡‘𝑀) → (𝜓 ↔ 𝜒)) |
89 | | rexrabdioph.3 |
. . . . . . . . . 10
⊢ (𝑢 = (𝑡 ↾ (1...𝑁)) → (𝜒 ↔ 𝜑)) |
90 | 88, 89 | sylan9bb 736 |
. . . . . . . . 9
⊢ ((𝑣 = (𝑡‘𝑀) ∧ 𝑢 = (𝑡 ↾ (1...𝑁))) → (𝜓 ↔ 𝜑)) |
91 | 85, 87, 90 | sbc2ie 3505 |
. . . . . . . 8
⊢
([(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ 𝜑) |
92 | 91 | a1i 11 |
. . . . . . 7
⊢ (𝑡 ∈ (ℕ0
↑𝑚 (1...𝑀)) → ([(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓 ↔ 𝜑)) |
93 | 92 | rabbiia 3185 |
. . . . . 6
⊢ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓} = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ 𝜑} |
94 | 93 | rexeqi 3143 |
. . . . 5
⊢
(∃𝑏 ∈
{𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁)) ↔ ∃𝑏 ∈ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁))) |
95 | 94 | abbii 2739 |
. . . 4
⊢ {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ [(𝑡‘𝑀) / 𝑣][(𝑡 ↾ (1...𝑁)) / 𝑢]𝜓}𝑎 = (𝑏 ↾ (1...𝑁))} = {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁))} |
96 | 84, 95 | syl6eq 2672 |
. . 3
⊢ (𝑁 ∈ ℕ0
→ {𝑢 ∈
(ℕ0 ↑𝑚 (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 𝜓} = {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁))}) |
97 | 96 | adantr 481 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → {𝑢 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 𝜓} = {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁))}) |
98 | | simpl 473 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → 𝑁 ∈
ℕ0) |
99 | | nn0z 11400 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℤ) |
100 | | uzid 11702 |
. . . . . 6
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
(ℤ≥‘𝑁)) |
101 | | peano2uz 11741 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘𝑁) → (𝑁 + 1) ∈
(ℤ≥‘𝑁)) |
102 | 99, 100, 101 | 3syl 18 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
(ℤ≥‘𝑁)) |
103 | 10, 102 | syl5eqel 2705 |
. . . 4
⊢ (𝑁 ∈ ℕ0
→ 𝑀 ∈
(ℤ≥‘𝑁)) |
104 | 103 | adantr 481 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → 𝑀 ∈ (ℤ≥‘𝑁)) |
105 | | simpr 477 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) |
106 | | diophrex 37339 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ 𝑀 ∈
(ℤ≥‘𝑁) ∧ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁))} ∈ (Dioph‘𝑁)) |
107 | 98, 104, 105, 106 | syl3anc 1326 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → {𝑎 ∣ ∃𝑏 ∈ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ 𝜑}𝑎 = (𝑏 ↾ (1...𝑁))} ∈ (Dioph‘𝑁)) |
108 | 97, 107 | eqeltrd 2701 |
1
⊢ ((𝑁 ∈ ℕ0
∧ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝑀)) ∣ 𝜑} ∈ (Dioph‘𝑀)) → {𝑢 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 𝜓} ∈ (Dioph‘𝑁)) |