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 30674 |
. . . . 5
⊢ (𝑇 ∈ V → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉))) |
7 | 6 | adantr 480 |
. . . 4
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → 𝑆 = (𝑓 ∈ (𝑅 ↑pm 𝑉) ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉))) |
8 | | simplr 788 |
. . . . . . . 8
⊢ ((((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) ∧ 𝑒 ∈ 𝐸) → 𝑓 = 𝐹) |
9 | 8 | fveq2d 6107 |
. . . . . . 7
⊢ ((((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) ∧ 𝑒 ∈ 𝐸) → (𝑂‘𝑓) = (𝑂‘𝐹)) |
10 | 9 | fveq1d 6105 |
. . . . . 6
⊢ ((((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) ∧ 𝑒 ∈ 𝐸) → ((𝑂‘𝑓)‘(2nd ‘𝑒)) = ((𝑂‘𝐹)‘(2nd ‘𝑒))) |
11 | 10 | opeq2d 4347 |
. . . . 5
⊢ ((((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) ∧ 𝑒 ∈ 𝐸) → 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉 = 〈(1st
‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) |
12 | 11 | mpteq2dva 4672 |
. . . 4
⊢ (((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) ∧ 𝑓 = 𝐹) → (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑓)‘(2nd ‘𝑒))〉) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) |
13 | | fvex 6113 |
. . . . . . . 8
⊢
(mREx‘𝑇)
∈ V |
14 | 2, 13 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑅 ∈ V |
15 | | fvex 6113 |
. . . . . . . 8
⊢
(mVR‘𝑇) ∈
V |
16 | 1, 15 | eqeltri 2684 |
. . . . . . 7
⊢ 𝑉 ∈ V |
17 | 14, 16 | pm3.2i 470 |
. . . . . 6
⊢ (𝑅 ∈ V ∧ 𝑉 ∈ V) |
18 | 17 | a1i 11 |
. . . . 5
⊢ (𝑇 ∈ V → (𝑅 ∈ V ∧ 𝑉 ∈ V)) |
19 | | elpm2r 7761 |
. . . . 5
⊢ (((𝑅 ∈ V ∧ 𝑉 ∈ V) ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → 𝐹 ∈ (𝑅 ↑pm 𝑉)) |
20 | 18, 19 | sylan 487 |
. . . 4
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → 𝐹 ∈ (𝑅 ↑pm 𝑉)) |
21 | | fvex 6113 |
. . . . . . 7
⊢
(mEx‘𝑇) ∈
V |
22 | 4, 21 | eqeltri 2684 |
. . . . . 6
⊢ 𝐸 ∈ V |
23 | 22 | mptex 6390 |
. . . . 5
⊢ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) ∈
V |
24 | 23 | a1i 11 |
. . . 4
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) ∈
V) |
25 | 7, 12, 20, 24 | fvmptd 6197 |
. . 3
⊢ ((𝑇 ∈ V ∧ (𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉)) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) |
26 | 25 | ex 449 |
. 2
⊢ (𝑇 ∈ V → ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉))) |
27 | | 0fv 6137 |
. . . . 5
⊢
(∅‘𝐹) =
∅ |
28 | | mpt0 5934 |
. . . . 5
⊢ (𝑒 ∈ ∅ ↦
〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) =
∅ |
29 | 27, 28 | eqtr4i 2635 |
. . . 4
⊢
(∅‘𝐹) =
(𝑒 ∈ ∅ ↦
〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) |
30 | | fvprc 6097 |
. . . . . 6
⊢ (¬
𝑇 ∈ V →
(mSubst‘𝑇) =
∅) |
31 | 3, 30 | syl5eq 2656 |
. . . . 5
⊢ (¬
𝑇 ∈ V → 𝑆 = ∅) |
32 | 31 | fveq1d 6105 |
. . . 4
⊢ (¬
𝑇 ∈ V → (𝑆‘𝐹) = (∅‘𝐹)) |
33 | | fvprc 6097 |
. . . . . 6
⊢ (¬
𝑇 ∈ V →
(mEx‘𝑇) =
∅) |
34 | 4, 33 | syl5eq 2656 |
. . . . 5
⊢ (¬
𝑇 ∈ V → 𝐸 = ∅) |
35 | 34 | mpteq1d 4666 |
. . . 4
⊢ (¬
𝑇 ∈ V → (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉) = (𝑒 ∈ ∅ ↦ 〈(1st
‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) |
36 | 29, 32, 35 | 3eqtr4a 2670 |
. . 3
⊢ (¬
𝑇 ∈ V → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) |
37 | 36 | a1d 25 |
. 2
⊢ (¬
𝑇 ∈ V → ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉))) |
38 | 26, 37 | pm2.61i 175 |
1
⊢ ((𝐹:𝐴⟶𝑅 ∧ 𝐴 ⊆ 𝑉) → (𝑆‘𝐹) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝐹)‘(2nd ‘𝑒))〉)) |