Step |
Hyp |
Ref |
Expression |
1 |
|
msubco.s |
⊢ 𝑆 = ( mSubst ‘ 𝑇 ) |
2 |
|
eqid |
⊢ ( mEx ‘ 𝑇 ) = ( mEx ‘ 𝑇 ) |
3 |
|
eqid |
⊢ ( mRSubst ‘ 𝑇 ) = ( mRSubst ‘ 𝑇 ) |
4 |
2 3 1
|
elmsubrn |
⊢ ran 𝑆 = ran ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ) |
5 |
4
|
eleq2i |
⊢ ( 𝐹 ∈ ran 𝑆 ↔ 𝐹 ∈ ran ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ) ) |
6 |
|
eqid |
⊢ ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ) = ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ) |
7 |
|
fvex |
⊢ ( mEx ‘ 𝑇 ) ∈ V |
8 |
7
|
mptex |
⊢ ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ∈ V |
9 |
6 8
|
elrnmpti |
⊢ ( 𝐹 ∈ ran ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ) ↔ ∃ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) 𝐹 = ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ) |
10 |
5 9
|
bitri |
⊢ ( 𝐹 ∈ ran 𝑆 ↔ ∃ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) 𝐹 = ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ) |
11 |
2 3 1
|
elmsubrn |
⊢ ran 𝑆 = ran ( 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) |
12 |
11
|
eleq2i |
⊢ ( 𝐺 ∈ ran 𝑆 ↔ 𝐺 ∈ ran ( 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) ) |
13 |
|
eqid |
⊢ ( 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) = ( 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) |
14 |
7
|
mptex |
⊢ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ∈ V |
15 |
13 14
|
elrnmpti |
⊢ ( 𝐺 ∈ ran ( 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) ↔ ∃ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) 𝐺 = ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) |
16 |
12 15
|
bitri |
⊢ ( 𝐺 ∈ ran 𝑆 ↔ ∃ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) 𝐺 = ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) |
17 |
|
reeanv |
⊢ ( ∃ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∃ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ( 𝐹 = ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ∧ 𝐺 = ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) ↔ ( ∃ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) 𝐹 = ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ∧ ∃ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) 𝐺 = ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) ) |
18 |
|
simpr |
⊢ ( ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) ∧ 𝑦 ∈ ( mEx ‘ 𝑇 ) ) → 𝑦 ∈ ( mEx ‘ 𝑇 ) ) |
19 |
|
eqid |
⊢ ( mTC ‘ 𝑇 ) = ( mTC ‘ 𝑇 ) |
20 |
|
eqid |
⊢ ( mREx ‘ 𝑇 ) = ( mREx ‘ 𝑇 ) |
21 |
19 2 20
|
mexval |
⊢ ( mEx ‘ 𝑇 ) = ( ( mTC ‘ 𝑇 ) × ( mREx ‘ 𝑇 ) ) |
22 |
18 21
|
eleqtrdi |
⊢ ( ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) ∧ 𝑦 ∈ ( mEx ‘ 𝑇 ) ) → 𝑦 ∈ ( ( mTC ‘ 𝑇 ) × ( mREx ‘ 𝑇 ) ) ) |
23 |
|
xp1st |
⊢ ( 𝑦 ∈ ( ( mTC ‘ 𝑇 ) × ( mREx ‘ 𝑇 ) ) → ( 1st ‘ 𝑦 ) ∈ ( mTC ‘ 𝑇 ) ) |
24 |
22 23
|
syl |
⊢ ( ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) ∧ 𝑦 ∈ ( mEx ‘ 𝑇 ) ) → ( 1st ‘ 𝑦 ) ∈ ( mTC ‘ 𝑇 ) ) |
25 |
3 20
|
mrsubf |
⊢ ( 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) → 𝑔 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) ) |
26 |
25
|
ad2antlr |
⊢ ( ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) ∧ 𝑦 ∈ ( mEx ‘ 𝑇 ) ) → 𝑔 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) ) |
27 |
|
xp2nd |
⊢ ( 𝑦 ∈ ( ( mTC ‘ 𝑇 ) × ( mREx ‘ 𝑇 ) ) → ( 2nd ‘ 𝑦 ) ∈ ( mREx ‘ 𝑇 ) ) |
28 |
22 27
|
syl |
⊢ ( ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) ∧ 𝑦 ∈ ( mEx ‘ 𝑇 ) ) → ( 2nd ‘ 𝑦 ) ∈ ( mREx ‘ 𝑇 ) ) |
29 |
26 28
|
ffvelrnd |
⊢ ( ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) ∧ 𝑦 ∈ ( mEx ‘ 𝑇 ) ) → ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) ∈ ( mREx ‘ 𝑇 ) ) |
30 |
|
opelxpi |
⊢ ( ( ( 1st ‘ 𝑦 ) ∈ ( mTC ‘ 𝑇 ) ∧ ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) ∈ ( mREx ‘ 𝑇 ) ) → 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ∈ ( ( mTC ‘ 𝑇 ) × ( mREx ‘ 𝑇 ) ) ) |
31 |
24 29 30
|
syl2anc |
⊢ ( ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) ∧ 𝑦 ∈ ( mEx ‘ 𝑇 ) ) → 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ∈ ( ( mTC ‘ 𝑇 ) × ( mREx ‘ 𝑇 ) ) ) |
32 |
31 21
|
eleqtrrdi |
⊢ ( ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) ∧ 𝑦 ∈ ( mEx ‘ 𝑇 ) ) → 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ∈ ( mEx ‘ 𝑇 ) ) |
33 |
|
eqidd |
⊢ ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) → ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) = ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) |
34 |
|
eqidd |
⊢ ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) → ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) = ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ) |
35 |
|
fvex |
⊢ ( 1st ‘ 𝑦 ) ∈ V |
36 |
|
fvex |
⊢ ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) ∈ V |
37 |
35 36
|
op1std |
⊢ ( 𝑥 = 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 → ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) |
38 |
35 36
|
op2ndd |
⊢ ( 𝑥 = 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 → ( 2nd ‘ 𝑥 ) = ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) ) |
39 |
38
|
fveq2d |
⊢ ( 𝑥 = 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 → ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) = ( 𝑓 ‘ ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) ) ) |
40 |
37 39
|
opeq12d |
⊢ ( 𝑥 = 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 → 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 = 〈 ( 1st ‘ 𝑦 ) , ( 𝑓 ‘ ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) ) 〉 ) |
41 |
32 33 34 40
|
fmptco |
⊢ ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) → ( ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ∘ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) = ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑓 ‘ ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) ) 〉 ) ) |
42 |
|
fvco3 |
⊢ ( ( 𝑔 : ( mREx ‘ 𝑇 ) ⟶ ( mREx ‘ 𝑇 ) ∧ ( 2nd ‘ 𝑦 ) ∈ ( mREx ‘ 𝑇 ) ) → ( ( 𝑓 ∘ 𝑔 ) ‘ ( 2nd ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) ) ) |
43 |
26 28 42
|
syl2anc |
⊢ ( ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) ∧ 𝑦 ∈ ( mEx ‘ 𝑇 ) ) → ( ( 𝑓 ∘ 𝑔 ) ‘ ( 2nd ‘ 𝑦 ) ) = ( 𝑓 ‘ ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) ) ) |
44 |
43
|
opeq2d |
⊢ ( ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) ∧ 𝑦 ∈ ( mEx ‘ 𝑇 ) ) → 〈 ( 1st ‘ 𝑦 ) , ( ( 𝑓 ∘ 𝑔 ) ‘ ( 2nd ‘ 𝑦 ) ) 〉 = 〈 ( 1st ‘ 𝑦 ) , ( 𝑓 ‘ ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) ) 〉 ) |
45 |
44
|
mpteq2dva |
⊢ ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) → ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( ( 𝑓 ∘ 𝑔 ) ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) = ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑓 ‘ ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) ) 〉 ) ) |
46 |
41 45
|
eqtr4d |
⊢ ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) → ( ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ∘ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) = ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( ( 𝑓 ∘ 𝑔 ) ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) |
47 |
3
|
mrsubco |
⊢ ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) → ( 𝑓 ∘ 𝑔 ) ∈ ran ( mRSubst ‘ 𝑇 ) ) |
48 |
7
|
mptex |
⊢ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( ( 𝑓 ∘ 𝑔 ) ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ∈ V |
49 |
|
eqid |
⊢ ( ℎ ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( ℎ ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) = ( ℎ ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( ℎ ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) |
50 |
|
fveq1 |
⊢ ( ℎ = ( 𝑓 ∘ 𝑔 ) → ( ℎ ‘ ( 2nd ‘ 𝑦 ) ) = ( ( 𝑓 ∘ 𝑔 ) ‘ ( 2nd ‘ 𝑦 ) ) ) |
51 |
50
|
opeq2d |
⊢ ( ℎ = ( 𝑓 ∘ 𝑔 ) → 〈 ( 1st ‘ 𝑦 ) , ( ℎ ‘ ( 2nd ‘ 𝑦 ) ) 〉 = 〈 ( 1st ‘ 𝑦 ) , ( ( 𝑓 ∘ 𝑔 ) ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) |
52 |
51
|
mpteq2dv |
⊢ ( ℎ = ( 𝑓 ∘ 𝑔 ) → ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( ℎ ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) = ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( ( 𝑓 ∘ 𝑔 ) ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) |
53 |
49 52
|
elrnmpt1s |
⊢ ( ( ( 𝑓 ∘ 𝑔 ) ∈ ran ( mRSubst ‘ 𝑇 ) ∧ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( ( 𝑓 ∘ 𝑔 ) ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ∈ V ) → ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( ( 𝑓 ∘ 𝑔 ) ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ∈ ran ( ℎ ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( ℎ ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) ) |
54 |
47 48 53
|
sylancl |
⊢ ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) → ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( ( 𝑓 ∘ 𝑔 ) ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ∈ ran ( ℎ ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( ℎ ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) ) |
55 |
2 3 1
|
elmsubrn |
⊢ ran 𝑆 = ran ( ℎ ∈ ran ( mRSubst ‘ 𝑇 ) ↦ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( ℎ ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) |
56 |
54 55
|
eleqtrrdi |
⊢ ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) → ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( ( 𝑓 ∘ 𝑔 ) ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ∈ ran 𝑆 ) |
57 |
46 56
|
eqeltrd |
⊢ ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) → ( ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ∘ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) ∈ ran 𝑆 ) |
58 |
|
coeq1 |
⊢ ( 𝐹 = ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) → ( 𝐹 ∘ 𝐺 ) = ( ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ∘ 𝐺 ) ) |
59 |
|
coeq2 |
⊢ ( 𝐺 = ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) → ( ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ∘ 𝐺 ) = ( ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ∘ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) ) |
60 |
58 59
|
sylan9eq |
⊢ ( ( 𝐹 = ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ∧ 𝐺 = ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) → ( 𝐹 ∘ 𝐺 ) = ( ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ∘ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) ) |
61 |
60
|
eleq1d |
⊢ ( ( 𝐹 = ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ∧ 𝐺 = ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) → ( ( 𝐹 ∘ 𝐺 ) ∈ ran 𝑆 ↔ ( ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ∘ ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) ∈ ran 𝑆 ) ) |
62 |
57 61
|
syl5ibrcom |
⊢ ( ( 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∧ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ) → ( ( 𝐹 = ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ∧ 𝐺 = ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ran 𝑆 ) ) |
63 |
62
|
rexlimivv |
⊢ ( ∃ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) ∃ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) ( 𝐹 = ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ∧ 𝐺 = ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ran 𝑆 ) |
64 |
17 63
|
sylbir |
⊢ ( ( ∃ 𝑓 ∈ ran ( mRSubst ‘ 𝑇 ) 𝐹 = ( 𝑥 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑥 ) , ( 𝑓 ‘ ( 2nd ‘ 𝑥 ) ) 〉 ) ∧ ∃ 𝑔 ∈ ran ( mRSubst ‘ 𝑇 ) 𝐺 = ( 𝑦 ∈ ( mEx ‘ 𝑇 ) ↦ 〈 ( 1st ‘ 𝑦 ) , ( 𝑔 ‘ ( 2nd ‘ 𝑦 ) ) 〉 ) ) → ( 𝐹 ∘ 𝐺 ) ∈ ran 𝑆 ) |
65 |
10 16 64
|
syl2anb |
⊢ ( ( 𝐹 ∈ ran 𝑆 ∧ 𝐺 ∈ ran 𝑆 ) → ( 𝐹 ∘ 𝐺 ) ∈ ran 𝑆 ) |