| Step | Hyp | Ref
| Expression |
| 1 | | staffval.f |
. 2
⊢ ∙ =
(*rf‘𝑅) |
| 2 | | fveq2 6906 |
. . . . . 6
⊢ (𝑓 = 𝑅 → (Base‘𝑓) = (Base‘𝑅)) |
| 3 | | staffval.b |
. . . . . 6
⊢ 𝐵 = (Base‘𝑅) |
| 4 | 2, 3 | eqtr4di 2795 |
. . . . 5
⊢ (𝑓 = 𝑅 → (Base‘𝑓) = 𝐵) |
| 5 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑓 = 𝑅 → (*𝑟‘𝑓) =
(*𝑟‘𝑅)) |
| 6 | | staffval.i |
. . . . . . 7
⊢ ∗ =
(*𝑟‘𝑅) |
| 7 | 5, 6 | eqtr4di 2795 |
. . . . . 6
⊢ (𝑓 = 𝑅 → (*𝑟‘𝑓) = ∗ ) |
| 8 | 7 | fveq1d 6908 |
. . . . 5
⊢ (𝑓 = 𝑅 → ((*𝑟‘𝑓)‘𝑥) = ( ∗ ‘𝑥)) |
| 9 | 4, 8 | mpteq12dv 5233 |
. . . 4
⊢ (𝑓 = 𝑅 → (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟‘𝑓)‘𝑥)) = (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥))) |
| 10 | | df-staf 20840 |
. . . 4
⊢
*rf = (𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑓) ↦ ((*𝑟‘𝑓)‘𝑥))) |
| 11 | | eqid 2737 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)) = (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)) |
| 12 | | fvrn0 6936 |
. . . . . . 7
⊢ ( ∗
‘𝑥) ∈ (ran ∗ ∪
{∅}) |
| 13 | 12 | a1i 11 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵 → ( ∗ ‘𝑥) ∈ (ran ∗ ∪
{∅})) |
| 14 | 11, 13 | fmpti 7132 |
. . . . 5
⊢ (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)):𝐵⟶(ran ∗ ∪
{∅}) |
| 15 | 3 | fvexi 6920 |
. . . . 5
⊢ 𝐵 ∈ V |
| 16 | 6 | fvexi 6920 |
. . . . . . 7
⊢ ∗ ∈
V |
| 17 | 16 | rnex 7932 |
. . . . . 6
⊢ ran ∗ ∈
V |
| 18 | | p0ex 5384 |
. . . . . 6
⊢ {∅}
∈ V |
| 19 | 17, 18 | unex 7764 |
. . . . 5
⊢ (ran
∗
∪ {∅}) ∈ V |
| 20 | | fex2 7958 |
. . . . 5
⊢ (((𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)):𝐵⟶(ran ∗ ∪ {∅})
∧ 𝐵 ∈ V ∧ (ran
∗
∪ {∅}) ∈ V) → (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)) ∈ V) |
| 21 | 14, 15, 19, 20 | mp3an 1463 |
. . . 4
⊢ (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)) ∈ V |
| 22 | 9, 10, 21 | fvmpt 7016 |
. . 3
⊢ (𝑅 ∈ V →
(*rf‘𝑅) = (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥))) |
| 23 | | fvprc 6898 |
. . . . 5
⊢ (¬
𝑅 ∈ V →
(*rf‘𝑅) = ∅) |
| 24 | | mpt0 6710 |
. . . . 5
⊢ (𝑥 ∈ ∅ ↦ ( ∗
‘𝑥)) =
∅ |
| 25 | 23, 24 | eqtr4di 2795 |
. . . 4
⊢ (¬
𝑅 ∈ V →
(*rf‘𝑅) = (𝑥 ∈ ∅ ↦ ( ∗ ‘𝑥))) |
| 26 | | fvprc 6898 |
. . . . . 6
⊢ (¬
𝑅 ∈ V →
(Base‘𝑅) =
∅) |
| 27 | 3, 26 | eqtrid 2789 |
. . . . 5
⊢ (¬
𝑅 ∈ V → 𝐵 = ∅) |
| 28 | 27 | mpteq1d 5237 |
. . . 4
⊢ (¬
𝑅 ∈ V → (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)) = (𝑥 ∈ ∅ ↦ ( ∗ ‘𝑥))) |
| 29 | 25, 28 | eqtr4d 2780 |
. . 3
⊢ (¬
𝑅 ∈ V →
(*rf‘𝑅) = (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥))) |
| 30 | 22, 29 | pm2.61i 182 |
. 2
⊢
(*rf‘𝑅) = (𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)) |
| 31 | 1, 30 | eqtri 2765 |
1
⊢ ∙ =
(𝑥 ∈ 𝐵 ↦ ( ∗ ‘𝑥)) |