MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bndth Structured version   Visualization version   GIF version

Theorem bndth 25003
Description: The Boundedness Theorem. A continuous function from a compact topological space to the reals is bounded (above). (Boundedness below is obtained by applying this theorem to -𝐹.) (Contributed by Mario Carneiro, 12-Aug-2014.)
Hypotheses
Ref Expression
bndth.1 𝑋 = 𝐽
bndth.2 𝐾 = (topGen‘ran (,))
bndth.3 (𝜑𝐽 ∈ Comp)
bndth.4 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
Assertion
Ref Expression
bndth (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥)
Distinct variable groups:   𝑥,𝑦,𝐹   𝑦,𝐾   𝜑,𝑥,𝑦   𝑥,𝑋,𝑦   𝑥,𝐽,𝑦
Allowed substitution hint:   𝐾(𝑥)

Proof of Theorem bndth
Dummy variables 𝑣 𝑢 𝑧 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bndth.4 . . . . 5 (𝜑𝐹 ∈ (𝐽 Cn 𝐾))
2 bndth.1 . . . . . 6 𝑋 = 𝐽
3 bndth.2 . . . . . . . 8 𝐾 = (topGen‘ran (,))
4 retopon 24799 . . . . . . . 8 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
53, 4eqeltri 2834 . . . . . . 7 𝐾 ∈ (TopOn‘ℝ)
65toponunii 22937 . . . . . 6 ℝ = 𝐾
72, 6cnf 23269 . . . . 5 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶ℝ)
81, 7syl 17 . . . 4 (𝜑𝐹:𝑋⟶ℝ)
98frnd 6744 . . 3 (𝜑 → ran 𝐹 ⊆ ℝ)
10 unieq 4922 . . . . . . 7 (𝑢 = ((,) “ ({-∞} × ℝ)) → 𝑢 = ((,) “ ({-∞} × ℝ)))
11 imassrn 6090 . . . . . . . . . 10 ((,) “ ({-∞} × ℝ)) ⊆ ran (,)
1211unissi 4920 . . . . . . . . 9 ((,) “ ({-∞} × ℝ)) ⊆ ran (,)
13 unirnioo 13485 . . . . . . . . 9 ℝ = ran (,)
1412, 13sseqtrri 4032 . . . . . . . 8 ((,) “ ({-∞} × ℝ)) ⊆ ℝ
15 id 22 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑥 ∈ ℝ)
16 ltp1 12104 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑥 < (𝑥 + 1))
17 ressxr 11302 . . . . . . . . . . . . 13 ℝ ⊆ ℝ*
18 peano2re 11431 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
1917, 18sselid 3992 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ*)
20 elioomnf 13480 . . . . . . . . . . . 12 ((𝑥 + 1) ∈ ℝ* → (𝑥 ∈ (-∞(,)(𝑥 + 1)) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < (𝑥 + 1))))
2119, 20syl 17 . . . . . . . . . . 11 (𝑥 ∈ ℝ → (𝑥 ∈ (-∞(,)(𝑥 + 1)) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < (𝑥 + 1))))
2215, 16, 21mpbir2and 713 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑥 ∈ (-∞(,)(𝑥 + 1)))
23 df-ov 7433 . . . . . . . . . . 11 (-∞(,)(𝑥 + 1)) = ((,)‘⟨-∞, (𝑥 + 1)⟩)
24 mnfxr 11315 . . . . . . . . . . . . . . 15 -∞ ∈ ℝ*
2524elexi 3500 . . . . . . . . . . . . . 14 -∞ ∈ V
2625snid 4666 . . . . . . . . . . . . 13 -∞ ∈ {-∞}
27 opelxpi 5725 . . . . . . . . . . . . 13 ((-∞ ∈ {-∞} ∧ (𝑥 + 1) ∈ ℝ) → ⟨-∞, (𝑥 + 1)⟩ ∈ ({-∞} × ℝ))
2826, 18, 27sylancr 587 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → ⟨-∞, (𝑥 + 1)⟩ ∈ ({-∞} × ℝ))
29 ioof 13483 . . . . . . . . . . . . . 14 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
30 ffun 6739 . . . . . . . . . . . . . 14 ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → Fun (,))
3129, 30ax-mp 5 . . . . . . . . . . . . 13 Fun (,)
32 snssi 4812 . . . . . . . . . . . . . . . 16 (-∞ ∈ ℝ* → {-∞} ⊆ ℝ*)
3324, 32ax-mp 5 . . . . . . . . . . . . . . 15 {-∞} ⊆ ℝ*
34 xpss12 5703 . . . . . . . . . . . . . . 15 (({-∞} ⊆ ℝ* ∧ ℝ ⊆ ℝ*) → ({-∞} × ℝ) ⊆ (ℝ* × ℝ*))
3533, 17, 34mp2an 692 . . . . . . . . . . . . . 14 ({-∞} × ℝ) ⊆ (ℝ* × ℝ*)
3629fdmi 6747 . . . . . . . . . . . . . 14 dom (,) = (ℝ* × ℝ*)
3735, 36sseqtrri 4032 . . . . . . . . . . . . 13 ({-∞} × ℝ) ⊆ dom (,)
38 funfvima2 7250 . . . . . . . . . . . . 13 ((Fun (,) ∧ ({-∞} × ℝ) ⊆ dom (,)) → (⟨-∞, (𝑥 + 1)⟩ ∈ ({-∞} × ℝ) → ((,)‘⟨-∞, (𝑥 + 1)⟩) ∈ ((,) “ ({-∞} × ℝ))))
3931, 37, 38mp2an 692 . . . . . . . . . . . 12 (⟨-∞, (𝑥 + 1)⟩ ∈ ({-∞} × ℝ) → ((,)‘⟨-∞, (𝑥 + 1)⟩) ∈ ((,) “ ({-∞} × ℝ)))
4028, 39syl 17 . . . . . . . . . . 11 (𝑥 ∈ ℝ → ((,)‘⟨-∞, (𝑥 + 1)⟩) ∈ ((,) “ ({-∞} × ℝ)))
4123, 40eqeltrid 2842 . . . . . . . . . 10 (𝑥 ∈ ℝ → (-∞(,)(𝑥 + 1)) ∈ ((,) “ ({-∞} × ℝ)))
42 elunii 4916 . . . . . . . . . 10 ((𝑥 ∈ (-∞(,)(𝑥 + 1)) ∧ (-∞(,)(𝑥 + 1)) ∈ ((,) “ ({-∞} × ℝ))) → 𝑥 ((,) “ ({-∞} × ℝ)))
4322, 41, 42syl2anc 584 . . . . . . . . 9 (𝑥 ∈ ℝ → 𝑥 ((,) “ ({-∞} × ℝ)))
4443ssriv 3998 . . . . . . . 8 ℝ ⊆ ((,) “ ({-∞} × ℝ))
4514, 44eqssi 4011 . . . . . . 7 ((,) “ ({-∞} × ℝ)) = ℝ
4610, 45eqtrdi 2790 . . . . . 6 (𝑢 = ((,) “ ({-∞} × ℝ)) → 𝑢 = ℝ)
4746sseq2d 4027 . . . . 5 (𝑢 = ((,) “ ({-∞} × ℝ)) → (ran 𝐹 𝑢 ↔ ran 𝐹 ⊆ ℝ))
48 pweq 4618 . . . . . . 7 (𝑢 = ((,) “ ({-∞} × ℝ)) → 𝒫 𝑢 = 𝒫 ((,) “ ({-∞} × ℝ)))
4948ineq1d 4226 . . . . . 6 (𝑢 = ((,) “ ({-∞} × ℝ)) → (𝒫 𝑢 ∩ Fin) = (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin))
5049rexeqdv 3324 . . . . 5 (𝑢 = ((,) “ ({-∞} × ℝ)) → (∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 𝑣 ↔ ∃𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)ran 𝐹 𝑣))
5147, 50imbi12d 344 . . . 4 (𝑢 = ((,) “ ({-∞} × ℝ)) → ((ran 𝐹 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 𝑣) ↔ (ran 𝐹 ⊆ ℝ → ∃𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)ran 𝐹 𝑣)))
52 bndth.3 . . . . . 6 (𝜑𝐽 ∈ Comp)
53 rncmp 23419 . . . . . 6 ((𝐽 ∈ Comp ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐾t ran 𝐹) ∈ Comp)
5452, 1, 53syl2anc 584 . . . . 5 (𝜑 → (𝐾t ran 𝐹) ∈ Comp)
55 retop 24797 . . . . . . 7 (topGen‘ran (,)) ∈ Top
563, 55eqeltri 2834 . . . . . 6 𝐾 ∈ Top
576cmpsub 23423 . . . . . 6 ((𝐾 ∈ Top ∧ ran 𝐹 ⊆ ℝ) → ((𝐾t ran 𝐹) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 𝐾(ran 𝐹 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 𝑣)))
5856, 9, 57sylancr 587 . . . . 5 (𝜑 → ((𝐾t ran 𝐹) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 𝐾(ran 𝐹 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 𝑣)))
5954, 58mpbid 232 . . . 4 (𝜑 → ∀𝑢 ∈ 𝒫 𝐾(ran 𝐹 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 𝑣))
60 retopbas 24796 . . . . . . . . 9 ran (,) ∈ TopBases
61 bastg 22988 . . . . . . . . 9 (ran (,) ∈ TopBases → ran (,) ⊆ (topGen‘ran (,)))
6260, 61ax-mp 5 . . . . . . . 8 ran (,) ⊆ (topGen‘ran (,))
6362, 3sseqtrri 4032 . . . . . . 7 ran (,) ⊆ 𝐾
6411, 63sstri 4004 . . . . . 6 ((,) “ ({-∞} × ℝ)) ⊆ 𝐾
6556, 64elpwi2 5340 . . . . 5 ((,) “ ({-∞} × ℝ)) ∈ 𝒫 𝐾
6665a1i 11 . . . 4 (𝜑 → ((,) “ ({-∞} × ℝ)) ∈ 𝒫 𝐾)
6751, 59, 66rspcdva 3622 . . 3 (𝜑 → (ran 𝐹 ⊆ ℝ → ∃𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)ran 𝐹 𝑣))
689, 67mpd 15 . 2 (𝜑 → ∃𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)ran 𝐹 𝑣)
69 simpr 484 . . . . . . 7 ((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) → 𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin))
70 elin 3978 . . . . . . 7 (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ↔ (𝑣 ∈ 𝒫 ((,) “ ({-∞} × ℝ)) ∧ 𝑣 ∈ Fin))
7169, 70sylib 218 . . . . . 6 ((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) → (𝑣 ∈ 𝒫 ((,) “ ({-∞} × ℝ)) ∧ 𝑣 ∈ Fin))
7271adantrr 717 . . . . 5 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → (𝑣 ∈ 𝒫 ((,) “ ({-∞} × ℝ)) ∧ 𝑣 ∈ Fin))
7372simprd 495 . . . 4 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → 𝑣 ∈ Fin)
7471simpld 494 . . . . . . 7 ((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) → 𝑣 ∈ 𝒫 ((,) “ ({-∞} × ℝ)))
7574elpwid 4613 . . . . . 6 ((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) → 𝑣 ⊆ ((,) “ ({-∞} × ℝ)))
7633sseli 3990 . . . . . . . . . . . 12 (𝑢 ∈ {-∞} → 𝑢 ∈ ℝ*)
7776adantr 480 . . . . . . . . . . 11 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → 𝑢 ∈ ℝ*)
7817sseli 3990 . . . . . . . . . . . 12 (𝑤 ∈ ℝ → 𝑤 ∈ ℝ*)
7978adantl 481 . . . . . . . . . . 11 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℝ*)
80 mnflt 13162 . . . . . . . . . . . . . . 15 (𝑤 ∈ ℝ → -∞ < 𝑤)
81 xrltnle 11325 . . . . . . . . . . . . . . . 16 ((-∞ ∈ ℝ*𝑤 ∈ ℝ*) → (-∞ < 𝑤 ↔ ¬ 𝑤 ≤ -∞))
8224, 78, 81sylancr 587 . . . . . . . . . . . . . . 15 (𝑤 ∈ ℝ → (-∞ < 𝑤 ↔ ¬ 𝑤 ≤ -∞))
8380, 82mpbid 232 . . . . . . . . . . . . . 14 (𝑤 ∈ ℝ → ¬ 𝑤 ≤ -∞)
8483adantl 481 . . . . . . . . . . . . 13 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → ¬ 𝑤 ≤ -∞)
85 elsni 4647 . . . . . . . . . . . . . . 15 (𝑢 ∈ {-∞} → 𝑢 = -∞)
8685adantr 480 . . . . . . . . . . . . . 14 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → 𝑢 = -∞)
8786breq2d 5159 . . . . . . . . . . . . 13 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → (𝑤𝑢𝑤 ≤ -∞))
8884, 87mtbird 325 . . . . . . . . . . . 12 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → ¬ 𝑤𝑢)
89 ioo0 13408 . . . . . . . . . . . . . 14 ((𝑢 ∈ ℝ*𝑤 ∈ ℝ*) → ((𝑢(,)𝑤) = ∅ ↔ 𝑤𝑢))
9076, 78, 89syl2an 596 . . . . . . . . . . . . 13 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → ((𝑢(,)𝑤) = ∅ ↔ 𝑤𝑢))
9190necon3abid 2974 . . . . . . . . . . . 12 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → ((𝑢(,)𝑤) ≠ ∅ ↔ ¬ 𝑤𝑢))
9288, 91mpbird 257 . . . . . . . . . . 11 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → (𝑢(,)𝑤) ≠ ∅)
93 df-ioo 13387 . . . . . . . . . . . 12 (,) = (𝑦 ∈ ℝ*, 𝑧 ∈ ℝ* ↦ {𝑣 ∈ ℝ* ∣ (𝑦 < 𝑣𝑣 < 𝑧)})
94 idd 24 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ*𝑤 ∈ ℝ*) → (𝑥 < 𝑤𝑥 < 𝑤))
95 xrltle 13187 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ*𝑤 ∈ ℝ*) → (𝑥 < 𝑤𝑥𝑤))
96 idd 24 . . . . . . . . . . . 12 ((𝑢 ∈ ℝ*𝑥 ∈ ℝ*) → (𝑢 < 𝑥𝑢 < 𝑥))
97 xrltle 13187 . . . . . . . . . . . 12 ((𝑢 ∈ ℝ*𝑥 ∈ ℝ*) → (𝑢 < 𝑥𝑢𝑥))
9893, 94, 95, 96, 97ixxub 13404 . . . . . . . . . . 11 ((𝑢 ∈ ℝ*𝑤 ∈ ℝ* ∧ (𝑢(,)𝑤) ≠ ∅) → sup((𝑢(,)𝑤), ℝ*, < ) = 𝑤)
9977, 79, 92, 98syl3anc 1370 . . . . . . . . . 10 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → sup((𝑢(,)𝑤), ℝ*, < ) = 𝑤)
100 simpr 484 . . . . . . . . . 10 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℝ)
10199, 100eqeltrd 2838 . . . . . . . . 9 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → sup((𝑢(,)𝑤), ℝ*, < ) ∈ ℝ)
102101rgen2 3196 . . . . . . . 8 𝑢 ∈ {-∞}∀𝑤 ∈ ℝ sup((𝑢(,)𝑤), ℝ*, < ) ∈ ℝ
103 fveq2 6906 . . . . . . . . . . . 12 (𝑧 = ⟨𝑢, 𝑤⟩ → ((,)‘𝑧) = ((,)‘⟨𝑢, 𝑤⟩))
104 df-ov 7433 . . . . . . . . . . . 12 (𝑢(,)𝑤) = ((,)‘⟨𝑢, 𝑤⟩)
105103, 104eqtr4di 2792 . . . . . . . . . . 11 (𝑧 = ⟨𝑢, 𝑤⟩ → ((,)‘𝑧) = (𝑢(,)𝑤))
106105supeq1d 9483 . . . . . . . . . 10 (𝑧 = ⟨𝑢, 𝑤⟩ → sup(((,)‘𝑧), ℝ*, < ) = sup((𝑢(,)𝑤), ℝ*, < ))
107106eleq1d 2823 . . . . . . . . 9 (𝑧 = ⟨𝑢, 𝑤⟩ → (sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ ↔ sup((𝑢(,)𝑤), ℝ*, < ) ∈ ℝ))
108107ralxp 5854 . . . . . . . 8 (∀𝑧 ∈ ({-∞} × ℝ)sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ ↔ ∀𝑢 ∈ {-∞}∀𝑤 ∈ ℝ sup((𝑢(,)𝑤), ℝ*, < ) ∈ ℝ)
109102, 108mpbir 231 . . . . . . 7 𝑧 ∈ ({-∞} × ℝ)sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ
110 ffn 6736 . . . . . . . . 9 ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
11129, 110ax-mp 5 . . . . . . . 8 (,) Fn (ℝ* × ℝ*)
112 supeq1 9482 . . . . . . . . . 10 (𝑤 = ((,)‘𝑧) → sup(𝑤, ℝ*, < ) = sup(((,)‘𝑧), ℝ*, < ))
113112eleq1d 2823 . . . . . . . . 9 (𝑤 = ((,)‘𝑧) → (sup(𝑤, ℝ*, < ) ∈ ℝ ↔ sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ))
114113ralima 7256 . . . . . . . 8 (((,) Fn (ℝ* × ℝ*) ∧ ({-∞} × ℝ) ⊆ (ℝ* × ℝ*)) → (∀𝑤 ∈ ((,) “ ({-∞} × ℝ))sup(𝑤, ℝ*, < ) ∈ ℝ ↔ ∀𝑧 ∈ ({-∞} × ℝ)sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ))
115111, 35, 114mp2an 692 . . . . . . 7 (∀𝑤 ∈ ((,) “ ({-∞} × ℝ))sup(𝑤, ℝ*, < ) ∈ ℝ ↔ ∀𝑧 ∈ ({-∞} × ℝ)sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ)
116109, 115mpbir 231 . . . . . 6 𝑤 ∈ ((,) “ ({-∞} × ℝ))sup(𝑤, ℝ*, < ) ∈ ℝ
117 ssralv 4063 . . . . . 6 (𝑣 ⊆ ((,) “ ({-∞} × ℝ)) → (∀𝑤 ∈ ((,) “ ({-∞} × ℝ))sup(𝑤, ℝ*, < ) ∈ ℝ → ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ∈ ℝ))
11875, 116, 117mpisyl 21 . . . . 5 ((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) → ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ∈ ℝ)
119118adantrr 717 . . . 4 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ∈ ℝ)
120 fimaxre3 12211 . . . 4 ((𝑣 ∈ Fin ∧ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ∈ ℝ) → ∃𝑥 ∈ ℝ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥)
12173, 119, 120syl2anc 584 . . 3 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → ∃𝑥 ∈ ℝ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥)
122 simplrr 778 . . . . . . . 8 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → ran 𝐹 𝑣)
123122sselda 3994 . . . . . . 7 ((((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ran 𝐹) → 𝑧 𝑣)
124 eluni2 4915 . . . . . . . 8 (𝑧 𝑣 ↔ ∃𝑤𝑣 𝑧𝑤)
125 r19.29r 3113 . . . . . . . . . 10 ((∃𝑤𝑣 𝑧𝑤 ∧ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥) → ∃𝑤𝑣 (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥))
126 sspwuni 5104 . . . . . . . . . . . . . . . . . . 19 (((,) “ ({-∞} × ℝ)) ⊆ 𝒫 ℝ ↔ ((,) “ ({-∞} × ℝ)) ⊆ ℝ)
12714, 126mpbir 231 . . . . . . . . . . . . . . . . . 18 ((,) “ ({-∞} × ℝ)) ⊆ 𝒫 ℝ
128753ad2ant1 1132 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑣 ⊆ ((,) “ ({-∞} × ℝ)))
129 simp2r 1199 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤𝑣)
130128, 129sseldd 3995 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤 ∈ ((,) “ ({-∞} × ℝ)))
131127, 130sselid 3992 . . . . . . . . . . . . . . . . 17 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤 ∈ 𝒫 ℝ)
132131elpwid 4613 . . . . . . . . . . . . . . . 16 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤 ⊆ ℝ)
133 simp3l 1200 . . . . . . . . . . . . . . . 16 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑧𝑤)
134132, 133sseldd 3995 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑧 ∈ ℝ)
135118r19.21bi 3248 . . . . . . . . . . . . . . . . 17 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ 𝑤𝑣) → sup(𝑤, ℝ*, < ) ∈ ℝ)
136135adantrl 716 . . . . . . . . . . . . . . . 16 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣)) → sup(𝑤, ℝ*, < ) ∈ ℝ)
1371363adant3 1131 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → sup(𝑤, ℝ*, < ) ∈ ℝ)
138 simp2l 1198 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑥 ∈ ℝ)
139132, 17sstrdi 4007 . . . . . . . . . . . . . . . 16 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤 ⊆ ℝ*)
140 supxrub 13362 . . . . . . . . . . . . . . . 16 ((𝑤 ⊆ ℝ*𝑧𝑤) → 𝑧 ≤ sup(𝑤, ℝ*, < ))
141139, 133, 140syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑧 ≤ sup(𝑤, ℝ*, < ))
142 simp3r 1201 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → sup(𝑤, ℝ*, < ) ≤ 𝑥)
143134, 137, 138, 141, 142letrd 11415 . . . . . . . . . . . . . 14 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑧𝑥)
1441433expia 1120 . . . . . . . . . . . . 13 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣)) → ((𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧𝑥))
145144anassrs 467 . . . . . . . . . . . 12 ((((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ 𝑥 ∈ ℝ) ∧ 𝑤𝑣) → ((𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧𝑥))
146145rexlimdva 3152 . . . . . . . . . . 11 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ 𝑥 ∈ ℝ) → (∃𝑤𝑣 (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧𝑥))
147146adantlrr 721 . . . . . . . . . 10 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → (∃𝑤𝑣 (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧𝑥))
148125, 147syl5 34 . . . . . . . . 9 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → ((∃𝑤𝑣 𝑧𝑤 ∧ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧𝑥))
149148expdimp 452 . . . . . . . 8 ((((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) ∧ ∃𝑤𝑣 𝑧𝑤) → (∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥𝑧𝑥))
150124, 149sylan2b 594 . . . . . . 7 ((((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) ∧ 𝑧 𝑣) → (∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥𝑧𝑥))
151123, 150syldan 591 . . . . . 6 ((((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ran 𝐹) → (∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥𝑧𝑥))
152151ralrimdva 3151 . . . . 5 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → (∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥 → ∀𝑧 ∈ ran 𝐹 𝑧𝑥))
1538ffnd 6737 . . . . . . 7 (𝜑𝐹 Fn 𝑋)
154153ad2antrr 726 . . . . . 6 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn 𝑋)
155 breq1 5150 . . . . . . 7 (𝑧 = (𝐹𝑦) → (𝑧𝑥 ↔ (𝐹𝑦) ≤ 𝑥))
156155ralrn 7107 . . . . . 6 (𝐹 Fn 𝑋 → (∀𝑧 ∈ ran 𝐹 𝑧𝑥 ↔ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
157154, 156syl 17 . . . . 5 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran 𝐹 𝑧𝑥 ↔ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
158152, 157sylibd 239 . . . 4 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → (∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥 → ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
159158reximdva 3165 . . 3 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → (∃𝑥 ∈ ℝ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
160121, 159mpd 15 . 2 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → ∃𝑥 ∈ ℝ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥)
16168, 160rexlimddv 3158 1 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  cin 3961  wss 3962  c0 4338  𝒫 cpw 4604  {csn 4630  cop 4636   cuni 4911   class class class wbr 5147   × cxp 5686  dom cdm 5688  ran crn 5689  cima 5691  Fun wfun 6556   Fn wfn 6557  wf 6558  cfv 6562  (class class class)co 7430  Fincfn 8983  supcsup 9477  cr 11151  1c1 11153   + caddc 11155  -∞cmnf 11290  *cxr 11291   < clt 11292  cle 11293  (,)cioo 13383  t crest 17466  topGenctg 17483  Topctop 22914  TopOnctopon 22931  TopBasesctb 22967   Cn ccn 23247  Compccmp 23409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fi 9448  df-sup 9479  df-inf 9480  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-n0 12524  df-z 12611  df-uz 12876  df-q 12988  df-ioo 13387  df-rest 17468  df-topgen 17489  df-top 22915  df-topon 22932  df-bases 22968  df-cn 23250  df-cmp 23410
This theorem is referenced by:  evth  25004
  Copyright terms: Public domain W3C validator