Users' Mathboxes Mathbox for ML < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  relowlssretop Structured version   Visualization version   GIF version

Theorem relowlssretop 33522
Description: The lower limit topology on the reals is finer than the standard topology. (Contributed by ML, 1-Aug-2020.)
Hypothesis
Ref Expression
relowlssretop.1 𝐼 = ([,) “ (ℝ × ℝ))
Assertion
Ref Expression
relowlssretop (topGen‘ran (,)) ⊆ (topGen‘𝐼)

Proof of Theorem relowlssretop
Dummy variables 𝑎 𝑏 𝑖 𝑜 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ioof 12464 . . . . . 6 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
2 ffn 6206 . . . . . 6 ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
3 ovelrn 6975 . . . . . 6 ((,) Fn (ℝ* × ℝ*) → (𝑜 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏)))
41, 2, 3mp2b 10 . . . . 5 (𝑜 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏))
5 elxr 12143 . . . . . . . . . 10 (𝑏 ∈ ℝ* ↔ (𝑏 ∈ ℝ ∨ 𝑏 = +∞ ∨ 𝑏 = -∞))
6 simpr 479 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ) → 𝑏 ∈ ℝ)
7 elioore 12398 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑎(,)𝑏) → 𝑥 ∈ ℝ)
86, 7anim12ci 592 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ))
9 relowlssretop.1 . . . . . . . . . . . . . . . 16 𝐼 = ([,) “ (ℝ × ℝ))
109icoreelrn 33520 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ) → {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)} ∈ 𝐼)
118, 10syl 17 . . . . . . . . . . . . . 14 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)} ∈ 𝐼)
127adantl 473 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 ∈ ℝ)
137leidd 10786 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (𝑎(,)𝑏) → 𝑥𝑥)
1413adantl 473 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑥𝑥)
156rexrd 10281 . . . . . . . . . . . . . . . . . 18 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ) → 𝑏 ∈ ℝ*)
16 elioo1 12408 . . . . . . . . . . . . . . . . . 18 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) → (𝑥 ∈ (𝑎(,)𝑏) ↔ (𝑥 ∈ ℝ*𝑎 < 𝑥𝑥 < 𝑏)))
1715, 16syldan 488 . . . . . . . . . . . . . . . . 17 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ) → (𝑥 ∈ (𝑎(,)𝑏) ↔ (𝑥 ∈ ℝ*𝑎 < 𝑥𝑥 < 𝑏)))
1817biimpa 502 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ ℝ*𝑎 < 𝑥𝑥 < 𝑏))
1918simp3d 1139 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 < 𝑏)
20 rexr 10277 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ → 𝑥 ∈ ℝ*)
21203anim1i 1156 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ ∧ 𝑥𝑥𝑥 < 𝑏) → (𝑥 ∈ ℝ*𝑥𝑥𝑥 < 𝑏))
22 rexr 10277 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ ℝ → 𝑏 ∈ ℝ*)
23 elico1 12411 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℝ*𝑏 ∈ ℝ*) → (𝑥 ∈ (𝑥[,)𝑏) ↔ (𝑥 ∈ ℝ*𝑥𝑥𝑥 < 𝑏)))
2420, 22, 23syl2an 495 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑥 ∈ (𝑥[,)𝑏) ↔ (𝑥 ∈ ℝ*𝑥𝑥𝑥 < 𝑏)))
2524biimprd 238 . . . . . . . . . . . . . . . . 17 ((𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ) → ((𝑥 ∈ ℝ*𝑥𝑥𝑥 < 𝑏) → 𝑥 ∈ (𝑥[,)𝑏)))
268, 21, 25syl2im 40 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝑥 ∈ ℝ ∧ 𝑥𝑥𝑥 < 𝑏) → 𝑥 ∈ (𝑥[,)𝑏)))
27 icoreval 33512 . . . . . . . . . . . . . . . . . 18 ((𝑥 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑥[,)𝑏) = {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)})
288, 27syl 17 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥[,)𝑏) = {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)})
2928eleq2d 2825 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ (𝑥[,)𝑏) ↔ 𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)}))
3026, 29sylibd 229 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ((𝑥 ∈ ℝ ∧ 𝑥𝑥𝑥 < 𝑏) → 𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)}))
3112, 14, 19, 30mp3and 1576 . . . . . . . . . . . . . 14 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)})
32 nfv 1992 . . . . . . . . . . . . . . . 16 𝑧((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ 𝑥 ∈ (𝑎(,)𝑏))
33 nfrab1 3261 . . . . . . . . . . . . . . . 16 𝑧{𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)}
34 nfcv 2902 . . . . . . . . . . . . . . . 16 𝑧(𝑎(,)𝑏)
35 iooval 12392 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) → (𝑎(,)𝑏) = {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥𝑥 < 𝑏)})
3635eleq2d 2825 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) → (𝑥 ∈ (𝑎(,)𝑏) ↔ 𝑥 ∈ {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥𝑥 < 𝑏)}))
3736anbi1d 743 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) → ((𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)}) ↔ (𝑥 ∈ {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥𝑥 < 𝑏)} ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)})))
3837pm5.32i 672 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)})) ↔ ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑥 ∈ {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥𝑥 < 𝑏)} ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)})))
39 rabid 3254 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥𝑥 < 𝑏)} ↔ (𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥𝑥 < 𝑏)))
40 rabid 3254 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)} ↔ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏)))
4139, 40anbi12i 735 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥𝑥 < 𝑏)} ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)}) ↔ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏))))
42 simpl 474 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏)) → 𝑧 ∈ ℝ)
4342rexrd 10281 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏)) → 𝑧 ∈ ℝ*)
4443ad2antll 767 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ ℝ* ∧ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏)))) → 𝑧 ∈ ℝ*)
45 simpl 474 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥𝑥 < 𝑏)) → 𝑥 ∈ ℝ*)
4645, 43anim12i 591 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏))) → (𝑥 ∈ ℝ*𝑧 ∈ ℝ*))
4746anim2i 594 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ℝ* ∧ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏)))) → (𝑎 ∈ ℝ* ∧ (𝑥 ∈ ℝ*𝑧 ∈ ℝ*)))
48 3anass 1081 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑎 ∈ ℝ*𝑥 ∈ ℝ*𝑧 ∈ ℝ*) ↔ (𝑎 ∈ ℝ* ∧ (𝑥 ∈ ℝ*𝑧 ∈ ℝ*)))
4947, 48sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎 ∈ ℝ* ∧ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏)))) → (𝑎 ∈ ℝ*𝑥 ∈ ℝ*𝑧 ∈ ℝ*))
50 simprl 811 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥𝑥 < 𝑏)) → 𝑎 < 𝑥)
51 simprl 811 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏)) → 𝑥𝑧)
5250, 51anim12i 591 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏))) → (𝑎 < 𝑥𝑥𝑧))
5352adantl 473 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎 ∈ ℝ* ∧ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏)))) → (𝑎 < 𝑥𝑥𝑧))
54 xrltletr 12181 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎 ∈ ℝ*𝑥 ∈ ℝ*𝑧 ∈ ℝ*) → ((𝑎 < 𝑥𝑥𝑧) → 𝑎 < 𝑧))
5549, 53, 54sylc 65 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎 ∈ ℝ* ∧ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏)))) → 𝑎 < 𝑧)
56 simprr 813 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏)) → 𝑧 < 𝑏)
5756ad2antll 767 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎 ∈ ℝ* ∧ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏)))) → 𝑧 < 𝑏)
5855, 57jca 555 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑎 ∈ ℝ* ∧ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏)))) → (𝑎 < 𝑧𝑧 < 𝑏))
59 rabid 3254 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 ∈ {𝑧 ∈ ℝ* ∣ (𝑎 < 𝑧𝑧 < 𝑏)} ↔ (𝑧 ∈ ℝ* ∧ (𝑎 < 𝑧𝑧 < 𝑏)))
6044, 58, 59sylanbrc 701 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ ℝ* ∧ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏)))) → 𝑧 ∈ {𝑧 ∈ ℝ* ∣ (𝑎 < 𝑧𝑧 < 𝑏)})
6160adantlr 753 . . . . . . . . . . . . . . . . . . . 20 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏)))) → 𝑧 ∈ {𝑧 ∈ ℝ* ∣ (𝑎 < 𝑧𝑧 < 𝑏)})
62 iooval 12392 . . . . . . . . . . . . . . . . . . . . 21 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) → (𝑎(,)𝑏) = {𝑧 ∈ ℝ* ∣ (𝑎 < 𝑧𝑧 < 𝑏)})
6362adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏)))) → (𝑎(,)𝑏) = {𝑧 ∈ ℝ* ∣ (𝑎 < 𝑧𝑧 < 𝑏)})
6461, 63eleqtrrd 2842 . . . . . . . . . . . . . . . . . . 19 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ ((𝑥 ∈ ℝ* ∧ (𝑎 < 𝑥𝑥 < 𝑏)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < 𝑏)))) → 𝑧 ∈ (𝑎(,)𝑏))
6541, 64sylan2b 493 . . . . . . . . . . . . . . . . . 18 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑥 ∈ {𝑥 ∈ ℝ* ∣ (𝑎 < 𝑥𝑥 < 𝑏)} ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)})) → 𝑧 ∈ (𝑎(,)𝑏))
6638, 65sylbi 207 . . . . . . . . . . . . . . . . 17 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ (𝑥 ∈ (𝑎(,)𝑏) ∧ 𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)})) → 𝑧 ∈ (𝑎(,)𝑏))
6766expr 644 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)} → 𝑧 ∈ (𝑎(,)𝑏)))
6832, 33, 34, 67ssrd 3749 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)} ⊆ (𝑎(,)𝑏))
6922, 68sylanl2 686 . . . . . . . . . . . . . 14 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)} ⊆ (𝑎(,)𝑏))
70 eleq2 2828 . . . . . . . . . . . . . . . 16 (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)} → (𝑥𝑖𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)}))
71 sseq1 3767 . . . . . . . . . . . . . . . 16 (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)} → (𝑖 ⊆ (𝑎(,)𝑏) ↔ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)} ⊆ (𝑎(,)𝑏)))
7270, 71anbi12d 749 . . . . . . . . . . . . . . 15 (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)} → ((𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏)) ↔ (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)} ∧ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)} ⊆ (𝑎(,)𝑏))))
7372rspcev 3449 . . . . . . . . . . . . . 14 (({𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)} ∈ 𝐼 ∧ (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)} ∧ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < 𝑏)} ⊆ (𝑎(,)𝑏))) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏)))
7411, 31, 69, 73syl12anc 1475 . . . . . . . . . . . . 13 (((𝑎 ∈ ℝ*𝑏 ∈ ℝ) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏)))
7574ancom1s 882 . . . . . . . . . . . 12 (((𝑏 ∈ ℝ ∧ 𝑎 ∈ ℝ*) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏)))
7675expl 649 . . . . . . . . . . 11 (𝑏 ∈ ℝ → ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏))))
777adantl 473 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ℝ*𝑏 = +∞) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 ∈ ℝ)
78 peano2re 10401 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
7977, 78syl 17 . . . . . . . . . . . . . . 15 (((𝑎 ∈ ℝ*𝑏 = +∞) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 + 1) ∈ ℝ)
809icoreelrn 33520 . . . . . . . . . . . . . . 15 ((𝑥 ∈ ℝ ∧ (𝑥 + 1) ∈ ℝ) → {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ∈ 𝐼)
8177, 79, 80syl2anc 696 . . . . . . . . . . . . . 14 (((𝑎 ∈ ℝ*𝑏 = +∞) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ∈ 𝐼)
82 elioore 12398 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (𝑎(,)+∞) → 𝑥 ∈ ℝ)
8382adantl 473 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) → 𝑥 ∈ ℝ)
8483leidd 10786 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) → 𝑥𝑥)
8583ltp1d 11146 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) → 𝑥 < (𝑥 + 1))
8683, 84, 85jca32 559 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) → (𝑥 ∈ ℝ ∧ (𝑥𝑥𝑥 < (𝑥 + 1))))
87 breq2 4808 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑥 → (𝑥𝑧𝑥𝑥))
88 breq1 4807 . . . . . . . . . . . . . . . . . . . . 21 (𝑧 = 𝑥 → (𝑧 < (𝑥 + 1) ↔ 𝑥 < (𝑥 + 1)))
8987, 88anbi12d 749 . . . . . . . . . . . . . . . . . . . 20 (𝑧 = 𝑥 → ((𝑥𝑧𝑧 < (𝑥 + 1)) ↔ (𝑥𝑥𝑥 < (𝑥 + 1))))
9089elrab 3504 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ↔ (𝑥 ∈ ℝ ∧ (𝑥𝑥𝑥 < (𝑥 + 1))))
9186, 90sylibr 224 . . . . . . . . . . . . . . . . . 18 ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) → 𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))})
92 nfv 1992 . . . . . . . . . . . . . . . . . . 19 𝑧(𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞))
93 nfrab1 3261 . . . . . . . . . . . . . . . . . . 19 𝑧{𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))}
94 nfcv 2902 . . . . . . . . . . . . . . . . . . 19 𝑧(𝑎(,)+∞)
95 rabid 3254 . . . . . . . . . . . . . . . . . . . 20 (𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ↔ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < (𝑥 + 1))))
96 simprl 811 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < (𝑥 + 1)))) → 𝑧 ∈ ℝ)
97 simpll 807 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < (𝑥 + 1)))) → 𝑎 ∈ ℝ*)
9883adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < (𝑥 + 1)))) → 𝑥 ∈ ℝ)
9998rexrd 10281 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < (𝑥 + 1)))) → 𝑥 ∈ ℝ*)
10096rexrd 10281 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < (𝑥 + 1)))) → 𝑧 ∈ ℝ*)
101 elioopnf 12460 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ ℝ* → (𝑥 ∈ (𝑎(,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝑎 < 𝑥)))
102101simplbda 655 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) → 𝑎 < 𝑥)
103102adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < (𝑥 + 1)))) → 𝑎 < 𝑥)
104 simprl 811 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < (𝑥 + 1))) → 𝑥𝑧)
105104adantl 473 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < (𝑥 + 1)))) → 𝑥𝑧)
10697, 99, 100, 103, 105xrltletrd 12185 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < (𝑥 + 1)))) → 𝑎 < 𝑧)
107 elioopnf 12460 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑎 ∈ ℝ* → (𝑧 ∈ (𝑎(,)+∞) ↔ (𝑧 ∈ ℝ ∧ 𝑎 < 𝑧)))
108107biimprd 238 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 ∈ ℝ* → ((𝑧 ∈ ℝ ∧ 𝑎 < 𝑧) → 𝑧 ∈ (𝑎(,)+∞)))
109108adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) → ((𝑧 ∈ ℝ ∧ 𝑎 < 𝑧) → 𝑧 ∈ (𝑎(,)+∞)))
110109adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < (𝑥 + 1)))) → ((𝑧 ∈ ℝ ∧ 𝑎 < 𝑧) → 𝑧 ∈ (𝑎(,)+∞)))
11196, 106, 110mp2and 717 . . . . . . . . . . . . . . . . . . . . 21 (((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) ∧ (𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < (𝑥 + 1)))) → 𝑧 ∈ (𝑎(,)+∞))
112111ex 449 . . . . . . . . . . . . . . . . . . . 20 ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) → ((𝑧 ∈ ℝ ∧ (𝑥𝑧𝑧 < (𝑥 + 1))) → 𝑧 ∈ (𝑎(,)+∞)))
11395, 112syl5bi 232 . . . . . . . . . . . . . . . . . . 19 ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) → (𝑧 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} → 𝑧 ∈ (𝑎(,)+∞)))
11492, 93, 94, 113ssrd 3749 . . . . . . . . . . . . . . . . . 18 ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) → {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)+∞))
11591, 114jca 555 . . . . . . . . . . . . . . . . 17 ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)+∞)))
116 oveq2 6821 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = +∞ → (𝑎(,)𝑏) = (𝑎(,)+∞))
117116eleq2d 2825 . . . . . . . . . . . . . . . . . . 19 (𝑏 = +∞ → (𝑥 ∈ (𝑎(,)𝑏) ↔ 𝑥 ∈ (𝑎(,)+∞)))
118117anbi2d 742 . . . . . . . . . . . . . . . . . 18 (𝑏 = +∞ → ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)𝑏)) ↔ (𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞))))
119116sseq2d 3774 . . . . . . . . . . . . . . . . . . 19 (𝑏 = +∞ → ({𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏) ↔ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)+∞)))
120119anbi2d 742 . . . . . . . . . . . . . . . . . 18 (𝑏 = +∞ → ((𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏)) ↔ (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)+∞))))
121118, 120imbi12d 333 . . . . . . . . . . . . . . . . 17 (𝑏 = +∞ → (((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏))) ↔ ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)+∞)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)+∞)))))
122115, 121mpbiri 248 . . . . . . . . . . . . . . . 16 (𝑏 = +∞ → ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏))))
123122impl 651 . . . . . . . . . . . . . . 15 (((𝑏 = +∞ ∧ 𝑎 ∈ ℝ*) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏)))
124123ancom1s 882 . . . . . . . . . . . . . 14 (((𝑎 ∈ ℝ*𝑏 = +∞) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏)))
125 eleq2 2828 . . . . . . . . . . . . . . . 16 (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} → (𝑥𝑖𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))}))
126 sseq1 3767 . . . . . . . . . . . . . . . 16 (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} → (𝑖 ⊆ (𝑎(,)𝑏) ↔ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏)))
127125, 126anbi12d 749 . . . . . . . . . . . . . . 15 (𝑖 = {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} → ((𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏)) ↔ (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏))))
128127rspcev 3449 . . . . . . . . . . . . . 14 (({𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ∈ 𝐼 ∧ (𝑥 ∈ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ∧ {𝑧 ∈ ℝ ∣ (𝑥𝑧𝑧 < (𝑥 + 1))} ⊆ (𝑎(,)𝑏))) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏)))
12981, 124, 128syl2anc 696 . . . . . . . . . . . . 13 (((𝑎 ∈ ℝ*𝑏 = +∞) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏)))
130129ancom1s 882 . . . . . . . . . . . 12 (((𝑏 = +∞ ∧ 𝑎 ∈ ℝ*) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏)))
131130expl 649 . . . . . . . . . . 11 (𝑏 = +∞ → ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏))))
1327adantl 473 . . . . . . . . . . . . . 14 (((𝑎 ∈ ℝ*𝑏 = -∞) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → 𝑥 ∈ ℝ)
133 oveq2 6821 . . . . . . . . . . . . . . . . . . 19 (𝑏 = -∞ → (𝑎(,)𝑏) = (𝑎(,)-∞))
134133eleq2d 2825 . . . . . . . . . . . . . . . . . 18 (𝑏 = -∞ → (𝑥 ∈ (𝑎(,)𝑏) ↔ 𝑥 ∈ (𝑎(,)-∞)))
135134adantl 473 . . . . . . . . . . . . . . . . 17 ((𝑎 ∈ ℝ*𝑏 = -∞) → (𝑥 ∈ (𝑎(,)𝑏) ↔ 𝑥 ∈ (𝑎(,)-∞)))
136135pm5.32i 672 . . . . . . . . . . . . . . . 16 (((𝑎 ∈ ℝ*𝑏 = -∞) ∧ 𝑥 ∈ (𝑎(,)𝑏)) ↔ ((𝑎 ∈ ℝ*𝑏 = -∞) ∧ 𝑥 ∈ (𝑎(,)-∞)))
137 nltmnf 12156 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ℝ* → ¬ 𝑥 < -∞)
138137intnand 1000 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ ℝ* → ¬ (𝑎 < 𝑥𝑥 < -∞))
139 eliooord 12426 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (𝑎(,)-∞) → (𝑎 < 𝑥𝑥 < -∞))
140138, 139nsyl 135 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ ℝ* → ¬ 𝑥 ∈ (𝑎(,)-∞))
141140pm2.21d 118 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℝ* → (𝑥 ∈ (𝑎(,)-∞) → ((𝑎 ∈ ℝ*𝑏 = -∞) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏)))))
142141impd 446 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℝ* → ((𝑥 ∈ (𝑎(,)-∞) ∧ (𝑎 ∈ ℝ*𝑏 = -∞)) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏))))
143142ancomsd 469 . . . . . . . . . . . . . . . 16 (𝑥 ∈ ℝ* → (((𝑎 ∈ ℝ*𝑏 = -∞) ∧ 𝑥 ∈ (𝑎(,)-∞)) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏))))
144136, 143syl5bi 232 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ* → (((𝑎 ∈ ℝ*𝑏 = -∞) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏))))
14520, 144syl 17 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (((𝑎 ∈ ℝ*𝑏 = -∞) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏))))
146132, 145mpcom 38 . . . . . . . . . . . . 13 (((𝑎 ∈ ℝ*𝑏 = -∞) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏)))
147146ancom1s 882 . . . . . . . . . . . 12 (((𝑏 = -∞ ∧ 𝑎 ∈ ℝ*) ∧ 𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏)))
148147expl 649 . . . . . . . . . . 11 (𝑏 = -∞ → ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏))))
14976, 131, 1483jaoi 1540 . . . . . . . . . 10 ((𝑏 ∈ ℝ ∨ 𝑏 = +∞ ∨ 𝑏 = -∞) → ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏))))
1505, 149sylbi 207 . . . . . . . . 9 (𝑏 ∈ ℝ* → ((𝑎 ∈ ℝ*𝑥 ∈ (𝑎(,)𝑏)) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏))))
151150expdimp 452 . . . . . . . 8 ((𝑏 ∈ ℝ*𝑎 ∈ ℝ*) → (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏))))
152151ancoms 468 . . . . . . 7 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) → (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏))))
153 eleq2 2828 . . . . . . . 8 (𝑜 = (𝑎(,)𝑏) → (𝑥𝑜𝑥 ∈ (𝑎(,)𝑏)))
154 sseq2 3768 . . . . . . . . . 10 (𝑜 = (𝑎(,)𝑏) → (𝑖𝑜𝑖 ⊆ (𝑎(,)𝑏)))
155154anbi2d 742 . . . . . . . . 9 (𝑜 = (𝑎(,)𝑏) → ((𝑥𝑖𝑖𝑜) ↔ (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏))))
156155rexbidv 3190 . . . . . . . 8 (𝑜 = (𝑎(,)𝑏) → (∃𝑖𝐼 (𝑥𝑖𝑖𝑜) ↔ ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏))))
157153, 156imbi12d 333 . . . . . . 7 (𝑜 = (𝑎(,)𝑏) → ((𝑥𝑜 → ∃𝑖𝐼 (𝑥𝑖𝑖𝑜)) ↔ (𝑥 ∈ (𝑎(,)𝑏) → ∃𝑖𝐼 (𝑥𝑖𝑖 ⊆ (𝑎(,)𝑏)))))
158152, 157syl5ibrcom 237 . . . . . 6 ((𝑎 ∈ ℝ*𝑏 ∈ ℝ*) → (𝑜 = (𝑎(,)𝑏) → (𝑥𝑜 → ∃𝑖𝐼 (𝑥𝑖𝑖𝑜))))
159158rexlimivv 3174 . . . . 5 (∃𝑎 ∈ ℝ*𝑏 ∈ ℝ* 𝑜 = (𝑎(,)𝑏) → (𝑥𝑜 → ∃𝑖𝐼 (𝑥𝑖𝑖𝑜)))
1604, 159sylbi 207 . . . 4 (𝑜 ∈ ran (,) → (𝑥𝑜 → ∃𝑖𝐼 (𝑥𝑖𝑖𝑜)))
161160rgen 3060 . . 3 𝑜 ∈ ran (,)(𝑥𝑜 → ∃𝑖𝐼 (𝑥𝑖𝑖𝑜))
162161rgenw 3062 . 2 𝑥 ∈ ℝ ∀𝑜 ∈ ran (,)(𝑥𝑜 → ∃𝑖𝐼 (𝑥𝑖𝑖𝑜))
163 iooex 12391 . . . . 5 (,) ∈ V
164163rnex 7265 . . . 4 ran (,) ∈ V
165 unirnioo 12466 . . . . 5 ℝ = ran (,)
1669icoreunrn 33518 . . . . 5 ℝ = 𝐼
167165, 166eqtr3i 2784 . . . 4 ran (,) = 𝐼
168 tgss2 20993 . . . 4 ((ran (,) ∈ V ∧ ran (,) = 𝐼) → ((topGen‘ran (,)) ⊆ (topGen‘𝐼) ↔ ∀𝑥 ran (,)∀𝑜 ∈ ran (,)(𝑥𝑜 → ∃𝑖𝐼 (𝑥𝑖𝑖𝑜))))
169164, 167, 168mp2an 710 . . 3 ((topGen‘ran (,)) ⊆ (topGen‘𝐼) ↔ ∀𝑥 ran (,)∀𝑜 ∈ ran (,)(𝑥𝑜 → ∃𝑖𝐼 (𝑥𝑖𝑖𝑜)))
170165raleqi 3281 . . 3 (∀𝑥 ∈ ℝ ∀𝑜 ∈ ran (,)(𝑥𝑜 → ∃𝑖𝐼 (𝑥𝑖𝑖𝑜)) ↔ ∀𝑥 ran (,)∀𝑜 ∈ ran (,)(𝑥𝑜 → ∃𝑖𝐼 (𝑥𝑖𝑖𝑜)))
171169, 170bitr4i 267 . 2 ((topGen‘ran (,)) ⊆ (topGen‘𝐼) ↔ ∀𝑥 ∈ ℝ ∀𝑜 ∈ ran (,)(𝑥𝑜 → ∃𝑖𝐼 (𝑥𝑖𝑖𝑜)))
172162, 171mpbir 221 1 (topGen‘ran (,)) ⊆ (topGen‘𝐼)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3o 1071  w3a 1072   = wceq 1632  wcel 2139  wral 3050  wrex 3051  {crab 3054  Vcvv 3340  wss 3715  𝒫 cpw 4302   cuni 4588   class class class wbr 4804   × cxp 5264  ran crn 5267  cima 5269   Fn wfn 6044  wf 6045  cfv 6049  (class class class)co 6813  cr 10127  1c1 10129   + caddc 10131  +∞cpnf 10263  -∞cmnf 10264  *cxr 10265   < clt 10266  cle 10267  (,)cioo 12368  [,)cico 12370  topGenctg 16300
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-po 5187  df-so 5188  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-1st 7333  df-2nd 7334  df-er 7911  df-en 8122  df-dom 8123  df-sdom 8124  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-ioo 12372  df-ico 12374  df-topgen 16306
This theorem is referenced by:  relowlpssretop  33523
  Copyright terms: Public domain W3C validator