Metamath Proof Explorer


Theorem msubfval

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 msubfval F : A R A V S F = 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 1 2 3 4 5 msubffval T V S = f R 𝑝𝑚 V e E 1 st e O f 2 nd e
7 6 adantr T V F : A R A V S = f R 𝑝𝑚 V e E 1 st e O f 2 nd e
8 simplr T V F : A R A V f = F e E f = F
9 8 fveq2d T V F : A R A V f = F e E O f = O F
10 9 fveq1d T V F : A R A V f = F e E O f 2 nd e = O F 2 nd e
11 10 opeq2d T V F : A R A V f = F e E 1 st e O f 2 nd e = 1 st e O F 2 nd e
12 11 mpteq2dva T V F : A R A V f = F e E 1 st e O f 2 nd e = e E 1 st e O F 2 nd e
13 2 fvexi R V
14 1 fvexi V V
15 13 14 pm3.2i R V V V
16 15 a1i T V R V V V
17 elpm2r R V V V F : A R A V F R 𝑝𝑚 V
18 16 17 sylan T V F : A R A V F R 𝑝𝑚 V
19 4 fvexi E V
20 19 mptex e E 1 st e O F 2 nd e V
21 20 a1i T V F : A R A V e E 1 st e O F 2 nd e V
22 7 12 18 21 fvmptd T V F : A R A V S F = e E 1 st e O F 2 nd e
23 22 ex T V F : A R A V S F = e E 1 st e O F 2 nd e
24 0fv F =
25 mpt0 e 1 st e O F 2 nd e =
26 24 25 eqtr4i F = e 1 st e O F 2 nd e
27 fvprc ¬ T V mSubst T =
28 3 27 syl5eq ¬ T V S =
29 28 fveq1d ¬ T V S F = F
30 fvprc ¬ T V mEx T =
31 4 30 syl5eq ¬ T V E =
32 31 mpteq1d ¬ T V e E 1 st e O F 2 nd e = e 1 st e O F 2 nd e
33 26 29 32 3eqtr4a ¬ T V S F = e E 1 st e O F 2 nd e
34 33 a1d ¬ T V F : A R A V S F = e E 1 st e O F 2 nd e
35 23 34 pm2.61i F : A R A V S F = e E 1 st e O F 2 nd e