Metamath Proof Explorer

Theorem relowlpssretop

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

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

Proof

Step Hyp Ref Expression
1 relowlpssretop.1 ⊢ 𝐼 = ( [,) “ ( ℝ × ℝ ) )
2 1 relowlssretop ⊢ ( topGen ‘ ran (,) ) ⊆ ( topGen ‘ 𝐼 )
3 2re ⊢ 2 ∈ ℝ
4 1lt2 ⊢ 1 < 2
5 ovex ⊢ ( 1 [,) 𝑐 ) ∈ V
6 sbcan ⊢ ( [ 1 / 𝑥 ] ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ↔ ( [ 1 / 𝑥 ] 𝑐 ∈ ℝ ∧ [ 1 / 𝑥 ] 𝑥 < 𝑐 ) )
7 1re ⊢ 1 ∈ ℝ
8 sbcg ⊢ ( 1 ∈ ℝ → ( [ 1 / 𝑥 ] 𝑐 ∈ ℝ ↔ 𝑐 ∈ ℝ ) )
9 7 8 ax-mp ⊢ ( [ 1 / 𝑥 ] 𝑐 ∈ ℝ ↔ 𝑐 ∈ ℝ )
10 sbcbr123 ⊢ ( [ 1 / 𝑥 ] 𝑥 < 𝑐 ↔ ⦋ 1 / 𝑥 ⦌ 𝑥 ⦋ 1 / 𝑥 ⦌ < ⦋ 1 / 𝑥 ⦌ 𝑐 )
11 csbvarg ⊢ ( 1 ∈ ℝ → ⦋ 1 / 𝑥 ⦌ 𝑥 = 1 )
12 7 11 ax-mp ⊢ ⦋ 1 / 𝑥 ⦌ 𝑥 = 1
13 csbconstg ⊢ ( 1 ∈ ℝ → ⦋ 1 / 𝑥 ⦌ 𝑐 = 𝑐 )
14 7 13 ax-mp ⊢ ⦋ 1 / 𝑥 ⦌ 𝑐 = 𝑐
15 12 14 breq12i ⊢ ( ⦋ 1 / 𝑥 ⦌ 𝑥 ⦋ 1 / 𝑥 ⦌ < ⦋ 1 / 𝑥 ⦌ 𝑐 ↔ 1 ⦋ 1 / 𝑥 ⦌ < 𝑐 )
16 csbconstg ⊢ ( 1 ∈ ℝ → ⦋ 1 / 𝑥 ⦌ < = < )
17 7 16 ax-mp ⊢ ⦋ 1 / 𝑥 ⦌ < = <
18 17 breqi ⊢ ( 1 ⦋ 1 / 𝑥 ⦌ < 𝑐 ↔ 1 < 𝑐 )
19 10 15 18 3bitri ⊢ ( [ 1 / 𝑥 ] 𝑥 < 𝑐 ↔ 1 < 𝑐 )
20 9 19 anbi12i ⊢ ( ( [ 1 / 𝑥 ] 𝑐 ∈ ℝ ∧ [ 1 / 𝑥 ] 𝑥 < 𝑐 ) ↔ ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) )
21 6 20 bitri ⊢ ( [ 1 / 𝑥 ] ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ↔ ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) )
22 sbceqg ⊢ ( 1 ∈ ℝ → ( [ 1 / 𝑥 ] 𝑖 = ( 𝑥 [,) 𝑐 ) ↔ ⦋ 1 / 𝑥 ⦌ 𝑖 = ⦋ 1 / 𝑥 ⦌ ( 𝑥 [,) 𝑐 ) ) )
23 7 22 ax-mp ⊢ ( [ 1 / 𝑥 ] 𝑖 = ( 𝑥 [,) 𝑐 ) ↔ ⦋ 1 / 𝑥 ⦌ 𝑖 = ⦋ 1 / 𝑥 ⦌ ( 𝑥 [,) 𝑐 ) )
24 csbconstg ⊢ ( 1 ∈ ℝ → ⦋ 1 / 𝑥 ⦌ 𝑖 = 𝑖 )
25 7 24 ax-mp ⊢ ⦋ 1 / 𝑥 ⦌ 𝑖 = 𝑖
26 csbov123 ⊢ ⦋ 1 / 𝑥 ⦌ ( 𝑥 [,) 𝑐 ) = ( ⦋ 1 / 𝑥 ⦌ 𝑥 ⦋ 1 / 𝑥 ⦌ [,) ⦋ 1 / 𝑥 ⦌ 𝑐 )
27 csbconstg ⊢ ( 1 ∈ ℝ → ⦋ 1 / 𝑥 ⦌ [,) = [,) )
28 7 27 ax-mp ⊢ ⦋ 1 / 𝑥 ⦌ [,) = [,)
29 12 14 28 oveq123i ⊢ ( ⦋ 1 / 𝑥 ⦌ 𝑥 ⦋ 1 / 𝑥 ⦌ [,) ⦋ 1 / 𝑥 ⦌ 𝑐 ) = ( 1 [,) 𝑐 )
30 26 29 eqtri ⊢ ⦋ 1 / 𝑥 ⦌ ( 𝑥 [,) 𝑐 ) = ( 1 [,) 𝑐 )
31 25 30 eqeq12i ⊢ ( ⦋ 1 / 𝑥 ⦌ 𝑖 = ⦋ 1 / 𝑥 ⦌ ( 𝑥 [,) 𝑐 ) ↔ 𝑖 = ( 1 [,) 𝑐 ) )
32 23 31 bitri ⊢ ( [ 1 / 𝑥 ] 𝑖 = ( 𝑥 [,) 𝑐 ) ↔ 𝑖 = ( 1 [,) 𝑐 ) )
33 sbcan ⊢ ( [ 1 / 𝑥 ] ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) ↔ ( [ 1 / 𝑥 ] ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ [ 1 / 𝑥 ] 𝑖 = ( 𝑥 [,) 𝑐 ) ) )
34 simpr ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
35 simpl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → 𝑥 ∈ ℝ )
36 leid ⊢ ( 𝑥 ∈ ℝ → 𝑥 ≤ 𝑥 )
37 35 36 jccir ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ) )
38 rexr ⊢ ( 𝑐 ∈ ℝ → 𝑐 ∈ ℝ* )
39 elico2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑥 [,) 𝑐 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐 ) ) )
40 38 39 sylan2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( 𝑥 ∈ ( 𝑥 [,) 𝑐 ) ↔ ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐 ) ) )
41 df-3an ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ∧ 𝑥 < 𝑐 ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ) ∧ 𝑥 < 𝑐 ) )
42 40 41 bitrdi ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( 𝑥 ∈ ( 𝑥 [,) 𝑐 ) ↔ ( ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ) ∧ 𝑥 < 𝑐 ) ) )
43 42 baibd ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) ∧ ( 𝑥 ∈ ℝ ∧ 𝑥 ≤ 𝑥 ) ) → ( 𝑥 ∈ ( 𝑥 [,) 𝑐 ) ↔ 𝑥 < 𝑐 ) )
44 37 43 mpdan ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( 𝑥 ∈ ( 𝑥 [,) 𝑐 ) ↔ 𝑥 < 𝑐 ) )
45 44 biimpar ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) ∧ 𝑥 < 𝑐 ) → 𝑥 ∈ ( 𝑥 [,) 𝑐 ) )
46 45 adantr ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) → 𝑥 ∈ ( 𝑥 [,) 𝑐 ) )
47 eleq2 ⊢ ( 𝑖 = ( 𝑥 [,) 𝑐 ) → ( 𝑥 ∈ 𝑖 ↔ 𝑥 ∈ ( 𝑥 [,) 𝑐 ) ) )
48 47 adantl ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) → ( 𝑥 ∈ 𝑖 ↔ 𝑥 ∈ ( 𝑥 [,) 𝑐 ) ) )
49 46 48 mpbird ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) → 𝑥 ∈ 𝑖 )
50 rexpssxrxp ⊢ ( ℝ × ℝ ) ⊆ ( ℝ* × ℝ* )
51 opelxpi ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ⟨ 𝑥 , 𝑐 ⟩ ∈ ( ℝ × ℝ ) )
52 50 51 sselid ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ⟨ 𝑥 , 𝑐 ⟩ ∈ ( ℝ* × ℝ* ) )
53 df-ico ⊢ [,) = ( 𝑥 ∈ ℝ* , 𝑐 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑐 ) } )
54 53 ixxf ⊢ [,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
55 54 fdmi ⊢ dom [,) = ( ℝ* × ℝ* )
56 55 eleq2i ⊢ ( ⟨ 𝑥 , 𝑐 ⟩ ∈ dom [,) ↔ ⟨ 𝑥 , 𝑐 ⟩ ∈ ( ℝ* × ℝ* ) )
57 53 mpofun ⊢ Fun [,)
58 funfvima ⊢ ( ( Fun [,) ∧ ⟨ 𝑥 , 𝑐 ⟩ ∈ dom [,) ) → ( ⟨ 𝑥 , 𝑐 ⟩ ∈ ( ℝ × ℝ ) → ( [,) ‘ ⟨ 𝑥 , 𝑐 ⟩ ) ∈ ( [,) “ ( ℝ × ℝ ) ) ) )
59 57 58 mpan ⊢ ( ⟨ 𝑥 , 𝑐 ⟩ ∈ dom [,) → ( ⟨ 𝑥 , 𝑐 ⟩ ∈ ( ℝ × ℝ ) → ( [,) ‘ ⟨ 𝑥 , 𝑐 ⟩ ) ∈ ( [,) “ ( ℝ × ℝ ) ) ) )
60 56 59 sylbir ⊢ ( ⟨ 𝑥 , 𝑐 ⟩ ∈ ( ℝ* × ℝ* ) → ( ⟨ 𝑥 , 𝑐 ⟩ ∈ ( ℝ × ℝ ) → ( [,) ‘ ⟨ 𝑥 , 𝑐 ⟩ ) ∈ ( [,) “ ( ℝ × ℝ ) ) ) )
61 52 51 60 sylc ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( [,) ‘ ⟨ 𝑥 , 𝑐 ⟩ ) ∈ ( [,) “ ( ℝ × ℝ ) ) )
62 df-ov ⊢ ( 𝑥 [,) 𝑐 ) = ( [,) ‘ ⟨ 𝑥 , 𝑐 ⟩ )
63 61 62 1 3eltr4g ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( 𝑥 [,) 𝑐 ) ∈ 𝐼 )
64 eleq1 ⊢ ( 𝑖 = ( 𝑥 [,) 𝑐 ) → ( 𝑖 ∈ 𝐼 ↔ ( 𝑥 [,) 𝑐 ) ∈ 𝐼 ) )
65 63 64 syl5ibrcom ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( 𝑖 = ( 𝑥 [,) 𝑐 ) → 𝑖 ∈ 𝐼 ) )
66 65 imp ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) → 𝑖 ∈ 𝐼 )
67 ioof ⊢ (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ
68 ffn ⊢ ( (,) : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ → (,) Fn ( ℝ* × ℝ* ) )
69 67 68 ax-mp ⊢ (,) Fn ( ℝ* × ℝ* )
70 ovelrn ⊢ ( (,) Fn ( ℝ* × ℝ* ) → ( 𝑜 ∈ ran (,) ↔ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑜 = ( 𝑎 (,) 𝑏 ) ) )
71 69 70 ax-mp ⊢ ( 𝑜 ∈ ran (,) ↔ ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑜 = ( 𝑎 (,) 𝑏 ) )
72 iooelexlt ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ∃ 𝑦 ∈ ( 𝑎 (,) 𝑏 ) 𝑦 < 𝑥 )
73 df-rex ⊢ ( ∃ 𝑦 ∈ ( 𝑎 (,) 𝑏 ) 𝑦 < 𝑥 ↔ ∃ 𝑦 ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑦 < 𝑥 ) )
74 72 73 sylib ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ∃ 𝑦 ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑦 < 𝑥 ) )
75 simpl ⊢ ( ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑦 < 𝑥 ) → 𝑦 ∈ ( 𝑎 (,) 𝑏 ) )
76 75 a1i ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑦 < 𝑥 ) → 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ) )
77 53 elmpocl2 ⊢ ( 𝑦 ∈ ( 𝑥 [,) 𝑐 ) → 𝑐 ∈ ℝ* )
78 elioore ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → 𝑥 ∈ ℝ )
79 elico2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ* ) → ( 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐 ) ) )
80 78 79 sylan ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑐 ∈ ℝ* ) → ( 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐 ) ) )
81 simp2 ⊢ ( ( 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ∧ 𝑦 < 𝑐 ) → 𝑥 ≤ 𝑦 )
82 80 81 syl6bi ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑐 ∈ ℝ* ) → ( 𝑦 ∈ ( 𝑥 [,) 𝑐 ) → 𝑥 ≤ 𝑦 ) )
83 82 ex ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ( 𝑐 ∈ ℝ* → ( 𝑦 ∈ ( 𝑥 [,) 𝑐 ) → 𝑥 ≤ 𝑦 ) ) )
84 83 com23 ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ( 𝑦 ∈ ( 𝑥 [,) 𝑐 ) → ( 𝑐 ∈ ℝ* → 𝑥 ≤ 𝑦 ) ) )
85 77 84 mpdi ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ( 𝑦 ∈ ( 𝑥 [,) 𝑐 ) → 𝑥 ≤ 𝑦 ) )
86 85 imp ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) → 𝑥 ≤ 𝑦 )
87 78 rexrd ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → 𝑥 ∈ ℝ* )
88 87 adantr ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) → 𝑥 ∈ ℝ* )
89 elicore ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) → 𝑦 ∈ ℝ )
90 78 89 sylan ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) → 𝑦 ∈ ℝ )
91 90 rexrd ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) → 𝑦 ∈ ℝ* )
92 xrlenlt ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑥 ) )
93 92 biimpd ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑥 ≤ 𝑦 → ¬ 𝑦 < 𝑥 ) )
94 93 con2d ⊢ ( ( 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ* ) → ( 𝑦 < 𝑥 → ¬ 𝑥 ≤ 𝑦 ) )
95 88 91 94 syl2anc ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) → ( 𝑦 < 𝑥 → ¬ 𝑥 ≤ 𝑦 ) )
96 86 95 mt2d ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) → ¬ 𝑦 < 𝑥 )
97 96 intnand ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) → ¬ ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑦 < 𝑥 ) )
98 97 ex ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ( 𝑦 ∈ ( 𝑥 [,) 𝑐 ) → ¬ ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑦 < 𝑥 ) ) )
99 98 con2d ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑦 < 𝑥 ) → ¬ 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) )
100 76 99 jcad ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑦 < 𝑥 ) → ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ∧ ¬ 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) ) )
101 annim ⊢ ( ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ∧ ¬ 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) ↔ ¬ ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) → 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) )
102 100 101 syl6ib ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ( ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑦 < 𝑥 ) → ¬ ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) → 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) ) )
103 102 eximdv ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ( ∃ 𝑦 ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) ∧ 𝑦 < 𝑥 ) → ∃ 𝑦 ¬ ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) → 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) ) )
104 74 103 mpd ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ∃ 𝑦 ¬ ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) → 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) )
105 exnal ⊢ ( ∃ 𝑦 ¬ ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) → 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) ↔ ¬ ∀ 𝑦 ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) → 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) )
106 104 105 sylib ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ¬ ∀ 𝑦 ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) → 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) )
107 dfss2 ⊢ ( ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑥 [,) 𝑐 ) ↔ ∀ 𝑦 ( 𝑦 ∈ ( 𝑎 (,) 𝑏 ) → 𝑦 ∈ ( 𝑥 [,) 𝑐 ) ) )
108 106 107 sylnibr ⊢ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ¬ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑥 [,) 𝑐 ) )
109 imnan ⊢ ( ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) → ¬ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑥 [,) 𝑐 ) ) ↔ ¬ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑥 [,) 𝑐 ) ) )
110 108 109 mpbi ⊢ ¬ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑥 [,) 𝑐 ) )
111 eleq2 ⊢ ( 𝑜 = ( 𝑎 (,) 𝑏 ) → ( 𝑥 ∈ 𝑜 ↔ 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ) )
112 sseq1 ⊢ ( 𝑜 = ( 𝑎 (,) 𝑏 ) → ( 𝑜 ⊆ ( 𝑥 [,) 𝑐 ) ↔ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑥 [,) 𝑐 ) ) )
113 111 112 anbi12d ⊢ ( 𝑜 = ( 𝑎 (,) 𝑏 ) → ( ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( 𝑥 [,) 𝑐 ) ) ↔ ( 𝑥 ∈ ( 𝑎 (,) 𝑏 ) ∧ ( 𝑎 (,) 𝑏 ) ⊆ ( 𝑥 [,) 𝑐 ) ) ) )
114 110 113 mtbiri ⊢ ( 𝑜 = ( 𝑎 (,) 𝑏 ) → ¬ ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( 𝑥 [,) 𝑐 ) ) )
115 sseq2 ⊢ ( 𝑖 = ( 𝑥 [,) 𝑐 ) → ( 𝑜 ⊆ 𝑖 ↔ 𝑜 ⊆ ( 𝑥 [,) 𝑐 ) ) )
116 115 anbi2d ⊢ ( 𝑖 = ( 𝑥 [,) 𝑐 ) → ( ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ↔ ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( 𝑥 [,) 𝑐 ) ) ) )
117 116 notbid ⊢ ( 𝑖 = ( 𝑥 [,) 𝑐 ) → ( ¬ ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ↔ ¬ ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ ( 𝑥 [,) 𝑐 ) ) ) )
118 114 117 syl5ibrcom ⊢ ( 𝑜 = ( 𝑎 (,) 𝑏 ) → ( 𝑖 = ( 𝑥 [,) 𝑐 ) → ¬ ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
119 118 a1i ⊢ ( ( 𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ* ) → ( 𝑜 = ( 𝑎 (,) 𝑏 ) → ( 𝑖 = ( 𝑥 [,) 𝑐 ) → ¬ ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ) )
120 119 rexlimivv ⊢ ( ∃ 𝑎 ∈ ℝ* ∃ 𝑏 ∈ ℝ* 𝑜 = ( 𝑎 (,) 𝑏 ) → ( 𝑖 = ( 𝑥 [,) 𝑐 ) → ¬ ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
121 71 120 sylbi ⊢ ( 𝑜 ∈ ran (,) → ( 𝑖 = ( 𝑥 [,) 𝑐 ) → ¬ ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
122 121 com12 ⊢ ( 𝑖 = ( 𝑥 [,) 𝑐 ) → ( 𝑜 ∈ ran (,) → ¬ ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
123 122 ralrimiv ⊢ ( 𝑖 = ( 𝑥 [,) 𝑐 ) → ∀ 𝑜 ∈ ran (,) ¬ ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) )
124 ralnex ⊢ ( ∀ 𝑜 ∈ ran (,) ¬ ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ↔ ¬ ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) )
125 123 124 sylib ⊢ ( 𝑖 = ( 𝑥 [,) 𝑐 ) → ¬ ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) )
126 125 adantl ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) → ¬ ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) )
127 66 126 jca ⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) → ( 𝑖 ∈ 𝐼 ∧ ¬ ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
128 127 adantlr ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) → ( 𝑖 ∈ 𝐼 ∧ ¬ ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
129 49 128 jca ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) → ( 𝑥 ∈ 𝑖 ∧ ( 𝑖 ∈ 𝐼 ∧ ¬ ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ) )
130 an12 ⊢ ( ( 𝑥 ∈ 𝑖 ∧ ( 𝑖 ∈ 𝐼 ∧ ¬ ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ) ↔ ( 𝑖 ∈ 𝐼 ∧ ( 𝑥 ∈ 𝑖 ∧ ¬ ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ) )
131 annim ⊢ ( ( 𝑥 ∈ 𝑖 ∧ ¬ ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ↔ ¬ ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
132 131 anbi2i ⊢ ( ( 𝑖 ∈ 𝐼 ∧ ( 𝑥 ∈ 𝑖 ∧ ¬ ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ) ↔ ( 𝑖 ∈ 𝐼 ∧ ¬ ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ) )
133 130 132 bitri ⊢ ( ( 𝑥 ∈ 𝑖 ∧ ( 𝑖 ∈ 𝐼 ∧ ¬ ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ) ↔ ( 𝑖 ∈ 𝐼 ∧ ¬ ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ) )
134 129 133 sylib ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) → ( 𝑖 ∈ 𝐼 ∧ ¬ ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ) )
135 rspe ⊢ ( ( 𝑖 ∈ 𝐼 ∧ ¬ ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ) → ∃ 𝑖 ∈ 𝐼 ¬ ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
136 134 135 syl ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) → ∃ 𝑖 ∈ 𝐼 ¬ ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
137 rexnal ⊢ ( ∃ 𝑖 ∈ 𝐼 ¬ ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ↔ ¬ ∀ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
138 136 137 sylib ⊢ ( ( ( ( 𝑥 ∈ ℝ ∧ 𝑐 ∈ ℝ ) ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) → ¬ ∀ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
139 138 exp41 ⊢ ( 𝑥 ∈ ℝ → ( 𝑐 ∈ ℝ → ( 𝑥 < 𝑐 → ( 𝑖 = ( 𝑥 [,) 𝑐 ) → ¬ ∀ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ) ) ) )
140 139 com4l ⊢ ( 𝑐 ∈ ℝ → ( 𝑥 < 𝑐 → ( 𝑖 = ( 𝑥 [,) 𝑐 ) → ( 𝑥 ∈ ℝ → ¬ ∀ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ) ) ) )
141 140 imp41 ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) ∧ 𝑥 ∈ ℝ ) → ¬ ∀ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
142 rspe ⊢ ( ( 𝑥 ∈ ℝ ∧ ¬ ∀ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ) → ∃ 𝑥 ∈ ℝ ¬ ∀ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
143 34 141 142 syl2anc ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) ∧ 𝑥 ∈ ℝ ) → ∃ 𝑥 ∈ ℝ ¬ ∀ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
144 rexnal ⊢ ( ∃ 𝑥 ∈ ℝ ¬ ∀ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ↔ ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
145 143 144 sylib ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) ∧ 𝑥 ∈ ℝ ) → ¬ ∀ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
146 df-ico ⊢ [,) = ( 𝑚 ∈ ℝ* , 𝑛 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑚 ≤ 𝑧 ∧ 𝑧 < 𝑛 ) } )
147 146 ixxex ⊢ [,) ∈ V
148 imaexg ⊢ ( [,) ∈ V → ( [,) “ ( ℝ × ℝ ) ) ∈ V )
149 147 148 ax-mp ⊢ ( [,) “ ( ℝ × ℝ ) ) ∈ V
150 1 149 eqeltri ⊢ 𝐼 ∈ V
151 1 icoreunrn ⊢ ℝ = ∪ 𝐼
152 unirnioo ⊢ ℝ = ∪ ran (,)
153 151 152 eqtr3i ⊢ ∪ 𝐼 = ∪ ran (,)
154 tgss2 ⊢ ( ( 𝐼 ∈ V ∧ ∪ 𝐼 = ∪ ran (,) ) → ( ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ↔ ∀ 𝑥 ∈ ∪ 𝐼 ∀ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ) )
155 150 153 154 mp2an ⊢ ( ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ↔ ∀ 𝑥 ∈ ∪ 𝐼 ∀ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
156 151 raleqi ⊢ ( ∀ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) ↔ ∀ 𝑥 ∈ ∪ 𝐼 ∀ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
157 155 156 bitr4i ⊢ ( ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ↔ ∀ 𝑥 ∈ ℝ ∀ 𝑖 ∈ 𝐼 ( 𝑥 ∈ 𝑖 → ∃ 𝑜 ∈ ran (,) ( 𝑥 ∈ 𝑜 ∧ 𝑜 ⊆ 𝑖 ) ) )
158 145 157 sylnibr ⊢ ( ( ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) ∧ 𝑥 ∈ ℝ ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) )
159 158 sbcth ⊢ ( 1 ∈ ℝ → [ 1 / 𝑥 ] ( ( ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) ∧ 𝑥 ∈ ℝ ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) )
160 7 159 ax-mp ⊢ [ 1 / 𝑥 ] ( ( ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) ∧ 𝑥 ∈ ℝ ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) )
161 sbcimg ⊢ ( 1 ∈ ℝ → ( [ 1 / 𝑥 ] ( ( ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) ∧ 𝑥 ∈ ℝ ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) ↔ ( [ 1 / 𝑥 ] ( ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) ∧ 𝑥 ∈ ℝ ) → [ 1 / 𝑥 ] ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) ) )
162 7 161 ax-mp ⊢ ( [ 1 / 𝑥 ] ( ( ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) ∧ 𝑥 ∈ ℝ ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) ↔ ( [ 1 / 𝑥 ] ( ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) ∧ 𝑥 ∈ ℝ ) → [ 1 / 𝑥 ] ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) )
163 160 162 mpbi ⊢ ( [ 1 / 𝑥 ] ( ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) ∧ 𝑥 ∈ ℝ ) → [ 1 / 𝑥 ] ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) )
164 sbcel1v ⊢ ( [ 1 / 𝑥 ] 𝑥 ∈ ℝ ↔ 1 ∈ ℝ )
165 7 164 mpbir ⊢ [ 1 / 𝑥 ] 𝑥 ∈ ℝ
166 sbcan ⊢ ( [ 1 / 𝑥 ] ( ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) ∧ 𝑥 ∈ ℝ ) ↔ ( [ 1 / 𝑥 ] ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) ∧ [ 1 / 𝑥 ] 𝑥 ∈ ℝ ) )
167 165 166 mpbiran2 ⊢ ( [ 1 / 𝑥 ] ( ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) ∧ 𝑥 ∈ ℝ ) ↔ [ 1 / 𝑥 ] ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) )
168 sbcg ⊢ ( 1 ∈ ℝ → ( [ 1 / 𝑥 ] ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ↔ ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) )
169 7 168 ax-mp ⊢ ( [ 1 / 𝑥 ] ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ↔ ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) )
170 163 167 169 3imtr3i ⊢ ( [ 1 / 𝑥 ] ( ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ 𝑖 = ( 𝑥 [,) 𝑐 ) ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) )
171 33 170 sylbir ⊢ ( ( [ 1 / 𝑥 ] ( 𝑐 ∈ ℝ ∧ 𝑥 < 𝑐 ) ∧ [ 1 / 𝑥 ] 𝑖 = ( 𝑥 [,) 𝑐 ) ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) )
172 21 32 171 syl2anbr ⊢ ( ( ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ∧ 𝑖 = ( 1 [,) 𝑐 ) ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) )
173 172 sbcth ⊢ ( ( 1 [,) 𝑐 ) ∈ V → [ ( 1 [,) 𝑐 ) / 𝑖 ] ( ( ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ∧ 𝑖 = ( 1 [,) 𝑐 ) ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) )
174 5 173 ax-mp ⊢ [ ( 1 [,) 𝑐 ) / 𝑖 ] ( ( ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ∧ 𝑖 = ( 1 [,) 𝑐 ) ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) )
175 sbcimg ⊢ ( ( 1 [,) 𝑐 ) ∈ V → ( [ ( 1 [,) 𝑐 ) / 𝑖 ] ( ( ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ∧ 𝑖 = ( 1 [,) 𝑐 ) ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) ↔ ( [ ( 1 [,) 𝑐 ) / 𝑖 ] ( ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ∧ 𝑖 = ( 1 [,) 𝑐 ) ) → [ ( 1 [,) 𝑐 ) / 𝑖 ] ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) ) )
176 5 175 ax-mp ⊢ ( [ ( 1 [,) 𝑐 ) / 𝑖 ] ( ( ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ∧ 𝑖 = ( 1 [,) 𝑐 ) ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) ↔ ( [ ( 1 [,) 𝑐 ) / 𝑖 ] ( ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ∧ 𝑖 = ( 1 [,) 𝑐 ) ) → [ ( 1 [,) 𝑐 ) / 𝑖 ] ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) )
177 174 176 mpbi ⊢ ( [ ( 1 [,) 𝑐 ) / 𝑖 ] ( ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ∧ 𝑖 = ( 1 [,) 𝑐 ) ) → [ ( 1 [,) 𝑐 ) / 𝑖 ] ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) )
178 sbcan ⊢ ( [ ( 1 [,) 𝑐 ) / 𝑖 ] ( ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ∧ 𝑖 = ( 1 [,) 𝑐 ) ) ↔ ( [ ( 1 [,) 𝑐 ) / 𝑖 ] ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ∧ [ ( 1 [,) 𝑐 ) / 𝑖 ] 𝑖 = ( 1 [,) 𝑐 ) ) )
179 eqid ⊢ ( 1 [,) 𝑐 ) = ( 1 [,) 𝑐 )
180 eqsbc1 ⊢ ( ( 1 [,) 𝑐 ) ∈ V → ( [ ( 1 [,) 𝑐 ) / 𝑖 ] 𝑖 = ( 1 [,) 𝑐 ) ↔ ( 1 [,) 𝑐 ) = ( 1 [,) 𝑐 ) ) )
181 5 180 ax-mp ⊢ ( [ ( 1 [,) 𝑐 ) / 𝑖 ] 𝑖 = ( 1 [,) 𝑐 ) ↔ ( 1 [,) 𝑐 ) = ( 1 [,) 𝑐 ) )
182 179 181 mpbir ⊢ [ ( 1 [,) 𝑐 ) / 𝑖 ] 𝑖 = ( 1 [,) 𝑐 )
183 sbcg ⊢ ( ( 1 [,) 𝑐 ) ∈ V → ( [ ( 1 [,) 𝑐 ) / 𝑖 ] ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ↔ ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ) )
184 5 183 ax-mp ⊢ ( [ ( 1 [,) 𝑐 ) / 𝑖 ] ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ↔ ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) )
185 184 anbi1i ⊢ ( ( [ ( 1 [,) 𝑐 ) / 𝑖 ] ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ∧ [ ( 1 [,) 𝑐 ) / 𝑖 ] 𝑖 = ( 1 [,) 𝑐 ) ) ↔ ( ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ∧ [ ( 1 [,) 𝑐 ) / 𝑖 ] 𝑖 = ( 1 [,) 𝑐 ) ) )
186 182 185 mpbiran2 ⊢ ( ( [ ( 1 [,) 𝑐 ) / 𝑖 ] ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ∧ [ ( 1 [,) 𝑐 ) / 𝑖 ] 𝑖 = ( 1 [,) 𝑐 ) ) ↔ ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) )
187 178 186 bitri ⊢ ( [ ( 1 [,) 𝑐 ) / 𝑖 ] ( ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ∧ 𝑖 = ( 1 [,) 𝑐 ) ) ↔ ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) )
188 sbcg ⊢ ( ( 1 [,) 𝑐 ) ∈ V → ( [ ( 1 [,) 𝑐 ) / 𝑖 ] ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ↔ ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) )
189 5 188 ax-mp ⊢ ( [ ( 1 [,) 𝑐 ) / 𝑖 ] ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ↔ ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) )
190 177 187 189 3imtr3i ⊢ ( ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) )
191 190 sbcth ⊢ ( 2 ∈ ℝ → [ 2 / 𝑐 ] ( ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) )
192 3 191 ax-mp ⊢ [ 2 / 𝑐 ] ( ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) )
193 sbcimg ⊢ ( 2 ∈ ℝ → ( [ 2 / 𝑐 ] ( ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) ↔ ( [ 2 / 𝑐 ] ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) → [ 2 / 𝑐 ] ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) ) )
194 3 193 ax-mp ⊢ ( [ 2 / 𝑐 ] ( ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) ↔ ( [ 2 / 𝑐 ] ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) → [ 2 / 𝑐 ] ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) )
195 192 194 mpbi ⊢ ( [ 2 / 𝑐 ] ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) → [ 2 / 𝑐 ] ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) )
196 sbcan ⊢ ( [ 2 / 𝑐 ] ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ↔ ( [ 2 / 𝑐 ] 𝑐 ∈ ℝ ∧ [ 2 / 𝑐 ] 1 < 𝑐 ) )
197 sbcel1v ⊢ ( [ 2 / 𝑐 ] 𝑐 ∈ ℝ ↔ 2 ∈ ℝ )
198 sbcbr123 ⊢ ( [ 2 / 𝑐 ] 1 < 𝑐 ↔ ⦋ 2 / 𝑐 ⦌ 1 ⦋ 2 / 𝑐 ⦌ < ⦋ 2 / 𝑐 ⦌ 𝑐 )
199 csbconstg ⊢ ( 2 ∈ ℝ → ⦋ 2 / 𝑐 ⦌ 1 = 1 )
200 3 199 ax-mp ⊢ ⦋ 2 / 𝑐 ⦌ 1 = 1
201 csbvarg ⊢ ( 2 ∈ ℝ → ⦋ 2 / 𝑐 ⦌ 𝑐 = 2 )
202 3 201 ax-mp ⊢ ⦋ 2 / 𝑐 ⦌ 𝑐 = 2
203 200 202 breq12i ⊢ ( ⦋ 2 / 𝑐 ⦌ 1 ⦋ 2 / 𝑐 ⦌ < ⦋ 2 / 𝑐 ⦌ 𝑐 ↔ 1 ⦋ 2 / 𝑐 ⦌ < 2 )
204 csbconstg ⊢ ( 2 ∈ ℝ → ⦋ 2 / 𝑐 ⦌ < = < )
205 3 204 ax-mp ⊢ ⦋ 2 / 𝑐 ⦌ < = <
206 205 breqi ⊢ ( 1 ⦋ 2 / 𝑐 ⦌ < 2 ↔ 1 < 2 )
207 198 203 206 3bitri ⊢ ( [ 2 / 𝑐 ] 1 < 𝑐 ↔ 1 < 2 )
208 197 207 anbi12i ⊢ ( ( [ 2 / 𝑐 ] 𝑐 ∈ ℝ ∧ [ 2 / 𝑐 ] 1 < 𝑐 ) ↔ ( 2 ∈ ℝ ∧ 1 < 2 ) )
209 196 208 bitri ⊢ ( [ 2 / 𝑐 ] ( 𝑐 ∈ ℝ ∧ 1 < 𝑐 ) ↔ ( 2 ∈ ℝ ∧ 1 < 2 ) )
210 sbcg ⊢ ( 2 ∈ ℝ → ( [ 2 / 𝑐 ] ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ↔ ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ) )
211 3 210 ax-mp ⊢ ( [ 2 / 𝑐 ] ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) ↔ ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) )
212 195 209 211 3imtr3i ⊢ ( ( 2 ∈ ℝ ∧ 1 < 2 ) → ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) )
213 3 4 212 mp2an ⊢ ¬ ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) )
214 eqimss ⊢ ( ( topGen ‘ 𝐼 ) = ( topGen ‘ ran (,) ) → ( topGen ‘ 𝐼 ) ⊆ ( topGen ‘ ran (,) ) )
215 213 214 mto ⊢ ¬ ( topGen ‘ 𝐼 ) = ( topGen ‘ ran (,) )
216 215 nesymir ⊢ ( topGen ‘ ran (,) ) ≠ ( topGen ‘ 𝐼 )
217 df-pss ⊢ ( ( topGen ‘ ran (,) ) ⊊ ( topGen ‘ 𝐼 ) ↔ ( ( topGen ‘ ran (,) ) ⊆ ( topGen ‘ 𝐼 ) ∧ ( topGen ‘ ran (,) ) ≠ ( topGen ‘ 𝐼 ) ) )
218 2 216 217 mpbir2an ⊢ ( topGen ‘ ran (,) ) ⊊ ( topGen ‘ 𝐼 )