Metamath Proof Explorer

Theorem stoweidlem18

Description: This theorem proves Lemma 2 in BrosowskiDeutsh p. 92 when A is empty, the trivial case. Here D is used to denote the set A of Lemma 2, because the variable A is used for the subalgebra. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem18.1 ⊢ Ⅎ _ t D
stoweidlem18.2 ⊢ Ⅎ t φ
stoweidlem18.3 ⊢ F = t ∈ T ⟼ 1
stoweidlem18.4 ⊢ T = ⋃ J
stoweidlem18.5 ⊢ φ ∧ a ∈ ℝ → t ∈ T ⟼ a ∈ A
stoweidlem18.6 ⊢ φ → B ∈ Clsd ⁡ J
stoweidlem18.7 ⊢ φ → E ∈ ℝ +
stoweidlem18.8 ⊢ φ → D = ∅
Assertion stoweidlem18 ⊢ φ → ∃ x ∈ A ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ∧ ∀ t ∈ D x ⁡ t < E ∧ ∀ t ∈ B 1 − E < x ⁡ t

Proof

Step Hyp Ref Expression
1 stoweidlem18.1 ⊢ Ⅎ _ t D
2 stoweidlem18.2 ⊢ Ⅎ t φ
3 stoweidlem18.3 ⊢ F = t ∈ T ⟼ 1
4 stoweidlem18.4 ⊢ T = ⋃ J
5 stoweidlem18.5 ⊢ φ ∧ a ∈ ℝ → t ∈ T ⟼ a ∈ A
6 stoweidlem18.6 ⊢ φ → B ∈ Clsd ⁡ J
7 stoweidlem18.7 ⊢ φ → E ∈ ℝ +
8 stoweidlem18.8 ⊢ φ → D = ∅
9 1re ⊢ 1 ∈ ℝ
10 5 stoweidlem4 ⊢ φ ∧ 1 ∈ ℝ → t ∈ T ⟼ 1 ∈ A
11 9 10 mpan2 ⊢ φ → t ∈ T ⟼ 1 ∈ A
12 3 11 eqeltrid ⊢ φ → F ∈ A
13 0le1 ⊢ 0 ≤ 1
14 simpr ⊢ φ ∧ t ∈ T → t ∈ T
15 3 fvmpt2 ⊢ t ∈ T ∧ 1 ∈ ℝ → F ⁡ t = 1
16 14 9 15 sylancl ⊢ φ ∧ t ∈ T → F ⁡ t = 1
17 13 16 breqtrrid ⊢ φ ∧ t ∈ T → 0 ≤ F ⁡ t
18 1le1 ⊢ 1 ≤ 1
19 16 18 eqbrtrdi ⊢ φ ∧ t ∈ T → F ⁡ t ≤ 1
20 17 19 jca ⊢ φ ∧ t ∈ T → 0 ≤ F ⁡ t ∧ F ⁡ t ≤ 1
21 20 ex ⊢ φ → t ∈ T → 0 ≤ F ⁡ t ∧ F ⁡ t ≤ 1
22 2 21 ralrimi ⊢ φ → ∀ t ∈ T 0 ≤ F ⁡ t ∧ F ⁡ t ≤ 1
23 nfcv ⊢ Ⅎ _ t ∅
24 1 23 nfeq ⊢ Ⅎ t D = ∅
25 24 rzalf ⊢ D = ∅ → ∀ t ∈ D F ⁡ t < E
26 8 25 syl ⊢ φ → ∀ t ∈ D F ⁡ t < E
27 1red ⊢ φ → 1 ∈ ℝ
28 27 7 ltsubrpd ⊢ φ → 1 − E < 1
29 28 adantr ⊢ φ ∧ t ∈ B → 1 − E < 1
30 4 cldss ⊢ B ∈ Clsd ⁡ J → B ⊆ T
31 6 30 syl ⊢ φ → B ⊆ T
32 31 sselda ⊢ φ ∧ t ∈ B → t ∈ T
33 32 9 15 sylancl ⊢ φ ∧ t ∈ B → F ⁡ t = 1
34 29 33 breqtrrd ⊢ φ ∧ t ∈ B → 1 − E < F ⁡ t
35 34 ex ⊢ φ → t ∈ B → 1 − E < F ⁡ t
36 2 35 ralrimi ⊢ φ → ∀ t ∈ B 1 − E < F ⁡ t
37 nfcv ⊢ Ⅎ _ t x
38 nfmpt1 ⊢ Ⅎ _ t t ∈ T ⟼ 1
39 3 38 nfcxfr ⊢ Ⅎ _ t F
40 37 39 nfeq ⊢ Ⅎ t x = F
41 fveq1 ⊢ x = F → x ⁡ t = F ⁡ t
42 41 breq2d ⊢ x = F → 0 ≤ x ⁡ t ↔ 0 ≤ F ⁡ t
43 41 breq1d ⊢ x = F → x ⁡ t ≤ 1 ↔ F ⁡ t ≤ 1
44 42 43 anbi12d ⊢ x = F → 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ↔ 0 ≤ F ⁡ t ∧ F ⁡ t ≤ 1
45 40 44 ralbid ⊢ x = F → ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ↔ ∀ t ∈ T 0 ≤ F ⁡ t ∧ F ⁡ t ≤ 1
46 41 breq1d ⊢ x = F → x ⁡ t < E ↔ F ⁡ t < E
47 40 46 ralbid ⊢ x = F → ∀ t ∈ D x ⁡ t < E ↔ ∀ t ∈ D F ⁡ t < E
48 41 breq2d ⊢ x = F → 1 − E < x ⁡ t ↔ 1 − E < F ⁡ t
49 40 48 ralbid ⊢ x = F → ∀ t ∈ B 1 − E < x ⁡ t ↔ ∀ t ∈ B 1 − E < F ⁡ t
50 45 47 49 3anbi123d ⊢ x = F → ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ∧ ∀ t ∈ D x ⁡ t < E ∧ ∀ t ∈ B 1 − E < x ⁡ t ↔ ∀ t ∈ T 0 ≤ F ⁡ t ∧ F ⁡ t ≤ 1 ∧ ∀ t ∈ D F ⁡ t < E ∧ ∀ t ∈ B 1 − E < F ⁡ t
51 50 rspcev ⊢ F ∈ A ∧ ∀ t ∈ T 0 ≤ F ⁡ t ∧ F ⁡ t ≤ 1 ∧ ∀ t ∈ D F ⁡ t < E ∧ ∀ t ∈ B 1 − E < F ⁡ t → ∃ x ∈ A ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ∧ ∀ t ∈ D x ⁡ t < E ∧ ∀ t ∈ B 1 − E < x ⁡ t
52 12 22 26 36 51 syl13anc ⊢ φ → ∃ x ∈ A ∀ t ∈ T 0 ≤ x ⁡ t ∧ x ⁡ t ≤ 1 ∧ ∀ t ∈ D x ⁡ t < E ∧ ∀ t ∈ B 1 − E < x ⁡ t