Metamath Proof Explorer

Theorem metnrmlem1a

Description: Lemma for metnrm . (Contributed by Mario Carneiro, 14-Jan-2014) (Revised by Mario Carneiro, 4-Sep-2015)

Ref Expression
Hypotheses metdscn.f ⊢ F = x ∈ X ⟼ inf ran ⁡ y ∈ S ⟼ x D y ℝ * <
metdscn.j ⊢ J = MetOpen ⁡ D
metnrmlem.1 ⊢ φ → D ∈ ∞Met ⁡ X
metnrmlem.2 ⊢ φ → S ∈ Clsd ⁡ J
metnrmlem.3 ⊢ φ → T ∈ Clsd ⁡ J
metnrmlem.4 ⊢ φ → S ∩ T = ∅
Assertion metnrmlem1a ⊢ φ ∧ A ∈ T → 0 < F ⁡ A ∧ if 1 ≤ F ⁡ A 1 F ⁡ A ∈ ℝ +

Proof

Step Hyp Ref Expression
1 metdscn.f ⊢ F = x ∈ X ⟼ inf ran ⁡ y ∈ S ⟼ x D y ℝ * <
2 metdscn.j ⊢ J = MetOpen ⁡ D
3 metnrmlem.1 ⊢ φ → D ∈ ∞Met ⁡ X
4 metnrmlem.2 ⊢ φ → S ∈ Clsd ⁡ J
5 metnrmlem.3 ⊢ φ → T ∈ Clsd ⁡ J
6 metnrmlem.4 ⊢ φ → S ∩ T = ∅
7 6 adantr ⊢ φ ∧ A ∈ T → S ∩ T = ∅
8 inelcm ⊢ A ∈ S ∧ A ∈ T → S ∩ T ≠ ∅
9 8 expcom ⊢ A ∈ T → A ∈ S → S ∩ T ≠ ∅
10 9 adantl ⊢ φ ∧ A ∈ T → A ∈ S → S ∩ T ≠ ∅
11 10 necon2bd ⊢ φ ∧ A ∈ T → S ∩ T = ∅ → ¬ A ∈ S
12 7 11 mpd ⊢ φ ∧ A ∈ T → ¬ A ∈ S
13 eqcom ⊢ 0 = F ⁡ A ↔ F ⁡ A = 0
14 3 adantr ⊢ φ ∧ A ∈ T → D ∈ ∞Met ⁡ X
15 4 adantr ⊢ φ ∧ A ∈ T → S ∈ Clsd ⁡ J
16 eqid ⊢ ⋃ J = ⋃ J
17 16 cldss ⊢ S ∈ Clsd ⁡ J → S ⊆ ⋃ J
18 15 17 syl ⊢ φ ∧ A ∈ T → S ⊆ ⋃ J
19 2 mopnuni ⊢ D ∈ ∞Met ⁡ X → X = ⋃ J
20 14 19 syl ⊢ φ ∧ A ∈ T → X = ⋃ J
21 18 20 sseqtrrd ⊢ φ ∧ A ∈ T → S ⊆ X
22 5 adantr ⊢ φ ∧ A ∈ T → T ∈ Clsd ⁡ J
23 16 cldss ⊢ T ∈ Clsd ⁡ J → T ⊆ ⋃ J
24 22 23 syl ⊢ φ ∧ A ∈ T → T ⊆ ⋃ J
25 24 20 sseqtrrd ⊢ φ ∧ A ∈ T → T ⊆ X
26 simpr ⊢ φ ∧ A ∈ T → A ∈ T
27 25 26 sseldd ⊢ φ ∧ A ∈ T → A ∈ X
28 1 2 metdseq0 ⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X ∧ A ∈ X → F ⁡ A = 0 ↔ A ∈ cls ⁡ J ⁡ S
29 14 21 27 28 syl3anc ⊢ φ ∧ A ∈ T → F ⁡ A = 0 ↔ A ∈ cls ⁡ J ⁡ S
30 13 29 bitrid ⊢ φ ∧ A ∈ T → 0 = F ⁡ A ↔ A ∈ cls ⁡ J ⁡ S
31 cldcls ⊢ S ∈ Clsd ⁡ J → cls ⁡ J ⁡ S = S
32 15 31 syl ⊢ φ ∧ A ∈ T → cls ⁡ J ⁡ S = S
33 32 eleq2d ⊢ φ ∧ A ∈ T → A ∈ cls ⁡ J ⁡ S ↔ A ∈ S
34 30 33 bitrd ⊢ φ ∧ A ∈ T → 0 = F ⁡ A ↔ A ∈ S
35 12 34 mtbird ⊢ φ ∧ A ∈ T → ¬ 0 = F ⁡ A
36 1 metdsf ⊢ D ∈ ∞Met ⁡ X ∧ S ⊆ X → F : X ⟶ 0 +∞
37 14 21 36 syl2anc ⊢ φ ∧ A ∈ T → F : X ⟶ 0 +∞
38 37 27 ffvelcdmd ⊢ φ ∧ A ∈ T → F ⁡ A ∈ 0 +∞
39 elxrge0 ⊢ F ⁡ A ∈ 0 +∞ ↔ F ⁡ A ∈ ℝ * ∧ 0 ≤ F ⁡ A
40 39 simprbi ⊢ F ⁡ A ∈ 0 +∞ → 0 ≤ F ⁡ A
41 38 40 syl ⊢ φ ∧ A ∈ T → 0 ≤ F ⁡ A
42 0xr ⊢ 0 ∈ ℝ *
43 eliccxr ⊢ F ⁡ A ∈ 0 +∞ → F ⁡ A ∈ ℝ *
44 38 43 syl ⊢ φ ∧ A ∈ T → F ⁡ A ∈ ℝ *
45 xrleloe ⊢ 0 ∈ ℝ * ∧ F ⁡ A ∈ ℝ * → 0 ≤ F ⁡ A ↔ 0 < F ⁡ A ∨ 0 = F ⁡ A
46 42 44 45 sylancr ⊢ φ ∧ A ∈ T → 0 ≤ F ⁡ A ↔ 0 < F ⁡ A ∨ 0 = F ⁡ A
47 41 46 mpbid ⊢ φ ∧ A ∈ T → 0 < F ⁡ A ∨ 0 = F ⁡ A
48 47 ord ⊢ φ ∧ A ∈ T → ¬ 0 < F ⁡ A → 0 = F ⁡ A
49 35 48 mt3d ⊢ φ ∧ A ∈ T → 0 < F ⁡ A
50 1xr ⊢ 1 ∈ ℝ *
51 ifcl ⊢ 1 ∈ ℝ * ∧ F ⁡ A ∈ ℝ * → if 1 ≤ F ⁡ A 1 F ⁡ A ∈ ℝ *
52 50 44 51 sylancr ⊢ φ ∧ A ∈ T → if 1 ≤ F ⁡ A 1 F ⁡ A ∈ ℝ *
53 1red ⊢ φ ∧ A ∈ T → 1 ∈ ℝ
54 0lt1 ⊢ 0 < 1
55 breq2 ⊢ 1 = if 1 ≤ F ⁡ A 1 F ⁡ A → 0 < 1 ↔ 0 < if 1 ≤ F ⁡ A 1 F ⁡ A
56 breq2 ⊢ F ⁡ A = if 1 ≤ F ⁡ A 1 F ⁡ A → 0 < F ⁡ A ↔ 0 < if 1 ≤ F ⁡ A 1 F ⁡ A
57 55 56 ifboth ⊢ 0 < 1 ∧ 0 < F ⁡ A → 0 < if 1 ≤ F ⁡ A 1 F ⁡ A
58 54 49 57 sylancr ⊢ φ ∧ A ∈ T → 0 < if 1 ≤ F ⁡ A 1 F ⁡ A
59 xrltle ⊢ 0 ∈ ℝ * ∧ if 1 ≤ F ⁡ A 1 F ⁡ A ∈ ℝ * → 0 < if 1 ≤ F ⁡ A 1 F ⁡ A → 0 ≤ if 1 ≤ F ⁡ A 1 F ⁡ A
60 42 52 59 sylancr ⊢ φ ∧ A ∈ T → 0 < if 1 ≤ F ⁡ A 1 F ⁡ A → 0 ≤ if 1 ≤ F ⁡ A 1 F ⁡ A
61 58 60 mpd ⊢ φ ∧ A ∈ T → 0 ≤ if 1 ≤ F ⁡ A 1 F ⁡ A
62 xrmin1 ⊢ 1 ∈ ℝ * ∧ F ⁡ A ∈ ℝ * → if 1 ≤ F ⁡ A 1 F ⁡ A ≤ 1
63 50 44 62 sylancr ⊢ φ ∧ A ∈ T → if 1 ≤ F ⁡ A 1 F ⁡ A ≤ 1
64 xrrege0 ⊢ if 1 ≤ F ⁡ A 1 F ⁡ A ∈ ℝ * ∧ 1 ∈ ℝ ∧ 0 ≤ if 1 ≤ F ⁡ A 1 F ⁡ A ∧ if 1 ≤ F ⁡ A 1 F ⁡ A ≤ 1 → if 1 ≤ F ⁡ A 1 F ⁡ A ∈ ℝ
65 52 53 61 63 64 syl22anc ⊢ φ ∧ A ∈ T → if 1 ≤ F ⁡ A 1 F ⁡ A ∈ ℝ
66 65 58 elrpd ⊢ φ ∧ A ∈ T → if 1 ≤ F ⁡ A 1 F ⁡ A ∈ ℝ +
67 49 66 jca ⊢ φ ∧ A ∈ T → 0 < F ⁡ A ∧ if 1 ≤ F ⁡ A 1 F ⁡ A ∈ ℝ +