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

Theorem bndth 22565
 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 22377 . . . . . . . 8 (topGen‘ran (,)) ∈ (TopOn‘ℝ)
53, 4eqeltri 2684 . . . . . . 7 𝐾 ∈ (TopOn‘ℝ)
65toponunii 20547 . . . . . 6 ℝ = 𝐾
72, 6cnf 20860 . . . . 5 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶ℝ)
81, 7syl 17 . . . 4 (𝜑𝐹:𝑋⟶ℝ)
9 frn 5966 . . . 4 (𝐹:𝑋⟶ℝ → ran 𝐹 ⊆ ℝ)
108, 9syl 17 . . 3 (𝜑 → ran 𝐹 ⊆ ℝ)
11 imassrn 5396 . . . . . 6 ((,) “ ({-∞} × ℝ)) ⊆ ran (,)
12 retopbas 22374 . . . . . . . 8 ran (,) ∈ TopBases
13 bastg 20581 . . . . . . . 8 (ran (,) ∈ TopBases → ran (,) ⊆ (topGen‘ran (,)))
1412, 13ax-mp 5 . . . . . . 7 ran (,) ⊆ (topGen‘ran (,))
1514, 3sseqtr4i 3601 . . . . . 6 ran (,) ⊆ 𝐾
1611, 15sstri 3577 . . . . 5 ((,) “ ({-∞} × ℝ)) ⊆ 𝐾
17 retop 22375 . . . . . . . 8 (topGen‘ran (,)) ∈ Top
183, 17eqeltri 2684 . . . . . . 7 𝐾 ∈ Top
1918elexi 3186 . . . . . 6 𝐾 ∈ V
2019elpw2 4755 . . . . 5 (((,) “ ({-∞} × ℝ)) ∈ 𝒫 𝐾 ↔ ((,) “ ({-∞} × ℝ)) ⊆ 𝐾)
2116, 20mpbir 220 . . . 4 ((,) “ ({-∞} × ℝ)) ∈ 𝒫 𝐾
22 bndth.3 . . . . . 6 (𝜑𝐽 ∈ Comp)
23 rncmp 21009 . . . . . 6 ((𝐽 ∈ Comp ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐾t ran 𝐹) ∈ Comp)
2422, 1, 23syl2anc 691 . . . . 5 (𝜑 → (𝐾t ran 𝐹) ∈ Comp)
256cmpsub 21013 . . . . . 6 ((𝐾 ∈ Top ∧ ran 𝐹 ⊆ ℝ) → ((𝐾t ran 𝐹) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 𝐾(ran 𝐹 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 𝑣)))
2618, 10, 25sylancr 694 . . . . 5 (𝜑 → ((𝐾t ran 𝐹) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 𝐾(ran 𝐹 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 𝑣)))
2724, 26mpbid 221 . . . 4 (𝜑 → ∀𝑢 ∈ 𝒫 𝐾(ran 𝐹 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 𝑣))
28 unieq 4380 . . . . . . . 8 (𝑢 = ((,) “ ({-∞} × ℝ)) → 𝑢 = ((,) “ ({-∞} × ℝ)))
2911unissi 4397 . . . . . . . . . 10 ((,) “ ({-∞} × ℝ)) ⊆ ran (,)
30 unirnioo 12144 . . . . . . . . . 10 ℝ = ran (,)
3129, 30sseqtr4i 3601 . . . . . . . . 9 ((,) “ ({-∞} × ℝ)) ⊆ ℝ
32 id 22 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → 𝑥 ∈ ℝ)
33 ltp1 10740 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → 𝑥 < (𝑥 + 1))
34 ressxr 9962 . . . . . . . . . . . . . 14 ℝ ⊆ ℝ*
35 peano2re 10088 . . . . . . . . . . . . . 14 (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ)
3634, 35sseldi 3566 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → (𝑥 + 1) ∈ ℝ*)
37 elioomnf 12139 . . . . . . . . . . . . 13 ((𝑥 + 1) ∈ ℝ* → (𝑥 ∈ (-∞(,)(𝑥 + 1)) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < (𝑥 + 1))))
3836, 37syl 17 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → (𝑥 ∈ (-∞(,)(𝑥 + 1)) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < (𝑥 + 1))))
3932, 33, 38mpbir2and 959 . . . . . . . . . . 11 (𝑥 ∈ ℝ → 𝑥 ∈ (-∞(,)(𝑥 + 1)))
40 df-ov 6552 . . . . . . . . . . . 12 (-∞(,)(𝑥 + 1)) = ((,)‘⟨-∞, (𝑥 + 1)⟩)
41 mnfxr 9975 . . . . . . . . . . . . . . . 16 -∞ ∈ ℝ*
4241elexi 3186 . . . . . . . . . . . . . . 15 -∞ ∈ V
4342snid 4155 . . . . . . . . . . . . . 14 -∞ ∈ {-∞}
44 opelxpi 5072 . . . . . . . . . . . . . 14 ((-∞ ∈ {-∞} ∧ (𝑥 + 1) ∈ ℝ) → ⟨-∞, (𝑥 + 1)⟩ ∈ ({-∞} × ℝ))
4543, 35, 44sylancr 694 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ → ⟨-∞, (𝑥 + 1)⟩ ∈ ({-∞} × ℝ))
46 ioof 12142 . . . . . . . . . . . . . . 15 (,):(ℝ* × ℝ*)⟶𝒫 ℝ
47 ffun 5961 . . . . . . . . . . . . . . 15 ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → Fun (,))
4846, 47ax-mp 5 . . . . . . . . . . . . . 14 Fun (,)
49 snssi 4280 . . . . . . . . . . . . . . . . 17 (-∞ ∈ ℝ* → {-∞} ⊆ ℝ*)
5041, 49ax-mp 5 . . . . . . . . . . . . . . . 16 {-∞} ⊆ ℝ*
51 xpss12 5148 . . . . . . . . . . . . . . . 16 (({-∞} ⊆ ℝ* ∧ ℝ ⊆ ℝ*) → ({-∞} × ℝ) ⊆ (ℝ* × ℝ*))
5250, 34, 51mp2an 704 . . . . . . . . . . . . . . 15 ({-∞} × ℝ) ⊆ (ℝ* × ℝ*)
5346fdmi 5965 . . . . . . . . . . . . . . 15 dom (,) = (ℝ* × ℝ*)
5452, 53sseqtr4i 3601 . . . . . . . . . . . . . 14 ({-∞} × ℝ) ⊆ dom (,)
55 funfvima2 6397 . . . . . . . . . . . . . 14 ((Fun (,) ∧ ({-∞} × ℝ) ⊆ dom (,)) → (⟨-∞, (𝑥 + 1)⟩ ∈ ({-∞} × ℝ) → ((,)‘⟨-∞, (𝑥 + 1)⟩) ∈ ((,) “ ({-∞} × ℝ))))
5648, 54, 55mp2an 704 . . . . . . . . . . . . 13 (⟨-∞, (𝑥 + 1)⟩ ∈ ({-∞} × ℝ) → ((,)‘⟨-∞, (𝑥 + 1)⟩) ∈ ((,) “ ({-∞} × ℝ)))
5745, 56syl 17 . . . . . . . . . . . 12 (𝑥 ∈ ℝ → ((,)‘⟨-∞, (𝑥 + 1)⟩) ∈ ((,) “ ({-∞} × ℝ)))
5840, 57syl5eqel 2692 . . . . . . . . . . 11 (𝑥 ∈ ℝ → (-∞(,)(𝑥 + 1)) ∈ ((,) “ ({-∞} × ℝ)))
59 elunii 4377 . . . . . . . . . . 11 ((𝑥 ∈ (-∞(,)(𝑥 + 1)) ∧ (-∞(,)(𝑥 + 1)) ∈ ((,) “ ({-∞} × ℝ))) → 𝑥 ((,) “ ({-∞} × ℝ)))
6039, 58, 59syl2anc 691 . . . . . . . . . 10 (𝑥 ∈ ℝ → 𝑥 ((,) “ ({-∞} × ℝ)))
6160ssriv 3572 . . . . . . . . 9 ℝ ⊆ ((,) “ ({-∞} × ℝ))
6231, 61eqssi 3584 . . . . . . . 8 ((,) “ ({-∞} × ℝ)) = ℝ
6328, 62syl6eq 2660 . . . . . . 7 (𝑢 = ((,) “ ({-∞} × ℝ)) → 𝑢 = ℝ)
6463sseq2d 3596 . . . . . 6 (𝑢 = ((,) “ ({-∞} × ℝ)) → (ran 𝐹 𝑢 ↔ ran 𝐹 ⊆ ℝ))
65 pweq 4111 . . . . . . . 8 (𝑢 = ((,) “ ({-∞} × ℝ)) → 𝒫 𝑢 = 𝒫 ((,) “ ({-∞} × ℝ)))
6665ineq1d 3775 . . . . . . 7 (𝑢 = ((,) “ ({-∞} × ℝ)) → (𝒫 𝑢 ∩ Fin) = (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin))
6766rexeqdv 3122 . . . . . 6 (𝑢 = ((,) “ ({-∞} × ℝ)) → (∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 𝑣 ↔ ∃𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)ran 𝐹 𝑣))
6864, 67imbi12d 333 . . . . 5 (𝑢 = ((,) “ ({-∞} × ℝ)) → ((ran 𝐹 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 𝑣) ↔ (ran 𝐹 ⊆ ℝ → ∃𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)ran 𝐹 𝑣)))
6968rspcv 3278 . . . 4 (((,) “ ({-∞} × ℝ)) ∈ 𝒫 𝐾 → (∀𝑢 ∈ 𝒫 𝐾(ran 𝐹 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 𝑣) → (ran 𝐹 ⊆ ℝ → ∃𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)ran 𝐹 𝑣)))
7021, 27, 69mpsyl 66 . . 3 (𝜑 → (ran 𝐹 ⊆ ℝ → ∃𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)ran 𝐹 𝑣))
7110, 70mpd 15 . 2 (𝜑 → ∃𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)ran 𝐹 𝑣)
72 simpr 476 . . . . . . 7 ((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) → 𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin))
73 elin 3758 . . . . . . 7 (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ↔ (𝑣 ∈ 𝒫 ((,) “ ({-∞} × ℝ)) ∧ 𝑣 ∈ Fin))
7472, 73sylib 207 . . . . . 6 ((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) → (𝑣 ∈ 𝒫 ((,) “ ({-∞} × ℝ)) ∧ 𝑣 ∈ Fin))
7574adantrr 749 . . . . 5 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → (𝑣 ∈ 𝒫 ((,) “ ({-∞} × ℝ)) ∧ 𝑣 ∈ Fin))
7675simprd 478 . . . 4 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → 𝑣 ∈ Fin)
7774simpld 474 . . . . . . 7 ((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) → 𝑣 ∈ 𝒫 ((,) “ ({-∞} × ℝ)))
7877elpwid 4118 . . . . . 6 ((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) → 𝑣 ⊆ ((,) “ ({-∞} × ℝ)))
7950sseli 3564 . . . . . . . . . . . 12 (𝑢 ∈ {-∞} → 𝑢 ∈ ℝ*)
8079adantr 480 . . . . . . . . . . 11 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → 𝑢 ∈ ℝ*)
8134sseli 3564 . . . . . . . . . . . 12 (𝑤 ∈ ℝ → 𝑤 ∈ ℝ*)
8281adantl 481 . . . . . . . . . . 11 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℝ*)
83 mnflt 11833 . . . . . . . . . . . . . . 15 (𝑤 ∈ ℝ → -∞ < 𝑤)
84 xrltnle 9984 . . . . . . . . . . . . . . . 16 ((-∞ ∈ ℝ*𝑤 ∈ ℝ*) → (-∞ < 𝑤 ↔ ¬ 𝑤 ≤ -∞))
8541, 81, 84sylancr 694 . . . . . . . . . . . . . . 15 (𝑤 ∈ ℝ → (-∞ < 𝑤 ↔ ¬ 𝑤 ≤ -∞))
8683, 85mpbid 221 . . . . . . . . . . . . . 14 (𝑤 ∈ ℝ → ¬ 𝑤 ≤ -∞)
8786adantl 481 . . . . . . . . . . . . 13 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → ¬ 𝑤 ≤ -∞)
88 elsni 4142 . . . . . . . . . . . . . . 15 (𝑢 ∈ {-∞} → 𝑢 = -∞)
8988adantr 480 . . . . . . . . . . . . . 14 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → 𝑢 = -∞)
9089breq2d 4595 . . . . . . . . . . . . 13 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → (𝑤𝑢𝑤 ≤ -∞))
9187, 90mtbird 314 . . . . . . . . . . . 12 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → ¬ 𝑤𝑢)
92 ioo0 12071 . . . . . . . . . . . . . 14 ((𝑢 ∈ ℝ*𝑤 ∈ ℝ*) → ((𝑢(,)𝑤) = ∅ ↔ 𝑤𝑢))
9379, 81, 92syl2an 493 . . . . . . . . . . . . 13 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → ((𝑢(,)𝑤) = ∅ ↔ 𝑤𝑢))
9493necon3abid 2818 . . . . . . . . . . . 12 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → ((𝑢(,)𝑤) ≠ ∅ ↔ ¬ 𝑤𝑢))
9591, 94mpbird 246 . . . . . . . . . . 11 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → (𝑢(,)𝑤) ≠ ∅)
96 df-ioo 12050 . . . . . . . . . . . 12 (,) = (𝑦 ∈ ℝ*, 𝑧 ∈ ℝ* ↦ {𝑣 ∈ ℝ* ∣ (𝑦 < 𝑣𝑣 < 𝑧)})
97 idd 24 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ*𝑤 ∈ ℝ*) → (𝑥 < 𝑤𝑥 < 𝑤))
98 xrltle 11858 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ*𝑤 ∈ ℝ*) → (𝑥 < 𝑤𝑥𝑤))
99 idd 24 . . . . . . . . . . . 12 ((𝑢 ∈ ℝ*𝑥 ∈ ℝ*) → (𝑢 < 𝑥𝑢 < 𝑥))
100 xrltle 11858 . . . . . . . . . . . 12 ((𝑢 ∈ ℝ*𝑥 ∈ ℝ*) → (𝑢 < 𝑥𝑢𝑥))
10196, 97, 98, 99, 100ixxub 12067 . . . . . . . . . . 11 ((𝑢 ∈ ℝ*𝑤 ∈ ℝ* ∧ (𝑢(,)𝑤) ≠ ∅) → sup((𝑢(,)𝑤), ℝ*, < ) = 𝑤)
10280, 82, 95, 101syl3anc 1318 . . . . . . . . . 10 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → sup((𝑢(,)𝑤), ℝ*, < ) = 𝑤)
103 simpr 476 . . . . . . . . . 10 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → 𝑤 ∈ ℝ)
104102, 103eqeltrd 2688 . . . . . . . . 9 ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → sup((𝑢(,)𝑤), ℝ*, < ) ∈ ℝ)
105104rgen2 2958 . . . . . . . 8 𝑢 ∈ {-∞}∀𝑤 ∈ ℝ sup((𝑢(,)𝑤), ℝ*, < ) ∈ ℝ
106 fveq2 6103 . . . . . . . . . . . 12 (𝑧 = ⟨𝑢, 𝑤⟩ → ((,)‘𝑧) = ((,)‘⟨𝑢, 𝑤⟩))
107 df-ov 6552 . . . . . . . . . . . 12 (𝑢(,)𝑤) = ((,)‘⟨𝑢, 𝑤⟩)
108106, 107syl6eqr 2662 . . . . . . . . . . 11 (𝑧 = ⟨𝑢, 𝑤⟩ → ((,)‘𝑧) = (𝑢(,)𝑤))
109108supeq1d 8235 . . . . . . . . . 10 (𝑧 = ⟨𝑢, 𝑤⟩ → sup(((,)‘𝑧), ℝ*, < ) = sup((𝑢(,)𝑤), ℝ*, < ))
110109eleq1d 2672 . . . . . . . . 9 (𝑧 = ⟨𝑢, 𝑤⟩ → (sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ ↔ sup((𝑢(,)𝑤), ℝ*, < ) ∈ ℝ))
111110ralxp 5185 . . . . . . . 8 (∀𝑧 ∈ ({-∞} × ℝ)sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ ↔ ∀𝑢 ∈ {-∞}∀𝑤 ∈ ℝ sup((𝑢(,)𝑤), ℝ*, < ) ∈ ℝ)
112105, 111mpbir 220 . . . . . . 7 𝑧 ∈ ({-∞} × ℝ)sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ
113 ffn 5958 . . . . . . . . 9 ((,):(ℝ* × ℝ*)⟶𝒫 ℝ → (,) Fn (ℝ* × ℝ*))
11446, 113ax-mp 5 . . . . . . . 8 (,) Fn (ℝ* × ℝ*)
115 supeq1 8234 . . . . . . . . . 10 (𝑤 = ((,)‘𝑧) → sup(𝑤, ℝ*, < ) = sup(((,)‘𝑧), ℝ*, < ))
116115eleq1d 2672 . . . . . . . . 9 (𝑤 = ((,)‘𝑧) → (sup(𝑤, ℝ*, < ) ∈ ℝ ↔ sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ))
117116ralima 6402 . . . . . . . 8 (((,) Fn (ℝ* × ℝ*) ∧ ({-∞} × ℝ) ⊆ (ℝ* × ℝ*)) → (∀𝑤 ∈ ((,) “ ({-∞} × ℝ))sup(𝑤, ℝ*, < ) ∈ ℝ ↔ ∀𝑧 ∈ ({-∞} × ℝ)sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ))
118114, 52, 117mp2an 704 . . . . . . 7 (∀𝑤 ∈ ((,) “ ({-∞} × ℝ))sup(𝑤, ℝ*, < ) ∈ ℝ ↔ ∀𝑧 ∈ ({-∞} × ℝ)sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ)
119112, 118mpbir 220 . . . . . 6 𝑤 ∈ ((,) “ ({-∞} × ℝ))sup(𝑤, ℝ*, < ) ∈ ℝ
120 ssralv 3629 . . . . . 6 (𝑣 ⊆ ((,) “ ({-∞} × ℝ)) → (∀𝑤 ∈ ((,) “ ({-∞} × ℝ))sup(𝑤, ℝ*, < ) ∈ ℝ → ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ∈ ℝ))
12178, 119, 120mpisyl 21 . . . . 5 ((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) → ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ∈ ℝ)
122121adantrr 749 . . . 4 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ∈ ℝ)
123 fimaxre3 10849 . . . 4 ((𝑣 ∈ Fin ∧ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ∈ ℝ) → ∃𝑥 ∈ ℝ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥)
12476, 122, 123syl2anc 691 . . 3 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → ∃𝑥 ∈ ℝ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥)
125 simplrr 797 . . . . . . . 8 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → ran 𝐹 𝑣)
126125sselda 3568 . . . . . . 7 ((((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ran 𝐹) → 𝑧 𝑣)
127 eluni2 4376 . . . . . . . 8 (𝑧 𝑣 ↔ ∃𝑤𝑣 𝑧𝑤)
128 r19.29r 3055 . . . . . . . . . 10 ((∃𝑤𝑣 𝑧𝑤 ∧ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥) → ∃𝑤𝑣 (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥))
129 sspwuni 4547 . . . . . . . . . . . . . . . . . . 19 (((,) “ ({-∞} × ℝ)) ⊆ 𝒫 ℝ ↔ ((,) “ ({-∞} × ℝ)) ⊆ ℝ)
13031, 129mpbir 220 . . . . . . . . . . . . . . . . . 18 ((,) “ ({-∞} × ℝ)) ⊆ 𝒫 ℝ
131783ad2ant1 1075 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑣 ⊆ ((,) “ ({-∞} × ℝ)))
132 simp2r 1081 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤𝑣)
133131, 132sseldd 3569 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤 ∈ ((,) “ ({-∞} × ℝ)))
134130, 133sseldi 3566 . . . . . . . . . . . . . . . . 17 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤 ∈ 𝒫 ℝ)
135134elpwid 4118 . . . . . . . . . . . . . . . 16 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤 ⊆ ℝ)
136 simp3l 1082 . . . . . . . . . . . . . . . 16 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑧𝑤)
137135, 136sseldd 3569 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑧 ∈ ℝ)
138121r19.21bi 2916 . . . . . . . . . . . . . . . . 17 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ 𝑤𝑣) → sup(𝑤, ℝ*, < ) ∈ ℝ)
139138adantrl 748 . . . . . . . . . . . . . . . 16 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣)) → sup(𝑤, ℝ*, < ) ∈ ℝ)
1401393adant3 1074 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → sup(𝑤, ℝ*, < ) ∈ ℝ)
141 simp2l 1080 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑥 ∈ ℝ)
142135, 34syl6ss 3580 . . . . . . . . . . . . . . . 16 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤 ⊆ ℝ*)
143 supxrub 12026 . . . . . . . . . . . . . . . 16 ((𝑤 ⊆ ℝ*𝑧𝑤) → 𝑧 ≤ sup(𝑤, ℝ*, < ))
144142, 136, 143syl2anc 691 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑧 ≤ sup(𝑤, ℝ*, < ))
145 simp3r 1083 . . . . . . . . . . . . . . 15 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → sup(𝑤, ℝ*, < ) ≤ 𝑥)
146137, 140, 141, 144, 145letrd 10073 . . . . . . . . . . . . . 14 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣) ∧ (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑧𝑥)
1471463expia 1259 . . . . . . . . . . . . 13 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤𝑣)) → ((𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧𝑥))
148147anassrs 678 . . . . . . . . . . . 12 ((((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ 𝑥 ∈ ℝ) ∧ 𝑤𝑣) → ((𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧𝑥))
149148rexlimdva 3013 . . . . . . . . . . 11 (((𝜑𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin)) ∧ 𝑥 ∈ ℝ) → (∃𝑤𝑣 (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧𝑥))
150149adantlrr 753 . . . . . . . . . 10 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → (∃𝑤𝑣 (𝑧𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧𝑥))
151128, 150syl5 33 . . . . . . . . 9 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → ((∃𝑤𝑣 𝑧𝑤 ∧ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧𝑥))
152151expdimp 452 . . . . . . . 8 ((((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) ∧ ∃𝑤𝑣 𝑧𝑤) → (∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥𝑧𝑥))
153127, 152sylan2b 491 . . . . . . 7 ((((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) ∧ 𝑧 𝑣) → (∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥𝑧𝑥))
154126, 153syldan 486 . . . . . 6 ((((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ran 𝐹) → (∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥𝑧𝑥))
155154ralrimdva 2952 . . . . 5 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → (∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥 → ∀𝑧 ∈ ran 𝐹 𝑧𝑥))
156 ffn 5958 . . . . . . . 8 (𝐹:𝑋⟶ℝ → 𝐹 Fn 𝑋)
1578, 156syl 17 . . . . . . 7 (𝜑𝐹 Fn 𝑋)
158157ad2antrr 758 . . . . . 6 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn 𝑋)
159 breq1 4586 . . . . . . 7 (𝑧 = (𝐹𝑦) → (𝑧𝑥 ↔ (𝐹𝑦) ≤ 𝑥))
160159ralrn 6270 . . . . . 6 (𝐹 Fn 𝑋 → (∀𝑧 ∈ ran 𝐹 𝑧𝑥 ↔ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
161158, 160syl 17 . . . . 5 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran 𝐹 𝑧𝑥 ↔ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
162155, 161sylibd 228 . . . 4 (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) ∧ 𝑥 ∈ ℝ) → (∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥 → ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
163162reximdva 3000 . . 3 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → (∃𝑥 ∈ ℝ ∀𝑤𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥))
164124, 163mpd 15 . 2 ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞} × ℝ)) ∩ Fin) ∧ ran 𝐹 𝑣)) → ∃𝑥 ∈ ℝ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥)
16571, 164rexlimddv 3017 1 (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦𝑋 (𝐹𝑦) ≤ 𝑥)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108  {csn 4125  ⟨cop 4131  ∪ cuni 4372   class class class wbr 4583   × cxp 5036  dom cdm 5038  ran crn 5039   “ cima 5041  Fun wfun 5798   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  Fincfn 7841  supcsup 8229  ℝcr 9814  1c1 9816   + caddc 9818  -∞cmnf 9951  ℝ*cxr 9952   < clt 9953   ≤ cle 9954  (,)cioo 12046   ↾t crest 15904  topGenctg 15921  Topctop 20517  TopOnctopon 20518  TopBasesctb 20520   Cn ccn 20838  Compccmp 20999 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892  ax-pre-sup 9893 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-fi 8200  df-sup 8231  df-inf 8232  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-div 10564  df-nn 10898  df-n0 11170  df-z 11255  df-uz 11564  df-q 11665  df-ioo 12050  df-rest 15906  df-topgen 15927  df-top 20521  df-bases 20522  df-topon 20523  df-cn 20841  df-cmp 21000 This theorem is referenced by:  evth  22566
 Copyright terms: Public domain W3C validator