Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Mario Carneiro
Metamath formal systems
mstaval
Next ⟩
msrid
Metamath Proof Explorer
Ascii
Unicode
Theorem
mstaval
Description:
Value of the set of statements.
(Contributed by
Mario Carneiro
, 18-Jul-2016)
Ref
Expression
Hypotheses
mstaval.r
⊢
R
=
mStRed
⁡
T
mstaval.s
⊢
S
=
mStat
⁡
T
Assertion
mstaval
⊢
S
=
ran
⁡
R
Proof
Step
Hyp
Ref
Expression
1
mstaval.r
⊢
R
=
mStRed
⁡
T
2
mstaval.s
⊢
S
=
mStat
⁡
T
3
fveq2
⊢
t
=
T
→
mStRed
⁡
t
=
mStRed
⁡
T
4
3
1
eqtr4di
⊢
t
=
T
→
mStRed
⁡
t
=
R
5
4
rneqd
⊢
t
=
T
→
ran
⁡
mStRed
⁡
t
=
ran
⁡
R
6
df-msta
⊢
mStat
=
t
∈
V
⟼
ran
⁡
mStRed
⁡
t
7
1
fvexi
⊢
R
∈
V
8
7
rnex
⊢
ran
⁡
R
∈
V
9
5
6
8
fvmpt
⊢
T
∈
V
→
mStat
⁡
T
=
ran
⁡
R
10
rn0
⊢
ran
⁡
∅
=
∅
11
10
eqcomi
⊢
∅
=
ran
⁡
∅
12
fvprc
⊢
¬
T
∈
V
→
mStat
⁡
T
=
∅
13
fvprc
⊢
¬
T
∈
V
→
mStRed
⁡
T
=
∅
14
1
13
syl5eq
⊢
¬
T
∈
V
→
R
=
∅
15
14
rneqd
⊢
¬
T
∈
V
→
ran
⁡
R
=
ran
⁡
∅
16
11
12
15
3eqtr4a
⊢
¬
T
∈
V
→
mStat
⁡
T
=
ran
⁡
R
17
9
16
pm2.61i
⊢
mStat
⁡
T
=
ran
⁡
R
18
2
17
eqtri
⊢
S
=
ran
⁡
R