Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . . 6
⊢
(mVR‘𝑇) =
(mVR‘𝑇) |
2 | | eqid 2622 |
. . . . . 6
⊢
(mREx‘𝑇) =
(mREx‘𝑇) |
3 | | elmsubrn.s |
. . . . . 6
⊢ 𝑆 = (mSubst‘𝑇) |
4 | | elmsubrn.e |
. . . . . 6
⊢ 𝐸 = (mEx‘𝑇) |
5 | | elmsubrn.o |
. . . . . 6
⊢ 𝑂 = (mRSubst‘𝑇) |
6 | 1, 2, 3, 4, 5 | msubffval 31420 |
. . . . 5
⊢ (𝑇 ∈ V → 𝑆 = (𝑔 ∈ ((mREx‘𝑇) ↑pm
(mVR‘𝑇)) ↦
(𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑔)‘(2nd ‘𝑒))〉))) |
7 | 1, 2, 5 | mrsubff 31409 |
. . . . . . . 8
⊢ (𝑇 ∈ V → 𝑂:((mREx‘𝑇) ↑pm
(mVR‘𝑇))⟶((mREx‘𝑇) ↑𝑚
(mREx‘𝑇))) |
8 | | ffn 6045 |
. . . . . . . 8
⊢ (𝑂:((mREx‘𝑇) ↑pm
(mVR‘𝑇))⟶((mREx‘𝑇) ↑𝑚
(mREx‘𝑇)) →
𝑂 Fn ((mREx‘𝑇) ↑pm
(mVR‘𝑇))) |
9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (𝑇 ∈ V → 𝑂 Fn ((mREx‘𝑇) ↑pm
(mVR‘𝑇))) |
10 | | fnfvelrn 6356 |
. . . . . . 7
⊢ ((𝑂 Fn ((mREx‘𝑇) ↑pm
(mVR‘𝑇)) ∧ 𝑔 ∈ ((mREx‘𝑇) ↑pm
(mVR‘𝑇))) →
(𝑂‘𝑔) ∈ ran 𝑂) |
11 | 9, 10 | sylan 488 |
. . . . . 6
⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ ((mREx‘𝑇) ↑pm
(mVR‘𝑇))) →
(𝑂‘𝑔) ∈ ran 𝑂) |
12 | 7 | feqmptd 6249 |
. . . . . 6
⊢ (𝑇 ∈ V → 𝑂 = (𝑔 ∈ ((mREx‘𝑇) ↑pm
(mVR‘𝑇)) ↦
(𝑂‘𝑔))) |
13 | | eqidd 2623 |
. . . . . 6
⊢ (𝑇 ∈ V → (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) = (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉))) |
14 | | fveq1 6190 |
. . . . . . . 8
⊢ (𝑓 = (𝑂‘𝑔) → (𝑓‘(2nd ‘𝑒)) = ((𝑂‘𝑔)‘(2nd ‘𝑒))) |
15 | 14 | opeq2d 4409 |
. . . . . . 7
⊢ (𝑓 = (𝑂‘𝑔) → 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉 = 〈(1st
‘𝑒), ((𝑂‘𝑔)‘(2nd ‘𝑒))〉) |
16 | 15 | mpteq2dv 4745 |
. . . . . 6
⊢ (𝑓 = (𝑂‘𝑔) → (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉) = (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑔)‘(2nd ‘𝑒))〉)) |
17 | 11, 12, 13, 16 | fmptco 6396 |
. . . . 5
⊢ (𝑇 ∈ V → ((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) ∘ 𝑂) = (𝑔 ∈ ((mREx‘𝑇) ↑pm
(mVR‘𝑇)) ↦
(𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), ((𝑂‘𝑔)‘(2nd ‘𝑒))〉))) |
18 | 6, 17 | eqtr4d 2659 |
. . . 4
⊢ (𝑇 ∈ V → 𝑆 = ((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) ∘ 𝑂)) |
19 | 18 | rneqd 5353 |
. . 3
⊢ (𝑇 ∈ V → ran 𝑆 = ran ((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) ∘ 𝑂)) |
20 | | rnco 5641 |
. . . 4
⊢ ran
((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) ∘ 𝑂) = ran ((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) ↾ ran 𝑂) |
21 | | ssid 3624 |
. . . . . 6
⊢ ran 𝑂 ⊆ ran 𝑂 |
22 | | resmpt 5449 |
. . . . . 6
⊢ (ran
𝑂 ⊆ ran 𝑂 → ((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) ↾ ran 𝑂) = (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉))) |
23 | 21, 22 | ax-mp 5 |
. . . . 5
⊢ ((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) ↾ ran 𝑂) = (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) |
24 | 23 | rneqi 5352 |
. . . 4
⊢ ran
((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) ↾ ran 𝑂) = ran (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) |
25 | 20, 24 | eqtri 2644 |
. . 3
⊢ ran
((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) ∘ 𝑂) = ran (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) |
26 | 19, 25 | syl6eq 2672 |
. 2
⊢ (𝑇 ∈ V → ran 𝑆 = ran (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉))) |
27 | | mpt0 6021 |
. . . . 5
⊢ (𝑓 ∈ ∅ ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) =
∅ |
28 | 27 | eqcomi 2631 |
. . . 4
⊢ ∅ =
(𝑓 ∈ ∅ ↦
(𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) |
29 | | fvprc 6185 |
. . . . 5
⊢ (¬
𝑇 ∈ V →
(mSubst‘𝑇) =
∅) |
30 | 3, 29 | syl5eq 2668 |
. . . 4
⊢ (¬
𝑇 ∈ V → 𝑆 = ∅) |
31 | | fvprc 6185 |
. . . . . . . 8
⊢ (¬
𝑇 ∈ V →
(mRSubst‘𝑇) =
∅) |
32 | 5, 31 | syl5eq 2668 |
. . . . . . 7
⊢ (¬
𝑇 ∈ V → 𝑂 = ∅) |
33 | 32 | rneqd 5353 |
. . . . . 6
⊢ (¬
𝑇 ∈ V → ran 𝑂 = ran ∅) |
34 | | rn0 5377 |
. . . . . 6
⊢ ran
∅ = ∅ |
35 | 33, 34 | syl6eq 2672 |
. . . . 5
⊢ (¬
𝑇 ∈ V → ran 𝑂 = ∅) |
36 | 35 | mpteq1d 4738 |
. . . 4
⊢ (¬
𝑇 ∈ V → (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) = (𝑓 ∈ ∅ ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉))) |
37 | 28, 30, 36 | 3eqtr4a 2682 |
. . 3
⊢ (¬
𝑇 ∈ V → 𝑆 = (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉))) |
38 | 37 | rneqd 5353 |
. 2
⊢ (¬
𝑇 ∈ V → ran 𝑆 = ran (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉))) |
39 | 26, 38 | pm2.61i 176 |
1
⊢ ran 𝑆 = ran (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ 〈(1st ‘𝑒), (𝑓‘(2nd ‘𝑒))〉)) |