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

Metamath Proof Explorer

Theorem msubco

Proof