Metamath Proof Explorer


Theorem msubco

Description: The composition of two substitutions is a substitution. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypothesis msubco.s 𝑆 = ( mSubst ‘ 𝑇 )
Assertion msubco ( ( 𝐹 ∈ ran 𝑆𝐺 ∈ ran 𝑆 ) → ( 𝐹𝐺 ) ∈ ran 𝑆 )

Proof

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 𝑆 )