Step | Hyp | Ref
| Expression |
1 | | staffval.f |
. 2
⊢ ∙ =
(*rf‘𝑅) |
2 | | fveq2 6103 |
. . . . . 6
⊢ (𝑓 = 𝑅 → (Base‘𝑓) = (Base‘𝑅)) |
3 | | staffval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
4 | 2, 3 | syl6eqr 2662 |
. . . . 5
⊢ (𝑓 = 𝑅 → (Base‘𝑓) = 𝐵) |
5 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑓 = 𝑅 → (*𝑟‘𝑓) =
(*𝑟‘𝑅)) |
6 | | staffval.i |
. . . . . . 7
⊢ ∗ =
(*𝑟‘𝑅) |
7 | 5, 6 | syl6eqr 2662 |
. . . . . 6
⊢ (𝑓 = 𝑅 → (*𝑟‘𝑓) = ∗ ) |
8 | 7 | fveq1d 6105 |
. . . . 5
⊢ (𝑓 = 𝑅 → ((*𝑟‘𝑓)‘𝑥) = ( ∗ ‘𝑥)) |
9 | 4, 8 | mpteq12dv 4663 |
. . . 4
⊢ (𝑓 = 𝑅 → (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟‘𝑓)‘𝑥)) = (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥))) |
10 | | df-staf 18668 |
. . . 4
⊢
*rf = (𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟‘𝑓)‘𝑥))) |
11 | | eqid 2610 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)) = (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)) |
12 | | fvrn0 6126 |
. . . . . . 7
⊢ ( ∗
‘𝑥) ∈ (ran ∗ ∪
{∅}) |
13 | 12 | a1i 11 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵 → ( ∗ ‘𝑥) ∈ (ran ∗ ∪
{∅})) |
14 | 11, 13 | fmpti 6291 |
. . . . 5
⊢ (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)):𝐵⟶(ran ∗ ∪
{∅}) |
15 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑅)
∈ V |
16 | 3, 15 | eqeltri 2684 |
. . . . 5
⊢ 𝐵 ∈ V |
17 | | fvex 6113 |
. . . . . . . 8
⊢
(*𝑟‘𝑅) ∈ V |
18 | 6, 17 | eqeltri 2684 |
. . . . . . 7
⊢ ∗ ∈
V |
19 | 18 | rnex 6992 |
. . . . . 6
⊢ ran ∗ ∈
V |
20 | | p0ex 4779 |
. . . . . 6
⊢ {∅}
∈ V |
21 | 19, 20 | unex 6854 |
. . . . 5
⊢ (ran
∗
∪ {∅}) ∈ V |
22 | | fex2 7014 |
. . . . 5
⊢ (((𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)):𝐵⟶(ran ∗ ∪ {∅})
∧ 𝐵 ∈ V ∧ (ran
∗
∪ {∅}) ∈ V) → (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)) ∈ V) |
23 | 14, 16, 21, 22 | mp3an 1416 |
. . . 4
⊢ (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)) ∈ V |
24 | 9, 10, 23 | fvmpt 6191 |
. . 3
⊢ (𝑅 ∈ V →
(*rf‘𝑅) = (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥))) |
25 | | fvprc 6097 |
. . . . 5
⊢ (¬
𝑅 ∈ V →
(*rf‘𝑅) = ∅) |
26 | | mpt0 5934 |
. . . . 5
⊢ (𝑥 ∈ ∅ ↦ ( ∗
‘𝑥)) =
∅ |
27 | 25, 26 | syl6eqr 2662 |
. . . 4
⊢ (¬
𝑅 ∈ V →
(*rf‘𝑅) = (𝑥 ∈ ∅ ↦ ( ∗ ‘𝑥))) |
28 | | fvprc 6097 |
. . . . . 6
⊢ (¬
𝑅 ∈ V →
(Base‘𝑅) =
∅) |
29 | 3, 28 | syl5eq 2656 |
. . . . 5
⊢ (¬
𝑅 ∈ V → 𝐵 = ∅) |
30 | 29 | mpteq1d 4666 |
. . . 4
⊢ (¬
𝑅 ∈ V → (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)) = (𝑥 ∈ ∅ ↦ ( ∗ ‘𝑥))) |
31 | 27, 30 | eqtr4d 2647 |
. . 3
⊢ (¬
𝑅 ∈ V →
(*rf‘𝑅) = (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥))) |
32 | 24, 31 | pm2.61i 175 |
. 2
⊢
(*rf‘𝑅) = (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)) |
33 | 1, 32 | eqtri 2632 |
1
⊢ ∙ =
(𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)) |