Step | Hyp | Ref
| Expression |
1 | | mvrfval.v |
. 2
⊢ 𝑉 = (𝐼 mVar 𝑅) |
2 | | mvrfval.i |
. . . 4
⊢ (𝜑 → 𝐼 ∈ 𝑊) |
3 | | elex 3185 |
. . . 4
⊢ (𝐼 ∈ 𝑊 → 𝐼 ∈ V) |
4 | 2, 3 | syl 17 |
. . 3
⊢ (𝜑 → 𝐼 ∈ V) |
5 | | mvrfval.r |
. . . 4
⊢ (𝜑 → 𝑅 ∈ 𝑌) |
6 | | elex 3185 |
. . . 4
⊢ (𝑅 ∈ 𝑌 → 𝑅 ∈ V) |
7 | 5, 6 | syl 17 |
. . 3
⊢ (𝜑 → 𝑅 ∈ V) |
8 | | mptexg 6389 |
. . . 4
⊢ (𝐼 ∈ 𝑊 → (𝑥 ∈ 𝐼 ↦ (𝑓 ∈ 𝐷 ↦ if(𝑓 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, 1, 0)), 1 , 0 ))) ∈
V) |
9 | 2, 8 | syl 17 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ (𝑓 ∈ 𝐷 ↦ if(𝑓 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, 1, 0)), 1 , 0 ))) ∈
V) |
10 | | simpl 472 |
. . . . 5
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → 𝑖 = 𝐼) |
11 | 10 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (ℕ0
↑𝑚 𝑖) = (ℕ0
↑𝑚 𝐼)) |
12 | | rabeq 3166 |
. . . . . . . 8
⊢
((ℕ0 ↑𝑚 𝑖) = (ℕ0
↑𝑚 𝐼) → {ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈
Fin}) |
13 | 11, 12 | syl 17 |
. . . . . . 7
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → {ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈
Fin}) |
14 | | mvrfval.d |
. . . . . . 7
⊢ 𝐷 = {ℎ ∈ (ℕ0
↑𝑚 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} |
15 | 13, 14 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → {ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} = 𝐷) |
16 | | mpteq1 4665 |
. . . . . . . . 9
⊢ (𝑖 = 𝐼 → (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)) = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, 1, 0))) |
17 | 16 | adantr 480 |
. . . . . . . 8
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)) = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, 1, 0))) |
18 | 17 | eqeq2d 2620 |
. . . . . . 7
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)) ↔ 𝑓 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, 1, 0)))) |
19 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → 𝑟 = 𝑅) |
20 | 19 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (1r‘𝑟) = (1r‘𝑅)) |
21 | | mvrfval.o |
. . . . . . . 8
⊢ 1 =
(1r‘𝑅) |
22 | 20, 21 | syl6eqr 2662 |
. . . . . . 7
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (1r‘𝑟) = 1 ) |
23 | 19 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (0g‘𝑟) = (0g‘𝑅)) |
24 | | mvrfval.z |
. . . . . . . 8
⊢ 0 =
(0g‘𝑅) |
25 | 23, 24 | syl6eqr 2662 |
. . . . . . 7
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (0g‘𝑟) = 0 ) |
26 | 18, 22, 25 | ifbieq12d 4063 |
. . . . . 6
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟)) = if(𝑓 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, 1, 0)), 1 , 0 )) |
27 | 15, 26 | mpteq12dv 4663 |
. . . . 5
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑓 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟))) = (𝑓 ∈ 𝐷 ↦ if(𝑓 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, 1, 0)), 1 , 0 ))) |
28 | 10, 27 | mpteq12dv 4663 |
. . . 4
⊢ ((𝑖 = 𝐼 ∧ 𝑟 = 𝑅) → (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟)))) = (𝑥 ∈ 𝐼 ↦ (𝑓 ∈ 𝐷 ↦ if(𝑓 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, 1, 0)), 1 , 0 )))) |
29 | | df-mvr 19178 |
. . . 4
⊢ mVar =
(𝑖 ∈ V, 𝑟 ∈ V ↦ (𝑥 ∈ 𝑖 ↦ (𝑓 ∈ {ℎ ∈ (ℕ0
↑𝑚 𝑖) ∣ (◡ℎ “ ℕ) ∈ Fin} ↦ if(𝑓 = (𝑦 ∈ 𝑖 ↦ if(𝑦 = 𝑥, 1, 0)), (1r‘𝑟), (0g‘𝑟))))) |
30 | 28, 29 | ovmpt2ga 6688 |
. . 3
⊢ ((𝐼 ∈ V ∧ 𝑅 ∈ V ∧ (𝑥 ∈ 𝐼 ↦ (𝑓 ∈ 𝐷 ↦ if(𝑓 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, 1, 0)), 1 , 0 ))) ∈ V) →
(𝐼 mVar 𝑅) = (𝑥 ∈ 𝐼 ↦ (𝑓 ∈ 𝐷 ↦ if(𝑓 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, 1, 0)), 1 , 0 )))) |
31 | 4, 7, 9, 30 | syl3anc 1318 |
. 2
⊢ (𝜑 → (𝐼 mVar 𝑅) = (𝑥 ∈ 𝐼 ↦ (𝑓 ∈ 𝐷 ↦ if(𝑓 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, 1, 0)), 1 , 0 )))) |
32 | 1, 31 | syl5eq 2656 |
1
⊢ (𝜑 → 𝑉 = (𝑥 ∈ 𝐼 ↦ (𝑓 ∈ 𝐷 ↦ if(𝑓 = (𝑦 ∈ 𝐼 ↦ if(𝑦 = 𝑥, 1, 0)), 1 , 0 )))) |