Step | Hyp | Ref
| Expression |
1 | | msubffval.v |
. . . . . 6
⊢ 𝑉 = (mVR‘𝑇) |
2 | | msubffval.r |
. . . . . 6
⊢ 𝑅 = (mREx‘𝑇) |
3 | | msubffval.s |
. . . . . 6
⊢ 𝑆 = (mSubst‘𝑇) |
4 | | msubffval.e |
. . . . . 6
⊢ 𝐸 = (mEx‘𝑇) |
5 | | msubffval.o |
. . . . . 6
⊢ 𝑂 = (mRSubst‘𝑇) |
6 | 1, 2, 3, 4, 5 | msubffval 33485 |
. . . . 5
⊢ (𝑇 ∈ V → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉))) |
7 | 6 | adantr 481 |
. . . 4
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉))) |
8 | | simplr 766 |
. . . . . . . 8
⊢ ((((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) ∧ 𝑒 ∈ 𝐸) → 𝑓 = 𝐹) |
9 | 8 | fveq2d 6778 |
. . . . . . 7
⊢ ((((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) ∧ 𝑒 ∈ 𝐸) → (𝑂‘𝑓) = (𝑂‘𝐹)) |
10 | 9 | fveq1d 6776 |
. . . . . 6
⊢ ((((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) ∧ 𝑒 ∈ 𝐸) → ((𝑂‘𝑓)‘(2nd ‘𝑒)) = ((𝑂‘𝐹)‘(2nd ‘𝑒))) |
11 | 10 | opeq2d 4811 |
. . . . 5
⊢ ((((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) ∧ 𝑒 ∈ 𝐸) → 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉 = 〈(1st
‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) |
12 | 11 | mpteq2dva 5174 |
. . . 4
⊢ (((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) → (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) |
13 | 2 | fvexi 6788 |
. . . . . . 7
⊢ 𝑅 ∈ V |
14 | 1 | fvexi 6788 |
. . . . . . 7
⊢ 𝑉 ∈ V |
15 | 13, 14 | pm3.2i 471 |
. . . . . 6
⊢ (𝑅 ∈ V ∧ 𝑉 ∈ V) |
16 | 15 | a1i 11 |
. . . . 5
⊢ (𝑇 ∈ V → (𝑅 ∈ V ∧ 𝑉 ∈ V)) |
17 | | elpm2r 8633 |
. . . . 5
⊢ (((𝑅 ∈ V ∧ 𝑉 ∈ V) ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → 𝐹 ∈ (𝑅 ↑pm 𝑉)) |
18 | 16, 17 | sylan 580 |
. . . 4
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → 𝐹 ∈ (𝑅 ↑pm 𝑉)) |
19 | 4 | fvexi 6788 |
. . . . . 6
⊢ 𝐸 ∈ V |
20 | 19 | mptex 7099 |
. . . . 5
⊢ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) ∈
V |
21 | 20 | a1i 11 |
. . . 4
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) ∈
V) |
22 | 7, 12, 18, 21 | fvmptd 6882 |
. . 3
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) |
23 | 22 | ex 413 |
. 2
⊢ (𝑇 ∈ V → ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉))) |
24 | | 0fv 6813 |
. . . . 5
⊢
(∅‘𝐹) =
∅ |
25 | | mpt0 6575 |
. . . . 5
⊢ (𝑒 ∈ ∅ ↦
〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) =
∅ |
26 | 24, 25 | eqtr4i 2769 |
. . . 4
⊢
(∅‘𝐹) =
(𝑒 ∈ ∅ ↦
〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) |
27 | | fvprc 6766 |
. . . . . 6
⊢ (¬
𝑇 ∈ V →
(mSubst‘𝑇) =
∅) |
28 | 3, 27 | eqtrid 2790 |
. . . . 5
⊢ (¬
𝑇 ∈ V → 𝑆 = ∅) |
29 | 28 | fveq1d 6776 |
. . . 4
⊢ (¬
𝑇 ∈ V → (𝑆‘𝐹) = (∅‘𝐹)) |
30 | | fvprc 6766 |
. . . . . 6
⊢ (¬
𝑇 ∈ V →
(mEx‘𝑇) =
∅) |
31 | 4, 30 | eqtrid 2790 |
. . . . 5
⊢ (¬
𝑇 ∈ V → 𝐸 = ∅) |
32 | 31 | mpteq1d 5169 |
. . . 4
⊢ (¬
𝑇 ∈ V → (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) = (𝑒 ∈ ∅ ↦ 〈(1st
‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) |
33 | 26, 29, 32 | 3eqtr4a 2804 |
. . 3
⊢ (¬
𝑇 ∈ V → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) |
34 | 33 | a1d 25 |
. 2
⊢ (¬
𝑇 ∈ V → ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉))) |
35 | 23, 34 | pm2.61i 182 |
1
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) |