Metamath Proof Explorer

Theorem icccmplem3

Description: Lemma for icccmp . (Contributed by Mario Carneiro, 13-Jun-2014)

Ref Expression
Hypotheses icccmp.1 ⊢ J = topGen ⁡ ran ⁡ .
icccmp.2 ⊢ T = J ↾ 𝑡 A B
icccmp.3 ⊢ D = abs ∘ − ↾ ℝ 2
icccmp.4 ⊢ S = x ∈ A B | ∃ z ∈ 𝒫 U ∩ Fin A x ⊆ ⋃ z
icccmp.5 ⊢ φ → A ∈ ℝ
icccmp.6 ⊢ φ → B ∈ ℝ
icccmp.7 ⊢ φ → A ≤ B
icccmp.8 ⊢ φ → U ⊆ J
icccmp.9 ⊢ φ → A B ⊆ ⋃ U
Assertion icccmplem3 ⊢ φ → B ∈ S

Proof

Step Hyp Ref Expression
1 icccmp.1 ⊢ J = topGen ⁡ ran ⁡ .
2 icccmp.2 ⊢ T = J ↾ 𝑡 A B
3 icccmp.3 ⊢ D = abs ∘ − ↾ ℝ 2
4 icccmp.4 ⊢ S = x ∈ A B | ∃ z ∈ 𝒫 U ∩ Fin A x ⊆ ⋃ z
5 icccmp.5 ⊢ φ → A ∈ ℝ
6 icccmp.6 ⊢ φ → B ∈ ℝ
7 icccmp.7 ⊢ φ → A ≤ B
8 icccmp.8 ⊢ φ → U ⊆ J
9 icccmp.9 ⊢ φ → A B ⊆ ⋃ U
10 4 ssrab3 ⊢ S ⊆ A B
11 iccssre ⊢ A ∈ ℝ ∧ B ∈ ℝ → A B ⊆ ℝ
12 5 6 11 syl2anc ⊢ φ → A B ⊆ ℝ
13 10 12 sstrid ⊢ φ → S ⊆ ℝ
14 1 2 3 4 5 6 7 8 9 icccmplem1 ⊢ φ → A ∈ S ∧ ∀ y ∈ S y ≤ B
15 14 simpld ⊢ φ → A ∈ S
16 15 ne0d ⊢ φ → S ≠ ∅
17 14 simprd ⊢ φ → ∀ y ∈ S y ≤ B
18 brralrspcev ⊢ B ∈ ℝ ∧ ∀ y ∈ S y ≤ B → ∃ v ∈ ℝ ∀ y ∈ S y ≤ v
19 6 17 18 syl2anc ⊢ φ → ∃ v ∈ ℝ ∀ y ∈ S y ≤ v
20 13 16 19 suprcld ⊢ φ → sup S ℝ < ∈ ℝ
21 13 16 19 15 suprubd ⊢ φ → A ≤ sup S ℝ <
22 suprleub ⊢ S ⊆ ℝ ∧ S ≠ ∅ ∧ ∃ v ∈ ℝ ∀ y ∈ S y ≤ v ∧ B ∈ ℝ → sup S ℝ < ≤ B ↔ ∀ y ∈ S y ≤ B
23 13 16 19 6 22 syl31anc ⊢ φ → sup S ℝ < ≤ B ↔ ∀ y ∈ S y ≤ B
24 17 23 mpbird ⊢ φ → sup S ℝ < ≤ B
25 elicc2 ⊢ A ∈ ℝ ∧ B ∈ ℝ → sup S ℝ < ∈ A B ↔ sup S ℝ < ∈ ℝ ∧ A ≤ sup S ℝ < ∧ sup S ℝ < ≤ B
26 5 6 25 syl2anc ⊢ φ → sup S ℝ < ∈ A B ↔ sup S ℝ < ∈ ℝ ∧ A ≤ sup S ℝ < ∧ sup S ℝ < ≤ B
27 20 21 24 26 mpbir3and ⊢ φ → sup S ℝ < ∈ A B
28 9 27 sseldd ⊢ φ → sup S ℝ < ∈ ⋃ U
29 eluni2 ⊢ sup S ℝ < ∈ ⋃ U ↔ ∃ u ∈ U sup S ℝ < ∈ u
30 28 29 sylib ⊢ φ → ∃ u ∈ U sup S ℝ < ∈ u
31 8 sselda ⊢ φ ∧ u ∈ U → u ∈ J
32 3 rexmet ⊢ D ∈ ∞Met ⁡ ℝ
33 eqid ⊢ MetOpen ⁡ D = MetOpen ⁡ D
34 3 33 tgioo ⊢ topGen ⁡ ran ⁡ . = MetOpen ⁡ D
35 1 34 eqtri ⊢ J = MetOpen ⁡ D
36 35 mopni2 ⊢ D ∈ ∞Met ⁡ ℝ ∧ u ∈ J ∧ sup S ℝ < ∈ u → ∃ w ∈ ℝ + sup S ℝ < ball ⁡ D w ⊆ u
37 32 36 mp3an1 ⊢ u ∈ J ∧ sup S ℝ < ∈ u → ∃ w ∈ ℝ + sup S ℝ < ball ⁡ D w ⊆ u
38 37 ex ⊢ u ∈ J → sup S ℝ < ∈ u → ∃ w ∈ ℝ + sup S ℝ < ball ⁡ D w ⊆ u
39 31 38 syl ⊢ φ ∧ u ∈ U → sup S ℝ < ∈ u → ∃ w ∈ ℝ + sup S ℝ < ball ⁡ D w ⊆ u
40 5 ad2antrr ⊢ φ ∧ u ∈ U ∧ w ∈ ℝ + ∧ sup S ℝ < ball ⁡ D w ⊆ u → A ∈ ℝ
41 6 ad2antrr ⊢ φ ∧ u ∈ U ∧ w ∈ ℝ + ∧ sup S ℝ < ball ⁡ D w ⊆ u → B ∈ ℝ
42 7 ad2antrr ⊢ φ ∧ u ∈ U ∧ w ∈ ℝ + ∧ sup S ℝ < ball ⁡ D w ⊆ u → A ≤ B
43 8 ad2antrr ⊢ φ ∧ u ∈ U ∧ w ∈ ℝ + ∧ sup S ℝ < ball ⁡ D w ⊆ u → U ⊆ J
44 9 ad2antrr ⊢ φ ∧ u ∈ U ∧ w ∈ ℝ + ∧ sup S ℝ < ball ⁡ D w ⊆ u → A B ⊆ ⋃ U
45 simplr ⊢ φ ∧ u ∈ U ∧ w ∈ ℝ + ∧ sup S ℝ < ball ⁡ D w ⊆ u → u ∈ U
46 simprl ⊢ φ ∧ u ∈ U ∧ w ∈ ℝ + ∧ sup S ℝ < ball ⁡ D w ⊆ u → w ∈ ℝ +
47 simprr ⊢ φ ∧ u ∈ U ∧ w ∈ ℝ + ∧ sup S ℝ < ball ⁡ D w ⊆ u → sup S ℝ < ball ⁡ D w ⊆ u
48 eqid ⊢ sup S ℝ < = sup S ℝ <
49 eqid ⊢ if sup S ℝ < + w 2 ≤ B sup S ℝ < + w 2 B = if sup S ℝ < + w 2 ≤ B sup S ℝ < + w 2 B
50 1 2 3 4 40 41 42 43 44 45 46 47 48 49 icccmplem2 ⊢ φ ∧ u ∈ U ∧ w ∈ ℝ + ∧ sup S ℝ < ball ⁡ D w ⊆ u → B ∈ S
51 50 rexlimdvaa ⊢ φ ∧ u ∈ U → ∃ w ∈ ℝ + sup S ℝ < ball ⁡ D w ⊆ u → B ∈ S
52 39 51 syld ⊢ φ ∧ u ∈ U → sup S ℝ < ∈ u → B ∈ S
53 52 rexlimdva ⊢ φ → ∃ u ∈ U sup S ℝ < ∈ u → B ∈ S
54 30 53 mpd ⊢ φ → B ∈ S