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 ⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ inf ( ran ( 𝑦 ∈ 𝑆 ↦ ( 𝑥 𝐷 𝑦 ) ) , ℝ* , < ) )
metdscn.j ⊢ 𝐽 = ( MetOpen ‘ 𝐷 )
metnrmlem.1 ⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
metnrmlem.2 ⊢ ( 𝜑 → 𝑆 ∈ ( Clsd ‘ 𝐽 ) )
metnrmlem.3 ⊢ ( 𝜑 → 𝑇 ∈ ( Clsd ‘ 𝐽 ) )
metnrmlem.4 ⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ )
Assertion metnrmlem1a ( ( 𝜑 ∧ 𝐴 ∈ 𝑇 ) → ( 0 < ( 𝐹 ‘ 𝐴 ) ∧ if ( 1 ≤ ( 𝐹 ‘ 𝐴 ) , 1 , ( 𝐹 ‘ 𝐴 ) ) ∈ ℝ+ ) )

Proof

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