| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢
(mEx‘𝑇) =
(mEx‘𝑇) |
| 2 | | eqid 2737 |
. . . . 5
⊢
(mRSubst‘𝑇) =
(mRSubst‘𝑇) |
| 3 | | msubco.s |
. . . . 5
⊢ 𝑆 = (mSubst‘𝑇) |
| 4 | 1, 2, 3 | elmsubrn 35533 |
. . . 4
⊢ ran 𝑆 = ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉)) |
| 5 | 4 | eleq2i 2833 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉))) |
| 6 | | eqid 2737 |
. . . 4
⊢ (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉)) = (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉)) |
| 7 | | fvex 6919 |
. . . . 5
⊢
(mEx‘𝑇) ∈
V |
| 8 | 7 | mptex 7243 |
. . . 4
⊢ (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑥), (𝑓‘(2nd
‘𝑥))〉) ∈
V |
| 9 | 6, 8 | elrnmpti 5973 |
. . 3
⊢ (𝐹 ∈ ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉)) ↔ ∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉)) |
| 10 | 5, 9 | bitri 275 |
. 2
⊢ (𝐹 ∈ ran 𝑆 ↔ ∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉)) |
| 11 | 1, 2, 3 | elmsubrn 35533 |
. . . 4
⊢ ran 𝑆 = ran (𝑔 ∈ ran (mRSubst‘𝑇) ↦ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) |
| 12 | 11 | eleq2i 2833 |
. . 3
⊢ (𝐺 ∈ ran 𝑆 ↔ 𝐺 ∈ ran (𝑔 ∈ ran (mRSubst‘𝑇) ↦ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉))) |
| 13 | | eqid 2737 |
. . . 4
⊢ (𝑔 ∈ ran (mRSubst‘𝑇) ↦ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) = (𝑔 ∈ ran (mRSubst‘𝑇) ↦ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) |
| 14 | 7 | mptex 7243 |
. . . 4
⊢ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉) ∈
V |
| 15 | 13, 14 | elrnmpti 5973 |
. . 3
⊢ (𝐺 ∈ ran (𝑔 ∈ ran (mRSubst‘𝑇) ↦ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) ↔ ∃𝑔 ∈ ran (mRSubst‘𝑇)𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) |
| 16 | 12, 15 | bitri 275 |
. 2
⊢ (𝐺 ∈ ran 𝑆 ↔ ∃𝑔 ∈ ran (mRSubst‘𝑇)𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) |
| 17 | | reeanv 3229 |
. . 3
⊢
(∃𝑓 ∈ ran
(mRSubst‘𝑇)∃𝑔 ∈ ran (mRSubst‘𝑇)(𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∧ 𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) ↔ (∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∧ ∃𝑔 ∈ ran (mRSubst‘𝑇)𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉))) |
| 18 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → 𝑦 ∈ (mEx‘𝑇)) |
| 19 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(mTC‘𝑇) =
(mTC‘𝑇) |
| 20 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(mREx‘𝑇) =
(mREx‘𝑇) |
| 21 | 19, 1, 20 | mexval 35507 |
. . . . . . . . . . . 12
⊢
(mEx‘𝑇) =
((mTC‘𝑇) ×
(mREx‘𝑇)) |
| 22 | 18, 21 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → 𝑦 ∈ ((mTC‘𝑇) × (mREx‘𝑇))) |
| 23 | | xp1st 8046 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((mTC‘𝑇) × (mREx‘𝑇)) → (1st
‘𝑦) ∈
(mTC‘𝑇)) |
| 24 | 22, 23 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → (1st ‘𝑦) ∈ (mTC‘𝑇)) |
| 25 | 2, 20 | mrsubf 35522 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ ran (mRSubst‘𝑇) → 𝑔:(mREx‘𝑇)⟶(mREx‘𝑇)) |
| 26 | 25 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → 𝑔:(mREx‘𝑇)⟶(mREx‘𝑇)) |
| 27 | | xp2nd 8047 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ((mTC‘𝑇) × (mREx‘𝑇)) → (2nd
‘𝑦) ∈
(mREx‘𝑇)) |
| 28 | 22, 27 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → (2nd ‘𝑦) ∈ (mREx‘𝑇)) |
| 29 | 26, 28 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → (𝑔‘(2nd ‘𝑦)) ∈ (mREx‘𝑇)) |
| 30 | | opelxpi 5722 |
. . . . . . . . . 10
⊢
(((1st ‘𝑦) ∈ (mTC‘𝑇) ∧ (𝑔‘(2nd ‘𝑦)) ∈ (mREx‘𝑇)) → 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉 ∈
((mTC‘𝑇) ×
(mREx‘𝑇))) |
| 31 | 24, 29, 30 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉 ∈
((mTC‘𝑇) ×
(mREx‘𝑇))) |
| 32 | 31, 21 | eleqtrrdi 2852 |
. . . . . . . 8
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉 ∈ (mEx‘𝑇)) |
| 33 | | eqidd 2738 |
. . . . . . . 8
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) → (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉) = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) |
| 34 | | eqidd 2738 |
. . . . . . . 8
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) → (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉)) |
| 35 | | fvex 6919 |
. . . . . . . . . 10
⊢
(1st ‘𝑦) ∈ V |
| 36 | | fvex 6919 |
. . . . . . . . . 10
⊢ (𝑔‘(2nd
‘𝑦)) ∈
V |
| 37 | 35, 36 | op1std 8024 |
. . . . . . . . 9
⊢ (𝑥 = 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉 →
(1st ‘𝑥) =
(1st ‘𝑦)) |
| 38 | 35, 36 | op2ndd 8025 |
. . . . . . . . . 10
⊢ (𝑥 = 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉 →
(2nd ‘𝑥) =
(𝑔‘(2nd
‘𝑦))) |
| 39 | 38 | fveq2d 6910 |
. . . . . . . . 9
⊢ (𝑥 = 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉 →
(𝑓‘(2nd
‘𝑥)) = (𝑓‘(𝑔‘(2nd ‘𝑦)))) |
| 40 | 37, 39 | opeq12d 4881 |
. . . . . . . 8
⊢ (𝑥 = 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉 →
〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉 = 〈(1st
‘𝑦), (𝑓‘(𝑔‘(2nd ‘𝑦)))〉) |
| 41 | 32, 33, 34, 40 | fmptco 7149 |
. . . . . . 7
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) → ((𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∘ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉)) = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), (𝑓‘(𝑔‘(2nd ‘𝑦)))〉)) |
| 42 | | fvco3 7008 |
. . . . . . . . . 10
⊢ ((𝑔:(mREx‘𝑇)⟶(mREx‘𝑇) ∧ (2nd ‘𝑦) ∈ (mREx‘𝑇)) → ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦)) = (𝑓‘(𝑔‘(2nd ‘𝑦)))) |
| 43 | 26, 28, 42 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦)) = (𝑓‘(𝑔‘(2nd ‘𝑦)))) |
| 44 | 43 | opeq2d 4880 |
. . . . . . . 8
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → 〈(1st ‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉 = 〈(1st
‘𝑦), (𝑓‘(𝑔‘(2nd ‘𝑦)))〉) |
| 45 | 44 | mpteq2dva 5242 |
. . . . . . 7
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) → (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉) = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑓‘(𝑔‘(2nd ‘𝑦)))〉)) |
| 46 | 41, 45 | eqtr4d 2780 |
. . . . . 6
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) → ((𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∘ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉)) = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉)) |
| 47 | 2 | mrsubco 35526 |
. . . . . . . 8
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) → (𝑓 ∘ 𝑔) ∈ ran (mRSubst‘𝑇)) |
| 48 | 7 | mptex 7243 |
. . . . . . . 8
⊢ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉) ∈
V |
| 49 | | eqid 2737 |
. . . . . . . . 9
⊢ (ℎ ∈ ran (mRSubst‘𝑇) ↦ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (ℎ‘(2nd ‘𝑦))〉)) = (ℎ ∈ ran (mRSubst‘𝑇) ↦ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (ℎ‘(2nd ‘𝑦))〉)) |
| 50 | | fveq1 6905 |
. . . . . . . . . . 11
⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ‘(2nd ‘𝑦)) = ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))) |
| 51 | 50 | opeq2d 4880 |
. . . . . . . . . 10
⊢ (ℎ = (𝑓 ∘ 𝑔) → 〈(1st ‘𝑦), (ℎ‘(2nd ‘𝑦))〉 = 〈(1st
‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉) |
| 52 | 51 | mpteq2dv 5244 |
. . . . . . . . 9
⊢ (ℎ = (𝑓 ∘ 𝑔) → (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (ℎ‘(2nd ‘𝑦))〉) = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉)) |
| 53 | 49, 52 | elrnmpt1s 5970 |
. . . . . . . 8
⊢ (((𝑓 ∘ 𝑔) ∈ ran (mRSubst‘𝑇) ∧ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉) ∈ V) →
(𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉) ∈ ran (ℎ ∈ ran (mRSubst‘𝑇) ↦ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (ℎ‘(2nd ‘𝑦))〉))) |
| 54 | 47, 48, 53 | sylancl 586 |
. . . . . . 7
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) → (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉) ∈ ran (ℎ ∈ ran (mRSubst‘𝑇) ↦ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (ℎ‘(2nd ‘𝑦))〉))) |
| 55 | 1, 2, 3 | elmsubrn 35533 |
. . . . . . 7
⊢ ran 𝑆 = ran (ℎ ∈ ran (mRSubst‘𝑇) ↦ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (ℎ‘(2nd ‘𝑦))〉)) |
| 56 | 54, 55 | eleqtrrdi 2852 |
. . . . . 6
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) → (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉) ∈ ran 𝑆) |
| 57 | 46, 56 | eqeltrd 2841 |
. . . . 5
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) → ((𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∘ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉)) ∈
ran 𝑆) |
| 58 | | coeq1 5868 |
. . . . . . 7
⊢ (𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) → (𝐹 ∘ 𝐺) = ((𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∘ 𝐺)) |
| 59 | | coeq2 5869 |
. . . . . . 7
⊢ (𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉) → ((𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑥), (𝑓‘(2nd
‘𝑥))〉) ∘
𝐺) = ((𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∘ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉))) |
| 60 | 58, 59 | sylan9eq 2797 |
. . . . . 6
⊢ ((𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∧ 𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) → (𝐹 ∘ 𝐺) = ((𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∘ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉))) |
| 61 | 60 | eleq1d 2826 |
. . . . 5
⊢ ((𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∧ 𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) → ((𝐹 ∘ 𝐺) ∈ ran 𝑆 ↔ ((𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∘ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉)) ∈
ran 𝑆)) |
| 62 | 57, 61 | syl5ibrcom 247 |
. . . 4
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) → ((𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∧ 𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) → (𝐹 ∘ 𝐺) ∈ ran 𝑆)) |
| 63 | 62 | rexlimivv 3201 |
. . 3
⊢
(∃𝑓 ∈ ran
(mRSubst‘𝑇)∃𝑔 ∈ ran (mRSubst‘𝑇)(𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∧ 𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) → (𝐹 ∘ 𝐺) ∈ ran 𝑆) |
| 64 | 17, 63 | sylbir 235 |
. 2
⊢
((∃𝑓 ∈
ran (mRSubst‘𝑇)𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∧ ∃𝑔 ∈ ran (mRSubst‘𝑇)𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) → (𝐹 ∘ 𝐺) ∈ ran 𝑆) |
| 65 | 10, 16, 64 | syl2anb 598 |
1
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺) ∈ ran 𝑆) |