Metamath Proof Explorer

Theorem msubff

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

Ref Expression
Hypotheses msubff.v ⊢ V = mVR ⁡ T
msubff.r ⊢ R = mREx ⁡ T
msubff.s ⊢ S = mSubst ⁡ T
msubff.e ⊢ E = mEx ⁡ T
Assertion msubff ⊢ T ∈ W → S : R ↑ 𝑝𝑚 V ⟶ E E

Proof

Step Hyp Ref Expression
1 msubff.v ⊢ V = mVR ⁡ T
2 msubff.r ⊢ R = mREx ⁡ T
3 msubff.s ⊢ S = mSubst ⁡ T
4 msubff.e ⊢ E = mEx ⁡ T
5 xp1st ⊢ e ∈ mTC ⁡ T × R → 1 st ⁡ e ∈ mTC ⁡ T
6 eqid ⊢ mTC ⁡ T = mTC ⁡ T
7 6 4 2 mexval ⊢ E = mTC ⁡ T × R
8 5 7 eleq2s ⊢ e ∈ E → 1 st ⁡ e ∈ mTC ⁡ T
9 8 adantl ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V ∧ e ∈ E → 1 st ⁡ e ∈ mTC ⁡ T
10 eqid ⊢ mRSubst ⁡ T = mRSubst ⁡ T
11 1 2 10 mrsubff ⊢ T ∈ W → mRSubst ⁡ T : R ↑ 𝑝𝑚 V ⟶ R R
12 11 ffvelcdmda ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V → mRSubst ⁡ T ⁡ f ∈ R R
13 elmapi ⊢ mRSubst ⁡ T ⁡ f ∈ R R → mRSubst ⁡ T ⁡ f : R ⟶ R
14 12 13 syl ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V → mRSubst ⁡ T ⁡ f : R ⟶ R
15 xp2nd ⊢ e ∈ mTC ⁡ T × R → 2 nd ⁡ e ∈ R
16 15 7 eleq2s ⊢ e ∈ E → 2 nd ⁡ e ∈ R
17 ffvelcdm ⊢ mRSubst ⁡ T ⁡ f : R ⟶ R ∧ 2 nd ⁡ e ∈ R → mRSubst ⁡ T ⁡ f ⁡ 2 nd ⁡ e ∈ R
18 14 16 17 syl2an ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V ∧ e ∈ E → mRSubst ⁡ T ⁡ f ⁡ 2 nd ⁡ e ∈ R
19 opelxp ⊢ 1 st ⁡ e mRSubst ⁡ T ⁡ f ⁡ 2 nd ⁡ e ∈ mTC ⁡ T × R ↔ 1 st ⁡ e ∈ mTC ⁡ T ∧ mRSubst ⁡ T ⁡ f ⁡ 2 nd ⁡ e ∈ R
20 9 18 19 sylanbrc ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V ∧ e ∈ E → 1 st ⁡ e mRSubst ⁡ T ⁡ f ⁡ 2 nd ⁡ e ∈ mTC ⁡ T × R
21 20 7 eleqtrrdi ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V ∧ e ∈ E → 1 st ⁡ e mRSubst ⁡ T ⁡ f ⁡ 2 nd ⁡ e ∈ E
22 21 fmpttd ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V → e ∈ E ⟼ 1 st ⁡ e mRSubst ⁡ T ⁡ f ⁡ 2 nd ⁡ e : E ⟶ E
23 4 fvexi ⊢ E ∈ V
24 23 23 elmap ⊢ e ∈ E ⟼ 1 st ⁡ e mRSubst ⁡ T ⁡ f ⁡ 2 nd ⁡ e ∈ E E ↔ e ∈ E ⟼ 1 st ⁡ e mRSubst ⁡ T ⁡ f ⁡ 2 nd ⁡ e : E ⟶ E
25 22 24 sylibr ⊢ T ∈ W ∧ f ∈ R ↑ 𝑝𝑚 V → e ∈ E ⟼ 1 st ⁡ e mRSubst ⁡ T ⁡ f ⁡ 2 nd ⁡ e ∈ E E
26 25 fmpttd ⊢ T ∈ W → f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ E ⟼ 1 st ⁡ e mRSubst ⁡ T ⁡ f ⁡ 2 nd ⁡ e : R ↑ 𝑝𝑚 V ⟶ E E
27 1 2 3 4 10 msubffval ⊢ T ∈ W → S = f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ E ⟼ 1 st ⁡ e mRSubst ⁡ T ⁡ f ⁡ 2 nd ⁡ e
28 27 feq1d ⊢ T ∈ W → S : R ↑ 𝑝𝑚 V ⟶ E E ↔ f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ E ⟼ 1 st ⁡ e mRSubst ⁡ T ⁡ f ⁡ 2 nd ⁡ e : R ↑ 𝑝𝑚 V ⟶ E E
29 26 28 mpbird ⊢ T ∈ W → S : R ↑ 𝑝𝑚 V ⟶ E E