Metamath Proof Explorer


Theorem icccmplem1

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

Ref Expression
Hypotheses icccmp.1 𝐽 = ( topGen ‘ ran (,) )
icccmp.2 𝑇 = ( 𝐽t ( 𝐴 [,] 𝐵 ) )
icccmp.3 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
icccmp.4 𝑆 = { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ 𝑧 }
icccmp.5 ( 𝜑𝐴 ∈ ℝ )
icccmp.6 ( 𝜑𝐵 ∈ ℝ )
icccmp.7 ( 𝜑𝐴𝐵 )
icccmp.8 ( 𝜑𝑈𝐽 )
icccmp.9 ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝑈 )
Assertion icccmplem1 ( 𝜑 → ( 𝐴𝑆 ∧ ∀ 𝑦𝑆 𝑦𝐵 ) )

Proof

Step Hyp Ref Expression
1 icccmp.1 𝐽 = ( topGen ‘ ran (,) )
2 icccmp.2 𝑇 = ( 𝐽t ( 𝐴 [,] 𝐵 ) )
3 icccmp.3 𝐷 = ( ( abs ∘ − ) ↾ ( ℝ × ℝ ) )
4 icccmp.4 𝑆 = { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ 𝑧 }
5 icccmp.5 ( 𝜑𝐴 ∈ ℝ )
6 icccmp.6 ( 𝜑𝐵 ∈ ℝ )
7 icccmp.7 ( 𝜑𝐴𝐵 )
8 icccmp.8 ( 𝜑𝑈𝐽 )
9 icccmp.9 ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝑈 )
10 5 rexrd ( 𝜑𝐴 ∈ ℝ* )
11 6 rexrd ( 𝜑𝐵 ∈ ℝ* )
12 lbicc2 ( ( 𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐴𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
13 10 11 7 12 syl3anc ( 𝜑𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
14 9 13 sseldd ( 𝜑𝐴 𝑈 )
15 eluni2 ( 𝐴 𝑈 ↔ ∃ 𝑢𝑈 𝐴𝑢 )
16 14 15 sylib ( 𝜑 → ∃ 𝑢𝑈 𝐴𝑢 )
17 snssi ( 𝑢𝑈 → { 𝑢 } ⊆ 𝑈 )
18 17 ad2antrl ( ( 𝜑 ∧ ( 𝑢𝑈𝐴𝑢 ) ) → { 𝑢 } ⊆ 𝑈 )
19 snex { 𝑢 } ∈ V
20 19 elpw ( { 𝑢 } ∈ 𝒫 𝑈 ↔ { 𝑢 } ⊆ 𝑈 )
21 18 20 sylibr ( ( 𝜑 ∧ ( 𝑢𝑈𝐴𝑢 ) ) → { 𝑢 } ∈ 𝒫 𝑈 )
22 snfi { 𝑢 } ∈ Fin
23 22 a1i ( ( 𝜑 ∧ ( 𝑢𝑈𝐴𝑢 ) ) → { 𝑢 } ∈ Fin )
24 21 23 elind ( ( 𝜑 ∧ ( 𝑢𝑈𝐴𝑢 ) ) → { 𝑢 } ∈ ( 𝒫 𝑈 ∩ Fin ) )
25 10 adantr ( ( 𝜑 ∧ ( 𝑢𝑈𝐴𝑢 ) ) → 𝐴 ∈ ℝ* )
26 iccid ( 𝐴 ∈ ℝ* → ( 𝐴 [,] 𝐴 ) = { 𝐴 } )
27 25 26 syl ( ( 𝜑 ∧ ( 𝑢𝑈𝐴𝑢 ) ) → ( 𝐴 [,] 𝐴 ) = { 𝐴 } )
28 snssi ( 𝐴𝑢 → { 𝐴 } ⊆ 𝑢 )
29 28 ad2antll ( ( 𝜑 ∧ ( 𝑢𝑈𝐴𝑢 ) ) → { 𝐴 } ⊆ 𝑢 )
30 27 29 eqsstrd ( ( 𝜑 ∧ ( 𝑢𝑈𝐴𝑢 ) ) → ( 𝐴 [,] 𝐴 ) ⊆ 𝑢 )
31 unieq ( 𝑧 = { 𝑢 } → 𝑧 = { 𝑢 } )
32 vex 𝑢 ∈ V
33 32 unisn { 𝑢 } = 𝑢
34 31 33 eqtrdi ( 𝑧 = { 𝑢 } → 𝑧 = 𝑢 )
35 34 sseq2d ( 𝑧 = { 𝑢 } → ( ( 𝐴 [,] 𝐴 ) ⊆ 𝑧 ↔ ( 𝐴 [,] 𝐴 ) ⊆ 𝑢 ) )
36 35 rspcev ( ( { 𝑢 } ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ ( 𝐴 [,] 𝐴 ) ⊆ 𝑢 ) → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝐴 ) ⊆ 𝑧 )
37 24 30 36 syl2anc ( ( 𝜑 ∧ ( 𝑢𝑈𝐴𝑢 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝐴 ) ⊆ 𝑧 )
38 16 37 rexlimddv ( 𝜑 → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝐴 ) ⊆ 𝑧 )
39 oveq2 ( 𝑥 = 𝐴 → ( 𝐴 [,] 𝑥 ) = ( 𝐴 [,] 𝐴 ) )
40 39 sseq1d ( 𝑥 = 𝐴 → ( ( 𝐴 [,] 𝑥 ) ⊆ 𝑧 ↔ ( 𝐴 [,] 𝐴 ) ⊆ 𝑧 ) )
41 40 rexbidv ( 𝑥 = 𝐴 → ( ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝑥 ) ⊆ 𝑧 ↔ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝐴 ) ⊆ 𝑧 ) )
42 41 4 elrab2 ( 𝐴𝑆 ↔ ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) ( 𝐴 [,] 𝐴 ) ⊆ 𝑧 ) )
43 13 38 42 sylanbrc ( 𝜑𝐴𝑆 )
44 4 ssrab3 𝑆 ⊆ ( 𝐴 [,] 𝐵 )
45 44 sseli ( 𝑦𝑆𝑦 ∈ ( 𝐴 [,] 𝐵 ) )
46 elicc2 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴𝑦𝑦𝐵 ) ) )
47 5 6 46 syl2anc ( 𝜑 → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝐴𝑦𝑦𝐵 ) ) )
48 47 biimpa ( ( 𝜑𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑦 ∈ ℝ ∧ 𝐴𝑦𝑦𝐵 ) )
49 48 simp3d ( ( 𝜑𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑦𝐵 )
50 45 49 sylan2 ( ( 𝜑𝑦𝑆 ) → 𝑦𝐵 )
51 50 ralrimiva ( 𝜑 → ∀ 𝑦𝑆 𝑦𝐵 )
52 43 51 jca ( 𝜑 → ( 𝐴𝑆 ∧ ∀ 𝑦𝑆 𝑦𝐵 ) )