Metamath Proof Explorer

Theorem msubffval

Description: A substitution applied to an expression. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses msubffval.v ⊢ V = mVR ⁡ T
msubffval.r ⊢ R = mREx ⁡ T
msubffval.s ⊢ S = mSubst ⁡ T
msubffval.e ⊢ E = mEx ⁡ T
msubffval.o ⊢ O = mRSubst ⁡ T
Assertion msubffval ⊢ T ∈ W → S = f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ E ⟼ 1 st ⁡ e O ⁡ f ⁡ 2 nd ⁡ e

Proof

Step Hyp Ref Expression
1 msubffval.v ⊢ V = mVR ⁡ T
2 msubffval.r ⊢ R = mREx ⁡ T
3 msubffval.s ⊢ S = mSubst ⁡ T
4 msubffval.e ⊢ E = mEx ⁡ T
5 msubffval.o ⊢ O = mRSubst ⁡ T
6 elex ⊢ T ∈ W → T ∈ V
7 fveq2 ⊢ t = T → mREx ⁡ t = mREx ⁡ T
8 7 2 eqtr4di ⊢ t = T → mREx ⁡ t = R
9 fveq2 ⊢ t = T → mVR ⁡ t = mVR ⁡ T
10 9 1 eqtr4di ⊢ t = T → mVR ⁡ t = V
11 8 10 oveq12d ⊢ t = T → mREx ⁡ t ↑ 𝑝𝑚 mVR ⁡ t = R ↑ 𝑝𝑚 V
12 fveq2 ⊢ t = T → mEx ⁡ t = mEx ⁡ T
13 12 4 eqtr4di ⊢ t = T → mEx ⁡ t = E
14 fveq2 ⊢ t = T → mRSubst ⁡ t = mRSubst ⁡ T
15 14 5 eqtr4di ⊢ t = T → mRSubst ⁡ t = O
16 15 fveq1d ⊢ t = T → mRSubst ⁡ t ⁡ f = O ⁡ f
17 16 fveq1d ⊢ t = T → mRSubst ⁡ t ⁡ f ⁡ 2 nd ⁡ e = O ⁡ f ⁡ 2 nd ⁡ e
18 17 opeq2d ⊢ t = T → 1 st ⁡ e mRSubst ⁡ t ⁡ f ⁡ 2 nd ⁡ e = 1 st ⁡ e O ⁡ f ⁡ 2 nd ⁡ e
19 13 18 mpteq12dv ⊢ t = T → e ∈ mEx ⁡ t ⟼ 1 st ⁡ e mRSubst ⁡ t ⁡ f ⁡ 2 nd ⁡ e = e ∈ E ⟼ 1 st ⁡ e O ⁡ f ⁡ 2 nd ⁡ e
20 11 19 mpteq12dv ⊢ t = T → f ∈ mREx ⁡ t ↑ 𝑝𝑚 mVR ⁡ t ⟼ e ∈ mEx ⁡ t ⟼ 1 st ⁡ e mRSubst ⁡ t ⁡ f ⁡ 2 nd ⁡ e = f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ E ⟼ 1 st ⁡ e O ⁡ f ⁡ 2 nd ⁡ e
21 df-msub ⊢ mSubst = t ∈ V ⟼ f ∈ mREx ⁡ t ↑ 𝑝𝑚 mVR ⁡ t ⟼ e ∈ mEx ⁡ t ⟼ 1 st ⁡ e mRSubst ⁡ t ⁡ f ⁡ 2 nd ⁡ e
22 ovex ⊢ R ↑ 𝑝𝑚 V ∈ V
23 22 mptex ⊢ f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ E ⟼ 1 st ⁡ e O ⁡ f ⁡ 2 nd ⁡ e ∈ V
24 20 21 23 fvmpt ⊢ T ∈ V → mSubst ⁡ T = f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ E ⟼ 1 st ⁡ e O ⁡ f ⁡ 2 nd ⁡ e
25 3 24 eqtrid ⊢ T ∈ V → S = f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ E ⟼ 1 st ⁡ e O ⁡ f ⁡ 2 nd ⁡ e
26 6 25 syl ⊢ T ∈ W → S = f ∈ R ↑ 𝑝𝑚 V ⟼ e ∈ E ⟼ 1 st ⁡ e O ⁡ f ⁡ 2 nd ⁡ e