Step | Hyp | Ref
| Expression |
1 | | 2sbcrex 36366 |
. . . . 5
⊢
([(𝑎 ↾
(1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣]∃𝑤 ∈ ℕ0 𝜑 ↔ ∃𝑤 ∈ ℕ0 [(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣]𝜑) |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝑎 ∈ (ℕ0
↑𝑚 (1...𝑀)) → ([(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣]∃𝑤 ∈ ℕ0 𝜑 ↔ ∃𝑤 ∈ ℕ0 [(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣]𝜑)) |
3 | 2 | rabbiia 3161 |
. . 3
⊢ {𝑎 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ [(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣]∃𝑤 ∈ ℕ0 𝜑} = {𝑎 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ ∃𝑤 ∈ ℕ0 [(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣]𝜑} |
4 | | rexfrabdioph.1 |
. . . . . 6
⊢ 𝑀 = (𝑁 + 1) |
5 | | peano2nn0 11210 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) |
6 | 4, 5 | syl5eqel 2692 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ 𝑀 ∈
ℕ0) |
7 | 6 | adantr 480 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝐿)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑} ∈ (Dioph‘𝐿)) → 𝑀 ∈
ℕ0) |
8 | | sbcrot3 36373 |
. . . . . . . . 9
⊢
([(𝑡‘𝐿) / 𝑤][(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣]𝜑 ↔ [(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑) |
9 | 8 | sbcbii 3458 |
. . . . . . . 8
⊢
([(𝑡 ↾
(1...𝑀)) / 𝑎][(𝑡‘𝐿) / 𝑤][(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣]𝜑 ↔ [(𝑡 ↾ (1...𝑀)) / 𝑎][(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑) |
10 | | reseq1 5311 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑡 ↾ (1...𝑀)) → (𝑎 ↾ (1...𝑁)) = ((𝑡 ↾ (1...𝑀)) ↾ (1...𝑁))) |
11 | 10 | sbccomieg 36375 |
. . . . . . . . 9
⊢
([(𝑡 ↾
(1...𝑀)) / 𝑎][(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑 ↔ [((𝑡 ↾ (1...𝑀)) ↾ (1...𝑁)) / 𝑢][(𝑡 ↾ (1...𝑀)) / 𝑎][(𝑎‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑) |
12 | | fzssp1 12255 |
. . . . . . . . . . . 12
⊢
(1...𝑁) ⊆
(1...(𝑁 +
1)) |
13 | 4 | oveq2i 6560 |
. . . . . . . . . . . 12
⊢
(1...𝑀) =
(1...(𝑁 +
1)) |
14 | 12, 13 | sseqtr4i 3601 |
. . . . . . . . . . 11
⊢
(1...𝑁) ⊆
(1...𝑀) |
15 | | resabs1 5347 |
. . . . . . . . . . 11
⊢
((1...𝑁) ⊆
(1...𝑀) → ((𝑡 ↾ (1...𝑀)) ↾ (1...𝑁)) = (𝑡 ↾ (1...𝑁))) |
16 | | dfsbcq 3404 |
. . . . . . . . . . 11
⊢ (((𝑡 ↾ (1...𝑀)) ↾ (1...𝑁)) = (𝑡 ↾ (1...𝑁)) → ([((𝑡 ↾ (1...𝑀)) ↾ (1...𝑁)) / 𝑢][(𝑡 ↾ (1...𝑀)) / 𝑎][(𝑎‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑 ↔ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡 ↾ (1...𝑀)) / 𝑎][(𝑎‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑)) |
17 | 14, 15, 16 | mp2b 10 |
. . . . . . . . . 10
⊢
([((𝑡 ↾
(1...𝑀)) ↾ (1...𝑁)) / 𝑢][(𝑡 ↾ (1...𝑀)) / 𝑎][(𝑎‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑 ↔ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡 ↾ (1...𝑀)) / 𝑎][(𝑎‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑) |
18 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑡 ∈ V |
19 | 18 | resex 5363 |
. . . . . . . . . . . . 13
⊢ (𝑡 ↾ (1...𝑀)) ∈ V |
20 | | fveq1 6102 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (𝑡 ↾ (1...𝑀)) → (𝑎‘𝑀) = ((𝑡 ↾ (1...𝑀))‘𝑀)) |
21 | 20 | sbcco3g 3951 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ↾ (1...𝑀)) ∈ V → ([(𝑡 ↾ (1...𝑀)) / 𝑎][(𝑎‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑 ↔ [((𝑡 ↾ (1...𝑀))‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑)) |
22 | 19, 21 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
([(𝑡 ↾
(1...𝑀)) / 𝑎][(𝑎‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑 ↔ [((𝑡 ↾ (1...𝑀))‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑) |
23 | | nn0p1nn 11209 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ) |
24 | 4, 23 | syl5eqel 2692 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ 𝑀 ∈
ℕ) |
25 | | elfz1end 12242 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈ ℕ ↔ 𝑀 ∈ (1...𝑀)) |
26 | 24, 25 | sylib 207 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ 𝑀 ∈ (1...𝑀)) |
27 | | fvres 6117 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈ (1...𝑀) → ((𝑡 ↾ (1...𝑀))‘𝑀) = (𝑡‘𝑀)) |
28 | | dfsbcq 3404 |
. . . . . . . . . . . . 13
⊢ (((𝑡 ↾ (1...𝑀))‘𝑀) = (𝑡‘𝑀) → ([((𝑡 ↾ (1...𝑀))‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑 ↔ [(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑)) |
29 | 26, 27, 28 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈ ℕ0
→ ([((𝑡 ↾
(1...𝑀))‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑 ↔ [(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑)) |
30 | 22, 29 | syl5bb 271 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ ([(𝑡 ↾
(1...𝑀)) / 𝑎][(𝑎‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑 ↔ [(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑)) |
31 | 30 | sbcbidv 3457 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ0
→ ([(𝑡 ↾
(1...𝑁)) / 𝑢][(𝑡 ↾ (1...𝑀)) / 𝑎][(𝑎‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑 ↔ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑)) |
32 | 17, 31 | syl5bb 271 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ0
→ ([((𝑡 ↾
(1...𝑀)) ↾ (1...𝑁)) / 𝑢][(𝑡 ↾ (1...𝑀)) / 𝑎][(𝑎‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑 ↔ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑)) |
33 | 11, 32 | syl5bb 271 |
. . . . . . . 8
⊢ (𝑁 ∈ ℕ0
→ ([(𝑡 ↾
(1...𝑀)) / 𝑎][(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑 ↔ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑)) |
34 | 9, 33 | syl5rbb 272 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ ([(𝑡 ↾
(1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑 ↔ [(𝑡 ↾ (1...𝑀)) / 𝑎][(𝑡‘𝐿) / 𝑤][(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣]𝜑)) |
35 | 34 | rabbidv 3164 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝐿)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑} = {𝑡 ∈ (ℕ0
↑𝑚 (1...𝐿)) ∣ [(𝑡 ↾ (1...𝑀)) / 𝑎][(𝑡‘𝐿) / 𝑤][(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣]𝜑}) |
36 | 35 | eleq1d 2672 |
. . . . 5
⊢ (𝑁 ∈ ℕ0
→ ({𝑡 ∈
(ℕ0 ↑𝑚 (1...𝐿)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑} ∈ (Dioph‘𝐿) ↔ {𝑡 ∈ (ℕ0
↑𝑚 (1...𝐿)) ∣ [(𝑡 ↾ (1...𝑀)) / 𝑎][(𝑡‘𝐿) / 𝑤][(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣]𝜑} ∈ (Dioph‘𝐿))) |
37 | 36 | biimpa 500 |
. . . 4
⊢ ((𝑁 ∈ ℕ0
∧ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝐿)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑} ∈ (Dioph‘𝐿)) → {𝑡 ∈ (ℕ0
↑𝑚 (1...𝐿)) ∣ [(𝑡 ↾ (1...𝑀)) / 𝑎][(𝑡‘𝐿) / 𝑤][(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣]𝜑} ∈ (Dioph‘𝐿)) |
38 | | rexfrabdioph.2 |
. . . . 5
⊢ 𝐿 = (𝑀 + 1) |
39 | 38 | rexfrabdioph 36377 |
. . . 4
⊢ ((𝑀 ∈ ℕ0
∧ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝐿)) ∣ [(𝑡 ↾ (1...𝑀)) / 𝑎][(𝑡‘𝐿) / 𝑤][(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣]𝜑} ∈ (Dioph‘𝐿)) → {𝑎 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ ∃𝑤 ∈ ℕ0 [(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣]𝜑} ∈ (Dioph‘𝑀)) |
40 | 7, 37, 39 | syl2anc 691 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝐿)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑} ∈ (Dioph‘𝐿)) → {𝑎 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ ∃𝑤 ∈ ℕ0 [(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣]𝜑} ∈ (Dioph‘𝑀)) |
41 | 3, 40 | syl5eqel 2692 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝐿)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑} ∈ (Dioph‘𝐿)) → {𝑎 ∈ (ℕ0
↑𝑚 (1...𝑀)) ∣ [(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣]∃𝑤 ∈ ℕ0 𝜑} ∈ (Dioph‘𝑀)) |
42 | 4 | rexfrabdioph 36377 |
. 2
⊢ ((𝑁 ∈ ℕ0
∧ {𝑎 ∈
(ℕ0 ↑𝑚 (1...𝑀)) ∣ [(𝑎 ↾ (1...𝑁)) / 𝑢][(𝑎‘𝑀) / 𝑣]∃𝑤 ∈ ℕ0 𝜑} ∈ (Dioph‘𝑀)) → {𝑢 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 ∃𝑤 ∈ ℕ0
𝜑} ∈ (Dioph‘𝑁)) |
43 | 41, 42 | syldan 486 |
1
⊢ ((𝑁 ∈ ℕ0
∧ {𝑡 ∈
(ℕ0 ↑𝑚 (1...𝐿)) ∣ [(𝑡 ↾ (1...𝑁)) / 𝑢][(𝑡‘𝑀) / 𝑣][(𝑡‘𝐿) / 𝑤]𝜑} ∈ (Dioph‘𝐿)) → {𝑢 ∈ (ℕ0
↑𝑚 (1...𝑁)) ∣ ∃𝑣 ∈ ℕ0 ∃𝑤 ∈ ℕ0
𝜑} ∈ (Dioph‘𝑁)) |