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 syl6eq ⊢ 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