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 33056 |
. . . . 5
⊢ (𝑇 ∈ V → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉))) |
7 | 6 | adantr 484 |
. . . 4
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉))) |
8 | | simplr 769 |
. . . . . . . 8
⊢ ((((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) ∧ 𝑒 ∈ 𝐸) → 𝑓 = 𝐹) |
9 | 8 | fveq2d 6678 |
. . . . . . 7
⊢ ((((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) ∧ 𝑒 ∈ 𝐸) → (𝑂‘𝑓) = (𝑂‘𝐹)) |
10 | 9 | fveq1d 6676 |
. . . . . 6
⊢ ((((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) ∧ 𝑒 ∈ 𝐸) → ((𝑂‘𝑓)‘(2nd ‘𝑒)) = ((𝑂‘𝐹)‘(2nd ‘𝑒))) |
11 | 10 | opeq2d 4768 |
. . . . 5
⊢ ((((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) ∧ 𝑒 ∈ 𝐸) → 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉 = 〈(1st
‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) |
12 | 11 | mpteq2dva 5125 |
. . . 4
⊢ (((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) → (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) |
13 | 2 | fvexi 6688 |
. . . . . . 7
⊢ 𝑅 ∈ V |
14 | 1 | fvexi 6688 |
. . . . . . 7
⊢ 𝑉 ∈ V |
15 | 13, 14 | pm3.2i 474 |
. . . . . 6
⊢ (𝑅 ∈ V ∧ 𝑉 ∈ V) |
16 | 15 | a1i 11 |
. . . . 5
⊢ (𝑇 ∈ V → (𝑅 ∈ V ∧ 𝑉 ∈ V)) |
17 | | elpm2r 8455 |
. . . . 5
⊢ (((𝑅 ∈ V ∧ 𝑉 ∈ V) ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → 𝐹 ∈ (𝑅 ↑pm 𝑉)) |
18 | 16, 17 | sylan 583 |
. . . 4
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → 𝐹 ∈ (𝑅 ↑pm 𝑉)) |
19 | 4 | fvexi 6688 |
. . . . . 6
⊢ 𝐸 ∈ V |
20 | 19 | mptex 6996 |
. . . . 5
⊢ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) ∈
V |
21 | 20 | a1i 11 |
. . . 4
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) ∈
V) |
22 | 7, 12, 18, 21 | fvmptd 6782 |
. . 3
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) |
23 | 22 | ex 416 |
. 2
⊢ (𝑇 ∈ V → ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉))) |
24 | | 0fv 6713 |
. . . . 5
⊢
(∅‘𝐹) =
∅ |
25 | | mpt0 6479 |
. . . . 5
⊢ (𝑒 ∈ ∅ ↦
〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) =
∅ |
26 | 24, 25 | eqtr4i 2764 |
. . . 4
⊢
(∅‘𝐹) =
(𝑒 ∈ ∅ ↦
〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) |
27 | | fvprc 6666 |
. . . . . 6
⊢ (¬
𝑇 ∈ V →
(mSubst‘𝑇) =
∅) |
28 | 3, 27 | syl5eq 2785 |
. . . . 5
⊢ (¬
𝑇 ∈ V → 𝑆 = ∅) |
29 | 28 | fveq1d 6676 |
. . . 4
⊢ (¬
𝑇 ∈ V → (𝑆‘𝐹) = (∅‘𝐹)) |
30 | | fvprc 6666 |
. . . . . 6
⊢ (¬
𝑇 ∈ V →
(mEx‘𝑇) =
∅) |
31 | 4, 30 | syl5eq 2785 |
. . . . 5
⊢ (¬
𝑇 ∈ V → 𝐸 = ∅) |
32 | 31 | mpteq1d 5119 |
. . . 4
⊢ (¬
𝑇 ∈ V → (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) = (𝑒 ∈ ∅ ↦ 〈(1st
‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) |
33 | 26, 29, 32 | 3eqtr4a 2799 |
. . 3
⊢ (¬
𝑇 ∈ V → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) |
34 | 33 | a1d 25 |
. 2
⊢ (¬
𝑇 ∈ V → ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉))) |
35 | 23, 34 | pm2.61i 185 |
1
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) |