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⟼1st⁡eO⁡f⁡2nd⁡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⁡2nd⁡e=O⁡f⁡2nd⁡e
18 17 opeq2d ⊢t=T→1st⁡emRSubst⁡t⁡f⁡2nd⁡e=1st⁡eO⁡f⁡2nd⁡e
19 13 18 mpteq12dv ⊢t=T→e∈mEx⁡t⟼1st⁡emRSubst⁡t⁡f⁡2nd⁡e=e∈E⟼1st⁡eO⁡f⁡2nd⁡e
20 11 19 mpteq12dv ⊢t=T→f∈mREx⁡t↑𝑝𝑚mVR⁡t⟼e∈mEx⁡t⟼1st⁡emRSubst⁡t⁡f⁡2nd⁡e=f∈R↑𝑝𝑚V⟼e∈E⟼1st⁡eO⁡f⁡2nd⁡e
21 df-msub ⊢mSubst=t∈V⟼f∈mREx⁡t↑𝑝𝑚mVR⁡t⟼e∈mEx⁡t⟼1st⁡emRSubst⁡t⁡f⁡2nd⁡e
22 ovex ⊢R↑𝑝𝑚V∈V
23 22 mptex ⊢f∈R↑𝑝𝑚V⟼e∈E⟼1st⁡eO⁡f⁡2nd⁡e∈V
24 20 21 23 fvmpt ⊢T∈V→mSubst⁡T=f∈R↑𝑝𝑚V⟼e∈E⟼1st⁡eO⁡f⁡2nd⁡e
25 3 24 eqtrid ⊢T∈V→S=f∈R↑𝑝𝑚V⟼e∈E⟼1st⁡eO⁡f⁡2nd⁡e
26 6 25 syl ⊢T∈W→S=f∈R↑𝑝𝑚V⟼e∈E⟼1st⁡eO⁡f⁡2nd⁡e