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 33203 |
. . . 4
⊢ ran 𝑆 = ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉)) |
5 | 4 | eleq2i 2829 |
. . 3
⊢ (𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉))) |
6 | | eqid 2737 |
. . . 4
⊢ (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉)) = (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉)) |
7 | | fvex 6730 |
. . . . 5
⊢
(mEx‘𝑇) ∈
V |
8 | 7 | mptex 7039 |
. . . 4
⊢ (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑥), (𝑓‘(2nd
‘𝑥))〉) ∈
V |
9 | 6, 8 | elrnmpti 5829 |
. . 3
⊢ (𝐹 ∈ ran (𝑓 ∈ ran (mRSubst‘𝑇) ↦ (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉)) ↔ ∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉)) |
10 | 5, 9 | bitri 278 |
. 2
⊢ (𝐹 ∈ ran 𝑆 ↔ ∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉)) |
11 | 1, 2, 3 | elmsubrn 33203 |
. . . 4
⊢ ran 𝑆 = ran (𝑔 ∈ ran (mRSubst‘𝑇) ↦ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) |
12 | 11 | eleq2i 2829 |
. . 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 7039 |
. . . 4
⊢ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉) ∈
V |
15 | 13, 14 | elrnmpti 5829 |
. . 3
⊢ (𝐺 ∈ ran (𝑔 ∈ ran (mRSubst‘𝑇) ↦ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) ↔ ∃𝑔 ∈ ran (mRSubst‘𝑇)𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) |
16 | 12, 15 | bitri 278 |
. 2
⊢ (𝐺 ∈ ran 𝑆 ↔ ∃𝑔 ∈ ran (mRSubst‘𝑇)𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) |
17 | | reeanv 3279 |
. . 3
⊢
(∃𝑓 ∈ ran
(mRSubst‘𝑇)∃𝑔 ∈ ran (mRSubst‘𝑇)(𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∧ 𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) ↔ (∃𝑓 ∈ ran (mRSubst‘𝑇)𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∧ ∃𝑔 ∈ ran (mRSubst‘𝑇)𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉))) |
18 | | simpr 488 |
. . . . . . . . . . . 12
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → 𝑦 ∈ (mEx‘𝑇)) |
19 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(mTC‘𝑇) =
(mTC‘𝑇) |
20 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(mREx‘𝑇) =
(mREx‘𝑇) |
21 | 19, 1, 20 | mexval 33177 |
. . . . . . . . . . . 12
⊢
(mEx‘𝑇) =
((mTC‘𝑇) ×
(mREx‘𝑇)) |
22 | 18, 21 | eleqtrdi 2848 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → 𝑦 ∈ ((mTC‘𝑇) × (mREx‘𝑇))) |
23 | | xp1st 7793 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ((mTC‘𝑇) × (mREx‘𝑇)) → (1st
‘𝑦) ∈
(mTC‘𝑇)) |
24 | 22, 23 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → (1st ‘𝑦) ∈ (mTC‘𝑇)) |
25 | 2, 20 | mrsubf 33192 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ ran (mRSubst‘𝑇) → 𝑔:(mREx‘𝑇)⟶(mREx‘𝑇)) |
26 | 25 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → 𝑔:(mREx‘𝑇)⟶(mREx‘𝑇)) |
27 | | xp2nd 7794 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ((mTC‘𝑇) × (mREx‘𝑇)) → (2nd
‘𝑦) ∈
(mREx‘𝑇)) |
28 | 22, 27 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → (2nd ‘𝑦) ∈ (mREx‘𝑇)) |
29 | 26, 28 | ffvelrnd 6905 |
. . . . . . . . . 10
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → (𝑔‘(2nd ‘𝑦)) ∈ (mREx‘𝑇)) |
30 | | opelxpi 5588 |
. . . . . . . . . 10
⊢
(((1st ‘𝑦) ∈ (mTC‘𝑇) ∧ (𝑔‘(2nd ‘𝑦)) ∈ (mREx‘𝑇)) → 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉 ∈
((mTC‘𝑇) ×
(mREx‘𝑇))) |
31 | 24, 29, 30 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉 ∈
((mTC‘𝑇) ×
(mREx‘𝑇))) |
32 | 31, 21 | eleqtrrdi 2849 |
. . . . . . . 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 6730 |
. . . . . . . . . 10
⊢
(1st ‘𝑦) ∈ V |
36 | | fvex 6730 |
. . . . . . . . . 10
⊢ (𝑔‘(2nd
‘𝑦)) ∈
V |
37 | 35, 36 | op1std 7771 |
. . . . . . . . 9
⊢ (𝑥 = 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉 →
(1st ‘𝑥) =
(1st ‘𝑦)) |
38 | 35, 36 | op2ndd 7772 |
. . . . . . . . . 10
⊢ (𝑥 = 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉 →
(2nd ‘𝑥) =
(𝑔‘(2nd
‘𝑦))) |
39 | 38 | fveq2d 6721 |
. . . . . . . . 9
⊢ (𝑥 = 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉 →
(𝑓‘(2nd
‘𝑥)) = (𝑓‘(𝑔‘(2nd ‘𝑦)))) |
40 | 37, 39 | opeq12d 4792 |
. . . . . . . 8
⊢ (𝑥 = 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉 →
〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉 = 〈(1st
‘𝑦), (𝑓‘(𝑔‘(2nd ‘𝑦)))〉) |
41 | 32, 33, 34, 40 | fmptco 6944 |
. . . . . . 7
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) → ((𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∘ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉)) = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), (𝑓‘(𝑔‘(2nd ‘𝑦)))〉)) |
42 | | fvco3 6810 |
. . . . . . . . . 10
⊢ ((𝑔:(mREx‘𝑇)⟶(mREx‘𝑇) ∧ (2nd ‘𝑦) ∈ (mREx‘𝑇)) → ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦)) = (𝑓‘(𝑔‘(2nd ‘𝑦)))) |
43 | 26, 28, 42 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦)) = (𝑓‘(𝑔‘(2nd ‘𝑦)))) |
44 | 43 | opeq2d 4791 |
. . . . . . . 8
⊢ (((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) ∧ 𝑦 ∈ (mEx‘𝑇)) → 〈(1st ‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉 = 〈(1st
‘𝑦), (𝑓‘(𝑔‘(2nd ‘𝑦)))〉) |
45 | 44 | mpteq2dva 5150 |
. . . . . . 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 33196 |
. . . . . . . 8
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) → (𝑓 ∘ 𝑔) ∈ ran (mRSubst‘𝑇)) |
48 | 7 | mptex 7039 |
. . . . . . . 8
⊢ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉) ∈
V |
49 | | eqid 2737 |
. . . . . . . . 9
⊢ (ℎ ∈ ran (mRSubst‘𝑇) ↦ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (ℎ‘(2nd ‘𝑦))〉)) = (ℎ ∈ ran (mRSubst‘𝑇) ↦ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (ℎ‘(2nd ‘𝑦))〉)) |
50 | | fveq1 6716 |
. . . . . . . . . . 11
⊢ (ℎ = (𝑓 ∘ 𝑔) → (ℎ‘(2nd ‘𝑦)) = ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))) |
51 | 50 | opeq2d 4791 |
. . . . . . . . . 10
⊢ (ℎ = (𝑓 ∘ 𝑔) → 〈(1st ‘𝑦), (ℎ‘(2nd ‘𝑦))〉 = 〈(1st
‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉) |
52 | 51 | mpteq2dv 5151 |
. . . . . . . . 9
⊢ (ℎ = (𝑓 ∘ 𝑔) → (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (ℎ‘(2nd ‘𝑦))〉) = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉)) |
53 | 49, 52 | elrnmpt1s 5826 |
. . . . . . . 8
⊢ (((𝑓 ∘ 𝑔) ∈ ran (mRSubst‘𝑇) ∧ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉) ∈ V) →
(𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉) ∈ ran (ℎ ∈ ran (mRSubst‘𝑇) ↦ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (ℎ‘(2nd ‘𝑦))〉))) |
54 | 47, 48, 53 | sylancl 589 |
. . . . . . 7
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) → (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉) ∈ ran (ℎ ∈ ran (mRSubst‘𝑇) ↦ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (ℎ‘(2nd ‘𝑦))〉))) |
55 | 1, 2, 3 | elmsubrn 33203 |
. . . . . . 7
⊢ ran 𝑆 = ran (ℎ ∈ ran (mRSubst‘𝑇) ↦ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (ℎ‘(2nd ‘𝑦))〉)) |
56 | 54, 55 | eleqtrrdi 2849 |
. . . . . 6
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) → (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), ((𝑓 ∘ 𝑔)‘(2nd ‘𝑦))〉) ∈ ran 𝑆) |
57 | 46, 56 | eqeltrd 2838 |
. . . . 5
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) → ((𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∘ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉)) ∈
ran 𝑆) |
58 | | coeq1 5726 |
. . . . . . 7
⊢ (𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) → (𝐹 ∘ 𝐺) = ((𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∘ 𝐺)) |
59 | | coeq2 5727 |
. . . . . . 7
⊢ (𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉) → ((𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑥), (𝑓‘(2nd
‘𝑥))〉) ∘
𝐺) = ((𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∘ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉))) |
60 | 58, 59 | sylan9eq 2798 |
. . . . . 6
⊢ ((𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∧ 𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) → (𝐹 ∘ 𝐺) = ((𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∘ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉))) |
61 | 60 | eleq1d 2822 |
. . . . 5
⊢ ((𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∧ 𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) → ((𝐹 ∘ 𝐺) ∈ ran 𝑆 ↔ ((𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∘ (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st
‘𝑦), (𝑔‘(2nd
‘𝑦))〉)) ∈
ran 𝑆)) |
62 | 57, 61 | syl5ibrcom 250 |
. . . 4
⊢ ((𝑓 ∈ ran (mRSubst‘𝑇) ∧ 𝑔 ∈ ran (mRSubst‘𝑇)) → ((𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∧ 𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) → (𝐹 ∘ 𝐺) ∈ ran 𝑆)) |
63 | 62 | rexlimivv 3211 |
. . 3
⊢
(∃𝑓 ∈ ran
(mRSubst‘𝑇)∃𝑔 ∈ ran (mRSubst‘𝑇)(𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∧ 𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) → (𝐹 ∘ 𝐺) ∈ ran 𝑆) |
64 | 17, 63 | sylbir 238 |
. 2
⊢
((∃𝑓 ∈
ran (mRSubst‘𝑇)𝐹 = (𝑥 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑥), (𝑓‘(2nd ‘𝑥))〉) ∧ ∃𝑔 ∈ ran (mRSubst‘𝑇)𝐺 = (𝑦 ∈ (mEx‘𝑇) ↦ 〈(1st ‘𝑦), (𝑔‘(2nd ‘𝑦))〉)) → (𝐹 ∘ 𝐺) ∈ ran 𝑆) |
65 | 10, 16, 64 | syl2anb 601 |
1
⊢ ((𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆) → (𝐹 ∘ 𝐺) ∈ ran 𝑆) |