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

Theorem bndth 22958
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 22768 . . . . . . . 8 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
53, 4eqeltri 2835 . . . . . . 7 𝐾 ∈ (TopOn‘ℝ)
65toponunii 20923 . . . . . 6 ℝ = 𝐾
72, 6cnf 21252 . . . . 5 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶ℝ)
81, 7syl 17 . . . 4 (𝜑𝐹:𝑋⟶ℝ)
9 frn 6214 . . . 4 (𝐹:𝑋⟶ℝ → ran 𝐹 ⊆ ℝ)
108, 9syl 17 . . 3 (𝜑 → ran 𝐹 ⊆ ℝ)
11 unieq 4596 . . . . . . 7 (𝑢 = ((,) “ ({-∞} × ℝ)) → 𝑢 = ((,) “ ({-∞} × ℝ)))
12 imassrn 5635 . . . . . . . . . 10 ((,) “ ({-∞} × ℝ)) ⊆ ran (,)
1312unissi 4613 . . . . . . . . 9 ((,) “ ({-∞} × ℝ)) ⊆ ran (,)
14 unirnioo 12466 . . . . . . . . 9 ℝ = ran (,)
1513, 14sseqtr4i 3779 . . . . . . . 8 ((,) “ ({-∞} × ℝ)) ⊆ ℝ
16 id 22 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑥 ∈ ℝ)
17 ltp1 11053 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑥 < (𝑥 + 1))
18 ressxr 10275 . . . . . . . . . . . . 13 ℝ ⊆ ℝ*
19 peano2re 10401 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
2018, 19sseldi 3742 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ*)
21 elioomnf 12461 . . . . . . . . . . . 12 ((𝑥 + 1) ∈ ℝ* → (𝑥 ∈ (-∞(,)(𝑥 + 1)) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < (𝑥 + 1))))
2220, 21syl 17 . . . . . . . . . . 11 (𝑥 ∈ ℝ → (𝑥 ∈ (-∞(,)(𝑥 + 1)) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < (𝑥 + 1))))
2316, 17, 22mpbir2and 995 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑥 ∈ (-∞(,)(𝑥 + 1)))
24 df-ov 6816 . . . . . . . . . . 11 (-∞(,)(𝑥 + 1)) = ((,)‘⟨-∞, (𝑥 + 1)⟩)
25 mnfxr 10288 . . . . . . . . . . . . . . 15 -∞ ∈ ℝ*
2625elexi 3353 . . . . . . . . . . . . . 14 -∞ ∈ V
2726snid 4353 . . . . . . . . . . . . 13 -∞ ∈ {-∞}
28 opelxpi 5305 . . . . . . . . . . . . 13 ((-∞ ∈ {-∞} ∧ (𝑥 + 1) ∈ ℝ) → ⟨-∞, (𝑥 + 1)⟩ ∈ ({-∞} × ℝ))
2927, 19, 28sylancr 698 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → ⟨-∞, (𝑥 + 1)⟩ ∈ ({-∞} × ℝ))
30 ioof 12464 . . . . . . . . . . . . . 14 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
31 ffun 6209 . . . . . . . . . . . . . 14 ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → Fun (,))
3230, 31ax-mp 5 . . . . . . . . . . . . 13 Fun (,)
33 snssi 4484 . . . . . . . . . . . . . . . 16 (-∞ ∈ ℝ* → {-∞} ⊆ ℝ*)
3425, 33ax-mp 5 . . . . . . . . . . . . . . 15 {-∞} ⊆ ℝ*
35 xpss12 5281 . . . . . . . . . . . . . . 15 (({-∞} ⊆ ℝ* ∧ ℝ ⊆ ℝ*) → ({-∞} × ℝ) ⊆ (ℝ* × ℝ*))
3634, 18, 35mp2an 710 . . . . . . . . . . . . . 14 ({-∞} × ℝ) ⊆ (ℝ* × ℝ*)
3730fdmi 6213 . . . . . . . . . . . . . 14 dom (,) = (ℝ* × ℝ*)
3836, 37sseqtr4i 3779 . . . . . . . . . . . . 13 ({-∞} × ℝ) ⊆ dom (,)
39 funfvima2 6656 . . . . . . . . . . . . 13 ((Fun (,) ∧ ({-∞} × ℝ) ⊆ dom (,)) → (⟨-∞, (𝑥 + 1)⟩ ∈ ({-∞} × ℝ) → ((,)‘⟨-∞, (𝑥 + 1)⟩) ∈ ((,) “ ({-∞} × ℝ))))
4032, 38, 39mp2an 710 . . . . . . . . . . . 12 (⟨-∞, (𝑥 + 1)⟩ ∈ ({-∞} × ℝ) → ((,)‘⟨-∞, (𝑥 + 1)⟩) ∈ ((,) “ ({-∞} × ℝ)))
4129, 40syl 17 . . . . . . . . . . 11 (𝑥 ∈ ℝ → ((,)‘⟨-∞, (𝑥 + 1)⟩) ∈ ((,) “ ({-∞} × ℝ)))
4224, 41syl5eqel 2843 . . . . . . . . . 10 (𝑥 ∈ ℝ → (-∞(,)(𝑥 + 1)) ∈ ((,) “ ({-∞} × ℝ)))
43 elunii 4593 . . . . . . . . . 10 ((𝑥 ∈ (-∞(,)(𝑥 + 1)) ∧ (-∞(,)(𝑥 + 1)) ∈ ((,) “ ({-∞} × ℝ))) → 𝑥 ((,) “ ({-∞} × ℝ)))
4423, 42, 43syl2anc 696 . . . . . . . . 9 (𝑥 ∈ ℝ → 𝑥 ((,) “ ({-∞} × ℝ)))
4544ssriv 3748 . . . . . . . 8 ℝ ⊆ ((,) “ ({-∞} × ℝ))
4615, 45eqssi 3760 . . . . . . 7 ((,) “ ({-∞} × ℝ)) = ℝ
4711, 46syl6eq 2810 . . . . . 6 (𝑢 = ((,) “ ({-∞} × ℝ)) → 𝑢 = ℝ)
4847sseq2d 3774 . . . . 5 (𝑢 = ((,) “ ({-∞} × ℝ)) → (ran 𝐹 𝑢 ↔ ran 𝐹 ⊆ ℝ))
49 pweq 4305 . . . . . . 7 (𝑢 = ((,) “ ({-∞} × ℝ)) → 𝒫 𝑢 = 𝒫 ((,) “ ({-∞} × ℝ)))
5049ineq1d 3956 . . . . . 6 (𝑢 = ((,) “ ({-∞} × ℝ)) → (𝒫 𝑢 ∩ Fin) = (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin))
5150rexeqdv 3284 . . . . 5 (𝑢 = ((,) “ ({-∞} × ℝ)) → (∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 𝑣 ↔ ∃𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)ran 𝐹 𝑣))
5248, 51imbi12d 333 . . . 4 (𝑢 = ((,) “ ({-∞} × ℝ)) → ((ran 𝐹 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 𝑣) ↔ (ran 𝐹 ⊆ ℝ → ∃𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)ran 𝐹 𝑣)))
53 bndth.3 . . . . . 6 (𝜑𝐽 ∈ Comp)
54 rncmp 21401 . . . . . 6 ((𝐽 ∈ Comp ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐾t ran 𝐹) ∈ Comp)
5553, 1, 54syl2anc 696 . . . . 5 (𝜑 → (𝐾t ran 𝐹) ∈ Comp)
56 retop 22766 . . . . . . 7 (topGen‘ran (,)) ∈ Top
573, 56eqeltri 2835 . . . . . 6 𝐾 ∈ Top
586cmpsub 21405 . . . . . 6 ((𝐾 ∈ Top ∧ ran 𝐹 ⊆ ℝ) → ((𝐾t ran 𝐹) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 𝐾(ran 𝐹 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 𝑣)))
5957, 10, 58sylancr 698 . . . . 5 (𝜑 → ((𝐾t ran 𝐹) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 𝐾(ran 𝐹 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 𝑣)))
6055, 59mpbid 222 . . . 4 (𝜑 → ∀𝑢 ∈ 𝒫 𝐾(ran 𝐹 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 𝑣))
61 retopbas 22765 . . . . . . . . 9 ran (,) ∈ TopBases
62 bastg 20972 . . . . . . . . 9 (ran (,) ∈ TopBases → ran (,) ⊆ (topGen‘ran (,)))
6361, 62ax-mp 5 . . . . . . . 8 ran (,) ⊆ (topGen‘ran (,))
6463, 3sseqtr4i 3779 . . . . . . 7 ran (,) ⊆ 𝐾
6512, 64sstri 3753 . . . . . 6 ((,) “ ({-∞} × ℝ)) ⊆ 𝐾
6657elexi 3353 . . . . . . 7 𝐾 ∈ V
6766elpw2 4977 . . . . . 6 (((,) “ ({-∞} × ℝ)) ∈ 𝒫 𝐾 ↔ ((,) “ ({-∞} × ℝ)) ⊆ 𝐾)
6865, 67mpbir 221 . . . . 5 ((,) “ ({-∞} × ℝ)) ∈ 𝒫 𝐾
6968a1i 11 . . . 4 (𝜑 → ((,) “ ({-∞} × ℝ)) ∈ 𝒫 𝐾)
7052, 60, 69rspcdva 3455 . . 3 (𝜑 → (ran 𝐹 ⊆ ℝ → ∃𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)ran 𝐹 𝑣))
7110, 70mpd 15 . 2 (𝜑 → ∃𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)ran 𝐹 𝑣)
72 simpr 479 . . . . . . 7 ((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) → 𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin))
73 elin 3939 . . . . . . 7 (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ↔ (𝑣 ∈ 𝒫 ((,) “ ({-∞} × ℝ)) ∧ 𝑣 ∈ Fin))
7472, 73sylib 208 . . . . . 6 ((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) → (𝑣 ∈ 𝒫 ((,) “ ({-∞} × ℝ)) ∧ 𝑣 ∈ Fin))
7574adantrr 755 . . . . 5 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → (𝑣 ∈ 𝒫 ((,) “ ({-∞} × ℝ)) ∧ 𝑣 ∈ Fin))
7675simprd 482 . . . 4 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → 𝑣 ∈ Fin)
7774simpld 477 . . . . . . 7 ((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) → 𝑣 ∈ 𝒫 ((,) “ ({-∞} × ℝ)))
7877elpwid 4314 . . . . . 6 ((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) → 𝑣 ⊆ ((,) “ ({-∞} × ℝ)))
7934sseli 3740 . . . . . . . . . . . 12 (𝑢 ∈ {-∞} → 𝑢 ∈ ℝ*)
8079adantr 472 . . . . . . . . . . 11 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → 𝑢 ∈ ℝ*)
8118sseli 3740 . . . . . . . . . . . 12 (𝑤 ∈ ℝ → 𝑤 ∈ ℝ*)
8281adantl 473 . . . . . . . . . . 11 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℝ*)
83 mnflt 12150 . . . . . . . . . . . . . . 15 (𝑤 ∈ ℝ → -∞ < 𝑤)
84 xrltnle 10297 . . . . . . . . . . . . . . . 16 ((-∞ ∈ ℝ*𝑤 ∈ ℝ*) → (-∞ < 𝑤 ↔ ¬ 𝑤 ≤ -∞))
8525, 81, 84sylancr 698 . . . . . . . . . . . . . . 15 (𝑤 ∈ ℝ → (-∞ < 𝑤 ↔ ¬ 𝑤 ≤ -∞))
8683, 85mpbid 222 . . . . . . . . . . . . . 14 (𝑤 ∈ ℝ → ¬ 𝑤 ≤ -∞)
8786adantl 473 . . . . . . . . . . . . 13 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → ¬ 𝑤 ≤ -∞)
88 elsni 4338 . . . . . . . . . . . . . . 15 (𝑢 ∈ {-∞} → 𝑢 = -∞)
8988adantr 472 . . . . . . . . . . . . . 14 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → 𝑢 = -∞)
9089breq2d 4816 . . . . . . . . . . . . 13 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → (𝑤𝑢𝑤 ≤ -∞))
9187, 90mtbird 314 . . . . . . . . . . . 12 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → ¬ 𝑤𝑢)
92 ioo0 12393 . . . . . . . . . . . . . 14 ((𝑢 ∈ ℝ*𝑤 ∈ ℝ*) → ((𝑢(,)𝑤) = ∅ ↔ 𝑤𝑢))
9379, 81, 92syl2an 495 . . . . . . . . . . . . 13 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → ((𝑢(,)𝑤) = ∅ ↔ 𝑤𝑢))
9493necon3abid 2968 . . . . . . . . . . . 12 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → ((𝑢(,)𝑤) ≠ ∅ ↔ ¬ 𝑤𝑢))
9591, 94mpbird 247 . . . . . . . . . . 11 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → (𝑢(,)𝑤) ≠ ∅)
96 df-ioo 12372 . . . . . . . . . . . 12 (,) = (𝑦 ∈ ℝ*, 𝑧 ∈ ℝ* ↦ {𝑣 ∈ ℝ* ∣ (𝑦 < 𝑣𝑣 < 𝑧)})
97 idd 24 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ*𝑤 ∈ ℝ*) → (𝑥 < 𝑤𝑥 < 𝑤))
98 xrltle 12175 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ*𝑤 ∈ ℝ*) → (𝑥 < 𝑤𝑥𝑤))
99 idd 24 . . . . . . . . . . . 12 ((𝑢 ∈ ℝ*𝑥 ∈ ℝ*) → (𝑢 < 𝑥𝑢 < 𝑥))
100 xrltle 12175 . . . . . . . . . . . 12 ((𝑢 ∈ ℝ*𝑥 ∈ ℝ*) → (𝑢 < 𝑥𝑢𝑥))
10196, 97, 98, 99, 100ixxub 12389 . . . . . . . . . . 11 ((𝑢 ∈ ℝ*𝑤 ∈ ℝ* ∧ (𝑢(,)𝑤) ≠ ∅) → sup((𝑢(,)𝑤), ℝ*, < ) = 𝑤)
10280, 82, 95, 101syl3anc 1477 . . . . . . . . . 10 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → sup((𝑢(,)𝑤), ℝ*, < ) = 𝑤)
103 simpr 479 . . . . . . . . . 10 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℝ)
104102, 103eqeltrd 2839 . . . . . . . . 9 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → sup((𝑢(,)𝑤), ℝ*, < ) ∈ ℝ)
105104rgen2 3113 . . . . . . . 8 𝑢 ∈ {-∞}∀𝑤 ∈ ℝ sup((𝑢(,)𝑤), ℝ*, < ) ∈ ℝ
106 fveq2 6352 . . . . . . . . . . . 12 (𝑧 = ⟨𝑢, 𝑤⟩ → ((,)‘𝑧) = ((,)‘⟨𝑢, 𝑤⟩))
107 df-ov 6816 . . . . . . . . . . . 12 (𝑢(,)𝑤) = ((,)‘⟨𝑢, 𝑤⟩)
108106, 107syl6eqr 2812 . . . . . . . . . . 11 (𝑧 = ⟨𝑢, 𝑤⟩ → ((,)‘𝑧) = (𝑢(,)𝑤))
109108supeq1d 8517 . . . . . . . . . 10 (𝑧 = ⟨𝑢, 𝑤⟩ → sup(((,)‘𝑧), ℝ*, < ) = sup((𝑢(,)𝑤), ℝ*, < ))
110109eleq1d 2824 . . . . . . . . 9 (𝑧 = ⟨𝑢, 𝑤⟩ → (sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ ↔ sup((𝑢(,)𝑤), ℝ*, < ) ∈ ℝ))
111110ralxp 5419 . . . . . . . 8 (∀𝑧 ∈ ({-∞} × ℝ)sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ ↔ ∀𝑢 ∈ {-∞}∀𝑤 ∈ ℝ sup((𝑢(,)𝑤), ℝ*, < ) ∈ ℝ)
112105, 111mpbir 221 . . . . . . 7 𝑧 ∈ ({-∞} × ℝ)sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ
113 ffn 6206 . . . . . . . . 9 ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
11430, 113ax-mp 5 . . . . . . . 8 (,) Fn (ℝ* × ℝ*)
115 supeq1 8516 . . . . . . . . . 10 (𝑤 = ((,)‘𝑧) → sup(𝑤, ℝ*, < ) = sup(((,)‘𝑧), ℝ*, < ))
116115eleq1d 2824 . . . . . . . . 9 (𝑤 = ((,)‘𝑧) → (sup(𝑤, ℝ*, < ) ∈ ℝ ↔ sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ))
117116ralima 6661 . . . . . . . 8 (((,) Fn (ℝ* × ℝ*) ∧ ({-∞} × ℝ) ⊆ (ℝ* × ℝ*)) → (∀𝑤 ∈ ((,) “ ({-∞} × ℝ))sup(𝑤, ℝ*, < ) ∈ ℝ ↔ ∀𝑧 ∈ ({-∞} × ℝ)sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ))
118114, 36, 117mp2an 710 . . . . . . 7 (∀𝑤 ∈ ((,) “ ({-∞} × ℝ))sup(𝑤, ℝ*, < ) ∈ ℝ ↔ ∀𝑧 ∈ ({-∞} × ℝ)sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ)
119112, 118mpbir 221 . . . . . 6 𝑤 ∈ ((,) “ ({-∞} × ℝ))sup(𝑤, ℝ*, < ) ∈ ℝ
120 ssralv 3807 . . . . . 6 (𝑣 ⊆ ((,) “ ({-∞} × ℝ)) → (∀𝑤 ∈ ((,) “ ({-∞} × ℝ))sup(𝑤, ℝ*, < ) ∈ ℝ → ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ∈ ℝ))
12178, 119, 120mpisyl 21 . . . . 5 ((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) → ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ∈ ℝ)
122121adantrr 755 . . . 4 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ∈ ℝ)
123 fimaxre3 11162 . . . 4 ((𝑣 ∈ Fin ∧ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ∈ ℝ) → ∃𝑥 ∈ ℝ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥)
12476, 122, 123syl2anc 696 . . 3 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → ∃𝑥 ∈ ℝ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥)
125 simplrr 820 . . . . . . . 8 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → ran 𝐹 𝑣)
126125sselda 3744 . . . . . . 7 ((((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ran 𝐹) → 𝑧 𝑣)
127 eluni2 4592 . . . . . . . 8 (𝑧 𝑣 ↔ ∃𝑤𝑣 𝑧𝑤)
128 r19.29r 3211 . . . . . . . . . 10 ((∃𝑤𝑣 𝑧𝑤 ∧ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥) → ∃𝑤𝑣 (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥))
129 sspwuni 4763 . . . . . . . . . . . . . . . . . . 19 (((,) “ ({-∞} × ℝ)) ⊆ 𝒫 ℝ ↔ ((,) “ ({-∞} × ℝ)) ⊆ ℝ)
13015, 129mpbir 221 . . . . . . . . . . . . . . . . . 18 ((,) “ ({-∞} × ℝ)) ⊆ 𝒫 ℝ
131783ad2ant1 1128 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑣 ⊆ ((,) “ ({-∞} × ℝ)))
132 simp2r 1243 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤𝑣)
133131, 132sseldd 3745 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤 ∈ ((,) “ ({-∞} × ℝ)))
134130, 133sseldi 3742 . . . . . . . . . . . . . . . . 17 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤 ∈ 𝒫 ℝ)
135134elpwid 4314 . . . . . . . . . . . . . . . 16 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤 ⊆ ℝ)
136 simp3l 1244 . . . . . . . . . . . . . . . 16 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑧𝑤)
137135, 136sseldd 3745 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑧 ∈ ℝ)
138121r19.21bi 3070 . . . . . . . . . . . . . . . . 17 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ 𝑤𝑣) → sup(𝑤, ℝ*, < ) ∈ ℝ)
139138adantrl 754 . . . . . . . . . . . . . . . 16 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣)) → sup(𝑤, ℝ*, < ) ∈ ℝ)
1401393adant3 1127 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → sup(𝑤, ℝ*, < ) ∈ ℝ)
141 simp2l 1242 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑥 ∈ ℝ)
142135, 18syl6ss 3756 . . . . . . . . . . . . . . . 16 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤 ⊆ ℝ*)
143 supxrub 12347 . . . . . . . . . . . . . . . 16 ((𝑤 ⊆ ℝ*𝑧𝑤) → 𝑧 ≤ sup(𝑤, ℝ*, < ))
144142, 136, 143syl2anc 696 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑧 ≤ sup(𝑤, ℝ*, < ))
145 simp3r 1245 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → sup(𝑤, ℝ*, < ) ≤ 𝑥)
146137, 140, 141, 144, 145letrd 10386 . . . . . . . . . . . . . 14 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑧𝑥)
1471463expia 1115 . . . . . . . . . . . . 13 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣)) → ((𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧𝑥))
148147anassrs 683 . . . . . . . . . . . 12 ((((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ 𝑥 ∈ ℝ) ∧ 𝑤𝑣) → ((𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧𝑥))
149148rexlimdva 3169 . . . . . . . . . . 11 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ 𝑥 ∈ ℝ) → (∃𝑤𝑣 (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧𝑥))
150149adantlrr 759 . . . . . . . . . 10 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → (∃𝑤𝑣 (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧𝑥))
151128, 150syl5 34 . . . . . . . . 9 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → ((∃𝑤𝑣 𝑧𝑤 ∧ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧𝑥))
152151expdimp 452 . . . . . . . 8 ((((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) ∧ ∃𝑤𝑣 𝑧𝑤) → (∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥𝑧𝑥))
153127, 152sylan2b 493 . . . . . . 7 ((((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) ∧ 𝑧 𝑣) → (∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥𝑧𝑥))
154126, 153syldan 488 . . . . . 6 ((((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ran 𝐹) → (∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥𝑧𝑥))
155154ralrimdva 3107 . . . . 5 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → (∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥 → ∀𝑧 ∈ ran 𝐹 𝑧𝑥))
156 ffn 6206 . . . . . . . 8 (𝐹:𝑋⟶ℝ → 𝐹 Fn 𝑋)
1578, 156syl 17 . . . . . . 7 (𝜑𝐹 Fn 𝑋)
158157ad2antrr 764 . . . . . 6 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn 𝑋)
159 breq1 4807 . . . . . . 7 (𝑧 = (𝐹𝑦) → (𝑧𝑥 ↔ (𝐹𝑦) ≤ 𝑥))
160159ralrn 6525 . . . . . 6 (𝐹 Fn 𝑋 → (∀𝑧 ∈ ran 𝐹 𝑧𝑥 ↔ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
161158, 160syl 17 . . . . 5 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran 𝐹 𝑧𝑥 ↔ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
162155, 161sylibd 229 . . . 4 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → (∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥 → ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
163162reximdva 3155 . . 3 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → (∃𝑥 ∈ ℝ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
164124, 163mpd 15 . 2 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → ∃𝑥 ∈ ℝ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥)
16571, 164rexlimddv 3173 1 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2139  wne 2932  wral 3050  wrex 3051  cin 3714  wss 3715  c0 4058  𝒫 cpw 4302  {csn 4321  cop 4327   cuni 4588   class class class wbr 4804   × cxp 5264  dom cdm 5266  ran crn 5267  cima 5269  Fun wfun 6043   Fn wfn 6044  wf 6045  cfv 6049  (class class class)co 6813  Fincfn 8121  supcsup 8511  cr 10127  1c1 10129   + caddc 10131  -∞cmnf 10264  *cxr 10265   < clt 10266  cle 10267  (,)cioo 12368  t crest 16283  topGenctg 16300  Topctop 20900  TopOnctopon 20917  TopBasesctb 20951   Cn ccn 21230  Compccmp 21391
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-rep 4923  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  ax-pre-sup 10206
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-rmo 3058  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-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-we 5227  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-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  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-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-oadd 7733  df-er 7911  df-map 8025  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fi 8482  df-sup 8513  df-inf 8514  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-n0 11485  df-z 11570  df-uz 11880  df-q 11982  df-ioo 12372  df-rest 16285  df-topgen 16306  df-top 20901  df-topon 20918  df-bases 20952  df-cn 21233  df-cmp 21392
This theorem is referenced by:  evth  22959
  Copyright terms: Public domain W3C validator