Metamath Proof Explorer


Theorem stoweidlem9

Description: Lemma for stoweid : here the Stone Weierstrass theorem is proven for the trivial case, T is the empty set. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem9.1 φ T =
stoweidlem9.2 φ t T 1 A
Assertion stoweidlem9 φ g A t T g t F t < E

Proof

Step Hyp Ref Expression
1 stoweidlem9.1 φ T =
2 stoweidlem9.2 φ t T 1 A
3 mpteq1 T = t T 1 = t 1
4 mpt0 t 1 =
5 3 4 eqtrdi T = t T 1 =
6 1 5 syl φ t T 1 =
7 6 2 eqeltrrd φ A
8 rzal T = t T t F t < E
9 1 8 syl φ t T t F t < E
10 fveq1 g = g t = t
11 10 fvoveq1d g = g t F t = t F t
12 11 breq1d g = g t F t < E t F t < E
13 12 ralbidv g = t T g t F t < E t T t F t < E
14 13 rspcev A t T t F t < E g A t T g t F t < E
15 7 9 14 syl2anc φ g A t T g t F t < E