Metamath Proof Explorer

Theorem relowlssretop

Description: The lower limit topology on the reals is finer than the standard topology. (Contributed by ML, 1-Aug-2020)

Ref Expression
Hypothesis relowlssretop.1 ⊢ 𝐼 = ( [,) “ ( ℝ × ℝ ) )
Assertion relowlssretop ( topGen ‘ ran (,) ) ⊆ ( topGen ‘ 𝐼 )

Proof

Step Hyp Ref Expression
1 relowlssretop.1 ⊢ 𝐼 = ( [,) “ ( ℝ × ℝ ) )
2 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
3 ffn ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
4 ovelrn ⊢ ( (,) Fn ( ℝ* × ℝ* ) → ( 𝑜 ∈ ran (,) ↔ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑜 = ( 𝑎 (,) 𝑏 ) ) )
5 2 3 4 mp2b ⊢ ( 𝑜 ∈ ran (,) ↔ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑜 = ( 𝑎 (,) 𝑏 ) )
6 elxr ⊢ ( 𝑏 ∈ ℝ* ↔ ( 𝑏 ∈ ℝ ∨ 𝑏 = +∞ ∨ 𝑏 = -∞ ) )
7 simpr ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ ) → 𝑏 ∈ ℝ )
8 elioore ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → 𝑥 ∈ ℝ )
9 7 8 anim12ci ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( 𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ ) )
10 1 icoreelrn ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ∈ 𝐼 )
11 9 10 syl ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ∈ 𝐼 )
12 8 adantl ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → 𝑥 ∈ ℝ )
13 8 leidd ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → 𝑥 ≤ 𝑥 )
14 13 adantl ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → 𝑥 ≤ 𝑥 )
15 7 rexrd ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ ) → 𝑏 ∈ ℝ* )
16 elioo1 ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) )
17 15 16 syldan ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ ) → ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) )
18 17 biimpa ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( 𝑥 ∈ ℝ* ∧ 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) )
19 18 simp3d ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → 𝑥 < 𝑏 )
20 rexr ⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ* )
21 20 3anim1i ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏 ) → ( 𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏 ) )
22 rexr ⊢ ( 𝑏 ∈ ℝ → 𝑏 ∈ ℝ* )
23 elico1 ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑥 [,) 𝑏 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏 ) ) )
24 20 22 23 syl2an ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑥 ∈ ( 𝑥 [,) 𝑏 ) ↔ ( 𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏 ) ) )
25 24 biimprd ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( ( 𝑥 ∈ ℝ* ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏 ) → 𝑥 ∈ ( 𝑥 [,) 𝑏 ) ) )
26 9 21 25 syl2im ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏 ) → 𝑥 ∈ ( 𝑥 [,) 𝑏 ) ) )
27 icoreval ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ ) → ( 𝑥 [,) 𝑏 ) = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } )
28 9 27 syl ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( 𝑥 [,) 𝑏 ) = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } )
29 28 eleq2d ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( 𝑥 ∈ ( 𝑥 [,) 𝑏 ) ↔ 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) )
30 26 29 sylibd ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑏 ) → 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) )
31 12 14 19 30 mp3and ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } )
32 nfv ⊢ Ⅎ 𝑧 ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) )
33 nfrab1 ⊢ Ⅎ 𝑧 { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) }
34 nfcv ⊢ Ⅎ 𝑧 ( 𝑎 (,) 𝑏 )
35 iooval ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( 𝑎 (,) 𝑏 ) = { 𝑥 ∈ ℝ* ∣ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) } )
36 35 eleq2d ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ↔ 𝑥 ∈ { 𝑥 ∈ ℝ* ∣ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) } ) )
37 36 anbi1d ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ↔ ( 𝑥 ∈ { 𝑥 ∈ ℝ* ∣ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) } ∧ 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ) )
38 37 pm5.32i ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ) ↔ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( 𝑥 ∈ { 𝑥 ∈ ℝ* ∣ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) } ∧ 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ) )
39 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ ℝ* ∣ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) } ↔ ( 𝑥 ∈ ℝ* ∧ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) )
40 rabid ⊢ ( 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ↔ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) )
41 39 40 anbi12i ⊢ ( ( 𝑥 ∈ { 𝑥 ∈ ℝ* ∣ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) } ∧ 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ↔ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) )
42 simpl ⊢ ( ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) → 𝑧 ∈ ℝ )
43 42 rexrd ⊢ ( ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) → 𝑧 ∈ ℝ* )
44 43 ad2antll ⊢ ( ( 𝑎 ∈ ℝ* ∧ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) ) → 𝑧 ∈ ℝ* )
45 simpl ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) → 𝑥 ∈ ℝ* )
46 45 43 anim12i ⊢ ( ( ( 𝑥 ∈ ℝ* ∧ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) → ( 𝑥 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) )
47 46 anim2i ⊢ ( ( 𝑎 ∈ ℝ* ∧ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) ) → ( 𝑎 ∈ ℝ* ∧ ( 𝑥 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ) )
48 3anass ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ↔ ( 𝑎 ∈ ℝ* ∧ ( 𝑥 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) ) )
49 47 48 sylibr ⊢ ( ( 𝑎 ∈ ℝ* ∧ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) ) → ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) )
50 simprl ⊢ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) → 𝑎 < 𝑥 )
51 simprl ⊢ ( ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) → 𝑥 ≤ 𝑧 )
52 50 51 anim12i ⊢ ( ( ( 𝑥 ∈ ℝ* ∧ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) → ( 𝑎 < 𝑥 ∧ 𝑥 ≤ 𝑧 ) )
53 52 adantl ⊢ ( ( 𝑎 ∈ ℝ* ∧ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) ) → ( 𝑎 < 𝑥 ∧ 𝑥 ≤ 𝑧 ) )
54 xrltletr ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( ( 𝑎 < 𝑥 ∧ 𝑥 ≤ 𝑧 ) → 𝑎 < 𝑧 ) )
55 49 53 54 sylc ⊢ ( ( 𝑎 ∈ ℝ* ∧ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) ) → 𝑎 < 𝑧 )
56 simprr ⊢ ( ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) → 𝑧 < 𝑏 )
57 56 ad2antll ⊢ ( ( 𝑎 ∈ ℝ* ∧ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) ) → 𝑧 < 𝑏 )
58 55 57 jca ⊢ ( ( 𝑎 ∈ ℝ* ∧ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) ) → ( 𝑎 < 𝑧 ∧ 𝑧 < 𝑏 ) )
59 rabid ⊢ ( 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ( 𝑎 < 𝑧 ∧ 𝑧 < 𝑏 ) } ↔ ( 𝑧 ∈ ℝ* ∧ ( 𝑎 < 𝑧 ∧ 𝑧 < 𝑏 ) ) )
60 44 58 59 sylanbrc ⊢ ( ( 𝑎 ∈ ℝ* ∧ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) ) → 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ( 𝑎 < 𝑧 ∧ 𝑧 < 𝑏 ) } )
61 60 adantlr ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) ) → 𝑧 ∈ { 𝑧 ∈ ℝ* ∣ ( 𝑎 < 𝑧 ∧ 𝑧 < 𝑏 ) } )
62 iooval ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( 𝑎 (,) 𝑏 ) = { 𝑧 ∈ ℝ* ∣ ( 𝑎 < 𝑧 ∧ 𝑧 < 𝑏 ) } )
63 62 adantr ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) ) → ( 𝑎 (,) 𝑏 ) = { 𝑧 ∈ ℝ* ∣ ( 𝑎 < 𝑧 ∧ 𝑧 < 𝑏 ) } )
64 61 63 eleqtrrd ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( ( 𝑥 ∈ ℝ* ∧ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) ) ) ) → 𝑧 ∈ ( 𝑎 (,) 𝑏 ) )
65 41 64 sylan2b ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( 𝑥 ∈ { 𝑥 ∈ ℝ* ∣ ( 𝑎 < 𝑥 ∧ 𝑥 < 𝑏 ) } ∧ 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ) → 𝑧 ∈ ( 𝑎 (,) 𝑏 ) )
66 38 65 sylbi ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) ) → 𝑧 ∈ ( 𝑎 (,) 𝑏 ) )
67 66 expr ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } → 𝑧 ∈ ( 𝑎 (,) 𝑏 ) ) )
68 32 33 34 67 ssrd ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ⊆ ( 𝑎 (,) 𝑏 ) )
69 22 68 sylanl2 ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ⊆ ( 𝑎 (,) 𝑏 ) )
70 eleq2 ⊢ ( 𝑖 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } → ( 𝑥 ∈ 𝑖 ↔ 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ) )
71 sseq1 ⊢ ( 𝑖 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } → ( 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ↔ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ⊆ ( 𝑎 (,) 𝑏 ) ) )
72 70 71 anbi12d ⊢ ( 𝑖 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } → ( ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) ↔ ( 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ∧ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ⊆ ( 𝑎 (,) 𝑏 ) ) ) )
73 72 rspcev ⊢ ( ( { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ∈ 𝐼 ∧ ( 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ∧ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑏 ) } ⊆ ( 𝑎 (,) 𝑏 ) ) ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) )
74 11 31 69 73 syl12anc ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) )
75 74 ancom1s ⊢ ( ( ( 𝑏 ∈ ℝ ∧ 𝑎 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) )
76 75 expl ⊢ ( 𝑏 ∈ ℝ → ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) ) )
77 8 adantl ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 = +∞ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → 𝑥 ∈ ℝ )
78 peano2re ⊢ ( 𝑥 ∈ ℝ → ( 𝑥 + 1 ) ∈ ℝ )
79 1 icoreelrn ⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑥 + 1 ) ∈ ℝ ) → { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ∈ 𝐼 )
80 77 78 79 syl2anc2 ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 = +∞ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ∈ 𝐼 )
81 elioore ⊢ ( 𝑥 ∈ ( 𝑎 (,) +∞ ) → 𝑥 ∈ ℝ )
82 81 adantl ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) → 𝑥 ∈ ℝ )
83 82 leidd ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) → 𝑥 ≤ 𝑥 )
84 82 ltp1d ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) → 𝑥 < ( 𝑥 + 1 ) )
85 82 83 84 jca32 ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) → ( 𝑥 ∈ ℝ ∧ ( 𝑥 ≤ 𝑥 ∧ 𝑥 < ( 𝑥 + 1 ) ) ) )
86 breq2 ⊢ ( 𝑧 = 𝑥 → ( 𝑥 ≤ 𝑧 ↔ 𝑥 ≤ 𝑥 ) )
87 breq1 ⊢ ( 𝑧 = 𝑥 → ( 𝑧 < ( 𝑥 + 1 ) ↔ 𝑥 < ( 𝑥 + 1 ) ) )
88 86 87 anbi12d ⊢ ( 𝑧 = 𝑥 → ( ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) ↔ ( 𝑥 ≤ 𝑥 ∧ 𝑥 < ( 𝑥 + 1 ) ) ) )
89 88 elrab ⊢ ( 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ↔ ( 𝑥 ∈ ℝ ∧ ( 𝑥 ≤ 𝑥 ∧ 𝑥 < ( 𝑥 + 1 ) ) ) )
90 85 89 sylibr ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) → 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } )
91 nfv ⊢ Ⅎ 𝑧 ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) )
92 nfrab1 ⊢ Ⅎ 𝑧 { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) }
93 nfcv ⊢ Ⅎ 𝑧 ( 𝑎 (,) +∞ )
94 rabid ⊢ ( 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ↔ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) ) )
95 simprl ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) ) ) → 𝑧 ∈ ℝ )
96 simpll ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) ) ) → 𝑎 ∈ ℝ* )
97 82 adantr ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) ) ) → 𝑥 ∈ ℝ )
98 97 rexrd ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) ) ) → 𝑥 ∈ ℝ* )
99 95 rexrd ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) ) ) → 𝑧 ∈ ℝ* )
100 elioopnf ⊢ ( 𝑎 ∈ ℝ* → ( 𝑥 ∈ ( 𝑎 (,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑎 < 𝑥 ) ) )
101 100 simplbda ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) → 𝑎 < 𝑥 )
102 101 adantr ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) ) ) → 𝑎 < 𝑥 )
103 simprl ⊢ ( ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) ) → 𝑥 ≤ 𝑧 )
104 103 adantl ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) ) ) → 𝑥 ≤ 𝑧 )
105 96 98 99 102 104 xrltletrd ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) ) ) → 𝑎 < 𝑧 )
106 elioopnf ⊢ ( 𝑎 ∈ ℝ* → ( 𝑧 ∈ ( 𝑎 (,) +∞ ) ↔ ( 𝑧 ∈ ℝ ∧ 𝑎 < 𝑧 ) ) )
107 106 biimprd ⊢ ( 𝑎 ∈ ℝ* → ( ( 𝑧 ∈ ℝ ∧ 𝑎 < 𝑧 ) → 𝑧 ∈ ( 𝑎 (,) +∞ ) ) )
108 107 adantr ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) → ( ( 𝑧 ∈ ℝ ∧ 𝑎 < 𝑧 ) → 𝑧 ∈ ( 𝑎 (,) +∞ ) ) )
109 108 adantr ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) ) ) → ( ( 𝑧 ∈ ℝ ∧ 𝑎 < 𝑧 ) → 𝑧 ∈ ( 𝑎 (,) +∞ ) ) )
110 95 105 109 mp2and ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) ∧ ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) ) ) → 𝑧 ∈ ( 𝑎 (,) +∞ ) )
111 110 ex ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) → ( ( 𝑧 ∈ ℝ ∧ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) ) → 𝑧 ∈ ( 𝑎 (,) +∞ ) ) )
112 94 111 biimtrid ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) → ( 𝑧 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } → 𝑧 ∈ ( 𝑎 (,) +∞ ) ) )
113 91 92 93 112 ssrd ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) → { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ⊆ ( 𝑎 (,) +∞ ) )
114 90 113 jca ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) → ( 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ∧ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ⊆ ( 𝑎 (,) +∞ ) ) )
115 oveq2 ⊢ ( 𝑏 = +∞ → ( 𝑎 (,) 𝑏 ) = ( 𝑎 (,) +∞ ) )
116 115 eleq2d ⊢ ( 𝑏 = +∞ → ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ↔ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) )
117 116 anbi2d ⊢ ( 𝑏 = +∞ → ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) ↔ ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) ) )
118 115 sseq2d ⊢ ( 𝑏 = +∞ → ( { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ⊆ ( 𝑎 (,) 𝑏 ) ↔ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ⊆ ( 𝑎 (,) +∞ ) ) )
119 118 anbi2d ⊢ ( 𝑏 = +∞ → ( ( 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ∧ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ⊆ ( 𝑎 (,) 𝑏 ) ) ↔ ( 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ∧ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ⊆ ( 𝑎 (,) +∞ ) ) ) )
120 117 119 imbi12d ⊢ ( 𝑏 = +∞ → ( ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ∧ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ⊆ ( 𝑎 (,) 𝑏 ) ) ) ↔ ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) +∞ ) ) → ( 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ∧ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ⊆ ( 𝑎 (,) +∞ ) ) ) ) )
121 114 120 mpbiri ⊢ ( 𝑏 = +∞ → ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ∧ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ⊆ ( 𝑎 (,) 𝑏 ) ) ) )
122 121 impl ⊢ ( ( ( 𝑏 = +∞ ∧ 𝑎 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ∧ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ⊆ ( 𝑎 (,) 𝑏 ) ) )
123 122 ancom1s ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 = +∞ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ( 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ∧ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ⊆ ( 𝑎 (,) 𝑏 ) ) )
124 eleq2 ⊢ ( 𝑖 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } → ( 𝑥 ∈ 𝑖 ↔ 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ) )
125 sseq1 ⊢ ( 𝑖 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } → ( 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ↔ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ⊆ ( 𝑎 (,) 𝑏 ) ) )
126 124 125 anbi12d ⊢ ( 𝑖 = { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } → ( ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) ↔ ( 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ∧ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ⊆ ( 𝑎 (,) 𝑏 ) ) ) )
127 126 rspcev ⊢ ( ( { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ∈ 𝐼 ∧ ( 𝑥 ∈ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ∧ { 𝑧 ∈ ℝ ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < ( 𝑥 + 1 ) ) } ⊆ ( 𝑎 (,) 𝑏 ) ) ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) )
128 80 123 127 syl2anc ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 = +∞ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) )
129 128 ancom1s ⊢ ( ( ( 𝑏 = +∞ ∧ 𝑎 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) )
130 129 expl ⊢ ( 𝑏 = +∞ → ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) ) )
131 8 adantl ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 = -∞ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → 𝑥 ∈ ℝ )
132 oveq2 ⊢ ( 𝑏 = -∞ → ( 𝑎 (,) 𝑏 ) = ( 𝑎 (,) -∞ ) )
133 132 eleq2d ⊢ ( 𝑏 = -∞ → ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ↔ 𝑥 ∈ ( 𝑎 (,) -∞ ) ) )
134 133 adantl ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 = -∞ ) → ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ↔ 𝑥 ∈ ( 𝑎 (,) -∞ ) ) )
135 134 pm5.32i ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 = -∞ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) ↔ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 = -∞ ) ∧ 𝑥 ∈ ( 𝑎 (,) -∞ ) ) )
136 nltmnf ⊢ ( 𝑥 ∈ ℝ* → ¬ 𝑥 < -∞ )
137 136 intnand ⊢ ( 𝑥 ∈ ℝ* → ¬ ( 𝑎 < 𝑥 ∧ 𝑥 < -∞ ) )
138 eliooord ⊢ ( 𝑥 ∈ ( 𝑎 (,) -∞ ) → ( 𝑎 < 𝑥 ∧ 𝑥 < -∞ ) )
139 137 138 nsyl ⊢ ( 𝑥 ∈ ℝ* → ¬ 𝑥 ∈ ( 𝑎 (,) -∞ ) )
140 139 pm2.21d ⊢ ( 𝑥 ∈ ℝ* → ( 𝑥 ∈ ( 𝑎 (,) -∞ ) → ( ( 𝑎 ∈ ℝ* ∧ 𝑏 = -∞ ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) ) ) )
141 140 impd ⊢ ( 𝑥 ∈ ℝ* → ( ( 𝑥 ∈ ( 𝑎 (,) -∞ ) ∧ ( 𝑎 ∈ ℝ* ∧ 𝑏 = -∞ ) ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) ) )
142 141 ancomsd ⊢ ( 𝑥 ∈ ℝ* → ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 = -∞ ) ∧ 𝑥 ∈ ( 𝑎 (,) -∞ ) ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) ) )
143 135 142 biimtrid ⊢ ( 𝑥 ∈ ℝ* → ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 = -∞ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) ) )
144 20 143 syl ⊢ ( 𝑥 ∈ ℝ → ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 = -∞ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) ) )
145 131 144 mpcom ⊢ ( ( ( 𝑎 ∈ ℝ* ∧ 𝑏 = -∞ ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) )
146 145 ancom1s ⊢ ( ( ( 𝑏 = -∞ ∧ 𝑎 ∈ ℝ* ) ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) )
147 146 expl ⊢ ( 𝑏 = -∞ → ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) ) )
148 76 130 147 3jaoi ⊢ ( ( 𝑏 ∈ ℝ ∨ 𝑏 = +∞ ∨ 𝑏 = -∞ ) → ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) ) )
149 6 148 sylbi ⊢ ( 𝑏 ∈ ℝ* → ( ( 𝑎 ∈ ℝ* ∧ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) ) )
150 149 expdimp ⊢ ( ( 𝑏 ∈ ℝ* ∧ 𝑎 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) ) )
151 150 ancoms ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) ) )
152 eleq2 ⊢ ( 𝑜 = ( 𝑎 (,) 𝑏 ) → ( 𝑥 ∈ 𝑜 ↔ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) )
153 sseq2 ⊢ ( 𝑜 = ( 𝑎 (,) 𝑏 ) → ( 𝑖 ⊆ 𝑜 ↔ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) )
154 153 anbi2d ⊢ ( 𝑜 = ( 𝑎 (,) 𝑏 ) → ( ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜 ) ↔ ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) ) )
155 154 rexbidv ⊢ ( 𝑜 = ( 𝑎 (,) 𝑏 ) → ( ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜 ) ↔ ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) ) )
156 152 155 imbi12d ⊢ ( 𝑜 = ( 𝑎 (,) 𝑏 ) → ( ( 𝑥 ∈ 𝑜 → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜 ) ) ↔ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ ( 𝑎 (,) 𝑏 ) ) ) ) )
157 151 156 syl5ibrcom ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( 𝑜 = ( 𝑎 (,) 𝑏 ) → ( 𝑥 ∈ 𝑜 → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜 ) ) ) )
158 157 rexlimivv ⊢ ( ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑜 = ( 𝑎 (,) 𝑏 ) → ( 𝑥 ∈ 𝑜 → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜 ) ) )
159 5 158 sylbi ⊢ ( 𝑜 ∈ ran (,) → ( 𝑥 ∈ 𝑜 → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜 ) ) )
160 159 rgen ⊢ ∀ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜 ) )
161 160 rgenw ⊢ ∀ 𝑥 ∈ ℝ ∀ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜 ) )
162 iooex ⊢ (,) ∈ V
163 162 rnex ⊢ ran (,) ∈ V
164 unirnioo ⊢ ℝ = ∪ ran (,)
165 1 icoreunrn ⊢ ℝ = ∪ 𝐼
166 164 165 eqtr3i ⊢ ∪ ran (,) = ∪ 𝐼
167 tgss2 ⊢ ( ( ran (,) ∈ V ∧ ∪ ran (,) = ∪ 𝐼 ) → ( ( topGen ‘ ran (,) ) ⊆ ( topGen ‘ 𝐼 ) ↔ ∀ 𝑥 ∈ ∪ ran (,) ∀ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜 ) ) ) )
168 163 166 167 mp2an ⊢ ( ( topGen ‘ ran (,) ) ⊆ ( topGen ‘ 𝐼 ) ↔ ∀ 𝑥 ∈ ∪ ran (,) ∀ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜 ) ) )
169 164 raleqi ⊢ ( ∀ 𝑥 ∈ ℝ ∀ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜 ) ) ↔ ∀ 𝑥 ∈ ∪ ran (,) ∀ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜 ) ) )
170 168 169 bitr4i ⊢ ( ( topGen ‘ ran (,) ) ⊆ ( topGen ‘ 𝐼 ) ↔ ∀ 𝑥 ∈ ℝ ∀ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 → ∃ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 ∧ 𝑖 ⊆ 𝑜 ) ) )
171 161 170 mpbir ⊢ ( topGen ‘ ran (,) ) ⊆ ( topGen ‘ 𝐼 )