Step | Hyp | Ref
| Expression |
1 | | evl1fval.o |
. . 3
⊢ 𝑂 = (eval1‘𝑅) |
2 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑟)
∈ V |
3 | 2 | a1i 11 |
. . . . 5
⊢ (𝑟 = 𝑅 → (Base‘𝑟) ∈ V) |
4 | | id 22 |
. . . . . . . . 9
⊢ (𝑏 = (Base‘𝑟) → 𝑏 = (Base‘𝑟)) |
5 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = (Base‘𝑅)) |
6 | | evl1fval.b |
. . . . . . . . . 10
⊢ 𝐵 = (Base‘𝑅) |
7 | 5, 6 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝑟 = 𝑅 → (Base‘𝑟) = 𝐵) |
8 | 4, 7 | sylan9eqr 2666 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → 𝑏 = 𝐵) |
9 | 8 | oveq1d 6564 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → (𝑏 ↑𝑚
1𝑜) = (𝐵
↑𝑚 1𝑜)) |
10 | 8, 9 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) = (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜))) |
11 | 8 | mpteq1d 4666 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})) = (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦}))) |
12 | 11 | coeq2d 5206 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦}))) = (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) |
13 | 10, 12 | mpteq12dv 4663 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → (𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})))) = (𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦}))))) |
14 | | simpl 472 |
. . . . . . . 8
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → 𝑟 = 𝑅) |
15 | 14 | oveq2d 6565 |
. . . . . . 7
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → (1𝑜 eval 𝑟) = (1𝑜 eval
𝑅)) |
16 | | evl1fval.q |
. . . . . . 7
⊢ 𝑄 = (1𝑜 eval
𝑅) |
17 | 15, 16 | syl6eqr 2662 |
. . . . . 6
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → (1𝑜 eval 𝑟) = 𝑄) |
18 | 13, 17 | coeq12d 5208 |
. . . . 5
⊢ ((𝑟 = 𝑅 ∧ 𝑏 = (Base‘𝑟)) → ((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})))) ∘
(1𝑜 eval 𝑟)) = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘ 𝑄)) |
19 | 3, 18 | csbied 3526 |
. . . 4
⊢ (𝑟 = 𝑅 → ⦋(Base‘𝑟) / 𝑏⦌((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})))) ∘
(1𝑜 eval 𝑟)) = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘ 𝑄)) |
20 | | df-evl1 19502 |
. . . 4
⊢
eval1 = (𝑟 ∈ V ↦
⦋(Base‘𝑟) / 𝑏⦌((𝑥 ∈ (𝑏 ↑𝑚 (𝑏 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝑏 ↦ (1𝑜 ×
{𝑦})))) ∘
(1𝑜 eval 𝑟))) |
21 | | ovex 6577 |
. . . . . 6
⊢ (𝐵 ↑𝑚
(𝐵
↑𝑚 1𝑜)) ∈ V |
22 | 21 | mptex 6390 |
. . . . 5
⊢ (𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∈
V |
23 | | ovex 6577 |
. . . . . 6
⊢
(1𝑜 eval 𝑅) ∈ V |
24 | 16, 23 | eqeltri 2684 |
. . . . 5
⊢ 𝑄 ∈ V |
25 | 22, 24 | coex 7011 |
. . . 4
⊢ ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘ 𝑄) ∈ V |
26 | 19, 20, 25 | fvmpt 6191 |
. . 3
⊢ (𝑅 ∈ V →
(eval1‘𝑅)
= ((𝑥 ∈ (𝐵 ↑𝑚
(𝐵
↑𝑚 1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘ 𝑄)) |
27 | 1, 26 | syl5eq 2656 |
. 2
⊢ (𝑅 ∈ V → 𝑂 = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘ 𝑄)) |
28 | | fvprc 6097 |
. . . . 5
⊢ (¬
𝑅 ∈ V →
(eval1‘𝑅)
= ∅) |
29 | 1, 28 | syl5eq 2656 |
. . . 4
⊢ (¬
𝑅 ∈ V → 𝑂 = ∅) |
30 | | co02 5566 |
. . . 4
⊢ ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘ ∅) =
∅ |
31 | 29, 30 | syl6eqr 2662 |
. . 3
⊢ (¬
𝑅 ∈ V → 𝑂 = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘
∅)) |
32 | | df-evl 19328 |
. . . . . . 7
⊢ eval =
(𝑖 ∈ V, 𝑟 ∈ V ↦ ((𝑖 evalSub 𝑟)‘(Base‘𝑟))) |
33 | 32 | reldmmpt2 6669 |
. . . . . 6
⊢ Rel dom
eval |
34 | 33 | ovprc2 6583 |
. . . . 5
⊢ (¬
𝑅 ∈ V →
(1𝑜 eval 𝑅) = ∅) |
35 | 16, 34 | syl5eq 2656 |
. . . 4
⊢ (¬
𝑅 ∈ V → 𝑄 = ∅) |
36 | 35 | coeq2d 5206 |
. . 3
⊢ (¬
𝑅 ∈ V → ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘ 𝑄) = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘
∅)) |
37 | 31, 36 | eqtr4d 2647 |
. 2
⊢ (¬
𝑅 ∈ V → 𝑂 = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘ 𝑄)) |
38 | 27, 37 | pm2.61i 175 |
1
⊢ 𝑂 = ((𝑥 ∈ (𝐵 ↑𝑚 (𝐵 ↑𝑚
1𝑜)) ↦ (𝑥 ∘ (𝑦 ∈ 𝐵 ↦ (1𝑜 ×
{𝑦})))) ∘ 𝑄) |