Proof of Theorem cvmliftlem5
Step | Hyp | Ref
| Expression |
1 | | 0z 12187 |
. . . 4
⊢ 0 ∈
ℤ |
2 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → 𝑀 ∈ ℕ) |
3 | | nnuz 12477 |
. . . . . 6
⊢ ℕ =
(ℤ≥‘1) |
4 | | 1e0p1 12335 |
. . . . . . 7
⊢ 1 = (0 +
1) |
5 | 4 | fveq2i 6720 |
. . . . . 6
⊢
(ℤ≥‘1) = (ℤ≥‘(0 +
1)) |
6 | 3, 5 | eqtri 2765 |
. . . . 5
⊢ ℕ =
(ℤ≥‘(0 + 1)) |
7 | 2, 6 | eleqtrdi 2848 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → 𝑀 ∈ (ℤ≥‘(0 +
1))) |
8 | | seqm1 13593 |
. . . 4
⊢ ((0
∈ ℤ ∧ 𝑀
∈ (ℤ≥‘(0 + 1))) → (seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉}))‘𝑀) = ((seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉}))‘(𝑀 − 1))(𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))))((( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉})‘𝑀))) |
9 | 1, 7, 8 | sylancr 590 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉}))‘𝑀) = ((seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉}))‘(𝑀 − 1))(𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))))((( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉})‘𝑀))) |
10 | | cvmliftlem.q |
. . . 4
⊢ 𝑄 = seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉})) |
11 | 10 | fveq1i 6718 |
. . 3
⊢ (𝑄‘𝑀) = (seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉}))‘𝑀) |
12 | 10 | fveq1i 6718 |
. . . 4
⊢ (𝑄‘(𝑀 − 1)) = (seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉}))‘(𝑀 − 1)) |
13 | 12 | oveq1i 7223 |
. . 3
⊢ ((𝑄‘(𝑀 − 1))(𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))))((( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉})‘𝑀)) = ((seq0((𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))), (( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉}))‘(𝑀 − 1))(𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))))((( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉})‘𝑀)) |
14 | 9, 11, 13 | 3eqtr4g 2803 |
. 2
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑄‘𝑀) = ((𝑄‘(𝑀 − 1))(𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))))((( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉})‘𝑀))) |
15 | | 0nnn 11866 |
. . . . . 6
⊢ ¬ 0
∈ ℕ |
16 | | disjsn 4627 |
. . . . . 6
⊢ ((ℕ
∩ {0}) = ∅ ↔ ¬ 0 ∈ ℕ) |
17 | 15, 16 | mpbir 234 |
. . . . 5
⊢ (ℕ
∩ {0}) = ∅ |
18 | | fnresi 6506 |
. . . . . 6
⊢ ( I
↾ ℕ) Fn ℕ |
19 | | c0ex 10827 |
. . . . . . 7
⊢ 0 ∈
V |
20 | | snex 5324 |
. . . . . . 7
⊢ {〈0,
𝑃〉} ∈
V |
21 | 19, 20 | fnsn 6438 |
. . . . . 6
⊢ {〈0,
{〈0, 𝑃〉}〉}
Fn {0} |
22 | | fvun1 6802 |
. . . . . 6
⊢ ((( I
↾ ℕ) Fn ℕ ∧ {〈0, {〈0, 𝑃〉}〉} Fn {0} ∧ ((ℕ ∩
{0}) = ∅ ∧ 𝑀
∈ ℕ)) → ((( I ↾ ℕ) ∪ {〈0, {〈0, 𝑃〉}〉})‘𝑀) = (( I ↾
ℕ)‘𝑀)) |
23 | 18, 21, 22 | mp3an12 1453 |
. . . . 5
⊢
(((ℕ ∩ {0}) = ∅ ∧ 𝑀 ∈ ℕ) → ((( I ↾
ℕ) ∪ {〈0, {〈0, 𝑃〉}〉})‘𝑀) = (( I ↾ ℕ)‘𝑀)) |
24 | 17, 2, 23 | sylancr 590 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → ((( I ↾
ℕ) ∪ {〈0, {〈0, 𝑃〉}〉})‘𝑀) = (( I ↾ ℕ)‘𝑀)) |
25 | | fvresi 6988 |
. . . . 5
⊢ (𝑀 ∈ ℕ → (( I
↾ ℕ)‘𝑀) =
𝑀) |
26 | 25 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (( I ↾
ℕ)‘𝑀) = 𝑀) |
27 | 24, 26 | eqtrd 2777 |
. . 3
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → ((( I ↾
ℕ) ∪ {〈0, {〈0, 𝑃〉}〉})‘𝑀) = 𝑀) |
28 | 27 | oveq2d 7229 |
. 2
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → ((𝑄‘(𝑀 − 1))(𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))))((( I ↾ ℕ) ∪ {〈0,
{〈0, 𝑃〉}〉})‘𝑀)) = ((𝑄‘(𝑀 − 1))(𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))))𝑀)) |
29 | | fvexd 6732 |
. . 3
⊢ (𝜑 → (𝑄‘(𝑀 − 1)) ∈ V) |
30 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝑥 = (𝑄‘(𝑀 − 1)) ∧ 𝑚 = 𝑀) → 𝑚 = 𝑀) |
31 | 30 | oveq1d 7228 |
. . . . . . . 8
⊢ ((𝑥 = (𝑄‘(𝑀 − 1)) ∧ 𝑚 = 𝑀) → (𝑚 − 1) = (𝑀 − 1)) |
32 | 31 | oveq1d 7228 |
. . . . . . 7
⊢ ((𝑥 = (𝑄‘(𝑀 − 1)) ∧ 𝑚 = 𝑀) → ((𝑚 − 1) / 𝑁) = ((𝑀 − 1) / 𝑁)) |
33 | 30 | oveq1d 7228 |
. . . . . . 7
⊢ ((𝑥 = (𝑄‘(𝑀 − 1)) ∧ 𝑚 = 𝑀) → (𝑚 / 𝑁) = (𝑀 / 𝑁)) |
34 | 32, 33 | oveq12d 7231 |
. . . . . 6
⊢ ((𝑥 = (𝑄‘(𝑀 − 1)) ∧ 𝑚 = 𝑀) → (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁))) |
35 | | cvmliftlem5.3 |
. . . . . 6
⊢ 𝑊 = (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁)) |
36 | 34, 35 | eqtr4di 2796 |
. . . . 5
⊢ ((𝑥 = (𝑄‘(𝑀 − 1)) ∧ 𝑚 = 𝑀) → (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) = 𝑊) |
37 | 30 | fveq2d 6721 |
. . . . . . . . . 10
⊢ ((𝑥 = (𝑄‘(𝑀 − 1)) ∧ 𝑚 = 𝑀) → (𝑇‘𝑚) = (𝑇‘𝑀)) |
38 | 37 | fveq2d 6721 |
. . . . . . . . 9
⊢ ((𝑥 = (𝑄‘(𝑀 − 1)) ∧ 𝑚 = 𝑀) → (2nd ‘(𝑇‘𝑚)) = (2nd ‘(𝑇‘𝑀))) |
39 | | simpl 486 |
. . . . . . . . . . 11
⊢ ((𝑥 = (𝑄‘(𝑀 − 1)) ∧ 𝑚 = 𝑀) → 𝑥 = (𝑄‘(𝑀 − 1))) |
40 | 39, 32 | fveq12d 6724 |
. . . . . . . . . 10
⊢ ((𝑥 = (𝑄‘(𝑀 − 1)) ∧ 𝑚 = 𝑀) → (𝑥‘((𝑚 − 1) / 𝑁)) = ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁))) |
41 | 40 | eleq1d 2822 |
. . . . . . . . 9
⊢ ((𝑥 = (𝑄‘(𝑀 − 1)) ∧ 𝑚 = 𝑀) → ((𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏 ↔ ((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)) |
42 | 38, 41 | riotaeqbidv 7173 |
. . . . . . . 8
⊢ ((𝑥 = (𝑄‘(𝑀 − 1)) ∧ 𝑚 = 𝑀) → (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏) = (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏)) |
43 | 42 | reseq2d 5851 |
. . . . . . 7
⊢ ((𝑥 = (𝑄‘(𝑀 − 1)) ∧ 𝑚 = 𝑀) → (𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏)) = (𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))) |
44 | 43 | cnveqd 5744 |
. . . . . 6
⊢ ((𝑥 = (𝑄‘(𝑀 − 1)) ∧ 𝑚 = 𝑀) → ◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏)) = ◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))) |
45 | 44 | fveq1d 6719 |
. . . . 5
⊢ ((𝑥 = (𝑄‘(𝑀 − 1)) ∧ 𝑚 = 𝑀) → (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)) = (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))) |
46 | 36, 45 | mpteq12dv 5140 |
. . . 4
⊢ ((𝑥 = (𝑄‘(𝑀 − 1)) ∧ 𝑚 = 𝑀) → (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))) = (𝑧 ∈ 𝑊 ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))) |
47 | | eqid 2737 |
. . . 4
⊢ (𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))) = (𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))) |
48 | | ovex 7246 |
. . . . . 6
⊢ (((𝑀 − 1) / 𝑁)[,](𝑀 / 𝑁)) ∈ V |
49 | 35, 48 | eqeltri 2834 |
. . . . 5
⊢ 𝑊 ∈ V |
50 | 49 | mptex 7039 |
. . . 4
⊢ (𝑧 ∈ 𝑊 ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))) ∈ V |
51 | 46, 47, 50 | ovmpoa 7364 |
. . 3
⊢ (((𝑄‘(𝑀 − 1)) ∈ V ∧ 𝑀 ∈ ℕ) → ((𝑄‘(𝑀 − 1))(𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))))𝑀) = (𝑧 ∈ 𝑊 ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))) |
52 | 29, 51 | sylan 583 |
. 2
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → ((𝑄‘(𝑀 − 1))(𝑥 ∈ V, 𝑚 ∈ ℕ ↦ (𝑧 ∈ (((𝑚 − 1) / 𝑁)[,](𝑚 / 𝑁)) ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑚))(𝑥‘((𝑚 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧))))𝑀) = (𝑧 ∈ 𝑊 ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))) |
53 | 14, 28, 52 | 3eqtrd 2781 |
1
⊢ ((𝜑 ∧ 𝑀 ∈ ℕ) → (𝑄‘𝑀) = (𝑧 ∈ 𝑊 ↦ (◡(𝐹 ↾ (℩𝑏 ∈ (2nd ‘(𝑇‘𝑀))((𝑄‘(𝑀 − 1))‘((𝑀 − 1) / 𝑁)) ∈ 𝑏))‘(𝐺‘𝑧)))) |