msubff

Description: A substitution is a function from E to E . (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	msubff.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	msubff.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
	msubff.s	⊢ 𝑆 = ( mSubst ‘ 𝑇 )
	msubff.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
Assertion	msubff	⊢ ( 𝑇 ∈ 𝑊 → 𝑆 : ( 𝑅 ↑_pm 𝑉 ) ⟶ ( 𝐸 ↑_m 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		msubff.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
2		msubff.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
3		msubff.s	⊢ 𝑆 = ( mSubst ‘ 𝑇 )
4		msubff.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
5		xp1st	⊢ ( 𝑒 ∈ ( ( mTC ‘ 𝑇 ) × 𝑅 ) → ( 1^st ‘ 𝑒 ) ∈ ( mTC ‘ 𝑇 ) )
6		eqid	⊢ ( mTC ‘ 𝑇 ) = ( mTC ‘ 𝑇 )
7	6 4 2	mexval	⊢ 𝐸 = ( ( mTC ‘ 𝑇 ) × 𝑅 )
8	5 7	eleq2s	⊢ ( 𝑒 ∈ 𝐸 → ( 1^st ‘ 𝑒 ) ∈ ( mTC ‘ 𝑇 ) )
9	8	adantl	⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ 𝑓 ∈ ( 𝑅 ↑_pm 𝑉 ) ) ∧ 𝑒 ∈ 𝐸 ) → ( 1^st ‘ 𝑒 ) ∈ ( mTC ‘ 𝑇 ) )
10		eqid	⊢ ( mRSubst ‘ 𝑇 ) = ( mRSubst ‘ 𝑇 )
11	1 2 10	mrsubff	⊢ ( 𝑇 ∈ 𝑊 → ( mRSubst ‘ 𝑇 ) : ( 𝑅 ↑_pm 𝑉 ) ⟶ ( 𝑅 ↑_m 𝑅 ) )
12	11	ffvelrnda	⊢ ( ( 𝑇 ∈ 𝑊 ∧ 𝑓 ∈ ( 𝑅 ↑_pm 𝑉 ) ) → ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ∈ ( 𝑅 ↑_m 𝑅 ) )
13		elmapi	⊢ ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ∈ ( 𝑅 ↑_m 𝑅 ) → ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) : 𝑅 ⟶ 𝑅 )
14	12 13	syl	⊢ ( ( 𝑇 ∈ 𝑊 ∧ 𝑓 ∈ ( 𝑅 ↑_pm 𝑉 ) ) → ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) : 𝑅 ⟶ 𝑅 )
15		xp2nd	⊢ ( 𝑒 ∈ ( ( mTC ‘ 𝑇 ) × 𝑅 ) → ( 2^nd ‘ 𝑒 ) ∈ 𝑅 )
16	15 7	eleq2s	⊢ ( 𝑒 ∈ 𝐸 → ( 2^nd ‘ 𝑒 ) ∈ 𝑅 )
17		ffvelrn	⊢ ( ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) : 𝑅 ⟶ 𝑅 ∧ ( 2^nd ‘ 𝑒 ) ∈ 𝑅 ) → ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ∈ 𝑅 )
18	14 16 17	syl2an	⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ 𝑓 ∈ ( 𝑅 ↑_pm 𝑉 ) ) ∧ 𝑒 ∈ 𝐸 ) → ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ∈ 𝑅 )
19		opelxp	⊢ ( ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ∈ ( ( mTC ‘ 𝑇 ) × 𝑅 ) ↔ ( ( 1^st ‘ 𝑒 ) ∈ ( mTC ‘ 𝑇 ) ∧ ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ∈ 𝑅 ) )
20	9 18 19	sylanbrc	⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ 𝑓 ∈ ( 𝑅 ↑_pm 𝑉 ) ) ∧ 𝑒 ∈ 𝐸 ) → ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ∈ ( ( mTC ‘ 𝑇 ) × 𝑅 ) )
21	20 7	eleqtrrdi	⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ 𝑓 ∈ ( 𝑅 ↑_pm 𝑉 ) ) ∧ 𝑒 ∈ 𝐸 ) → ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ∈ 𝐸 )
22	21	fmpttd	⊢ ( ( 𝑇 ∈ 𝑊 ∧ 𝑓 ∈ ( 𝑅 ↑_pm 𝑉 ) ) → ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) : 𝐸 ⟶ 𝐸 )
23	4	fvexi	⊢ 𝐸 ∈ V
24	23 23	elmap	⊢ ( ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ∈ ( 𝐸 ↑_m 𝐸 ) ↔ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) : 𝐸 ⟶ 𝐸 )
25	22 24	sylibr	⊢ ( ( 𝑇 ∈ 𝑊 ∧ 𝑓 ∈ ( 𝑅 ↑_pm 𝑉 ) ) → ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ∈ ( 𝐸 ↑_m 𝐸 ) )
26	25	fmpttd	⊢ ( 𝑇 ∈ 𝑊 → ( 𝑓 ∈ ( 𝑅 ↑_pm 𝑉 ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) : ( 𝑅 ↑_pm 𝑉 ) ⟶ ( 𝐸 ↑_m 𝐸 ) )
27	1 2 3 4 10	msubffval	⊢ ( 𝑇 ∈ 𝑊 → 𝑆 = ( 𝑓 ∈ ( 𝑅 ↑_pm 𝑉 ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) )
28	27	feq1d	⊢ ( 𝑇 ∈ 𝑊 → ( 𝑆 : ( 𝑅 ↑_pm 𝑉 ) ⟶ ( 𝐸 ↑_m 𝐸 ) ↔ ( 𝑓 ∈ ( 𝑅 ↑_pm 𝑉 ) ↦ ( 𝑒 ∈ 𝐸 ↦ ⟨ ( 1^st ‘ 𝑒 ) , ( ( ( mRSubst ‘ 𝑇 ) ‘ 𝑓 ) ‘ ( 2^nd ‘ 𝑒 ) ) ⟩ ) ) : ( 𝑅 ↑_pm 𝑉 ) ⟶ ( 𝐸 ↑_m 𝐸 ) ) )
29	26 28	mpbird	⊢ ( 𝑇 ∈ 𝑊 → 𝑆 : ( 𝑅 ↑_pm 𝑉 ) ⟶ ( 𝐸 ↑_m 𝐸 ) )

Metamath Proof Explorer

Theorem msubff

Proof