Step | Hyp | Ref
| Expression |
1 | | bndth.4 |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝐽 Cn 𝐾)) |
2 | | bndth.1 |
. . . . . 6
⊢ 𝑋 = ∪
𝐽 |
3 | | bndth.2 |
. . . . . . . 8
⊢ 𝐾 = (topGen‘ran
(,)) |
4 | | retopon 23516 |
. . . . . . . 8
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
5 | 3, 4 | eqeltri 2829 |
. . . . . . 7
⊢ 𝐾 ∈
(TopOn‘ℝ) |
6 | 5 | toponunii 21667 |
. . . . . 6
⊢ ℝ =
∪ 𝐾 |
7 | 2, 6 | cnf 21997 |
. . . . 5
⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶ℝ) |
8 | 1, 7 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐹:𝑋⟶ℝ) |
9 | 8 | frnd 6512 |
. . 3
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
10 | | unieq 4807 |
. . . . . . 7
⊢ (𝑢 = ((,) “ ({-∞}
× ℝ)) → ∪ 𝑢 = ∪ ((,) “
({-∞} × ℝ))) |
11 | | imassrn 5914 |
. . . . . . . . . 10
⊢ ((,)
“ ({-∞} × ℝ)) ⊆ ran (,) |
12 | 11 | unissi 4805 |
. . . . . . . . 9
⊢ ∪ ((,) “ ({-∞} × ℝ)) ⊆ ∪ ran (,) |
13 | | unirnioo 12923 |
. . . . . . . . 9
⊢ ℝ =
∪ ran (,) |
14 | 12, 13 | sseqtrri 3914 |
. . . . . . . 8
⊢ ∪ ((,) “ ({-∞} × ℝ)) ⊆
ℝ |
15 | | id 22 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℝ) |
16 | | ltp1 11558 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → 𝑥 < (𝑥 + 1)) |
17 | | ressxr 10763 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℝ* |
18 | | peano2re 10891 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ) |
19 | 17, 18 | sseldi 3875 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ → (𝑥 + 1) ∈
ℝ*) |
20 | | elioomnf 12918 |
. . . . . . . . . . . 12
⊢ ((𝑥 + 1) ∈ ℝ*
→ (𝑥 ∈
(-∞(,)(𝑥 + 1)) ↔
(𝑥 ∈ ℝ ∧
𝑥 < (𝑥 + 1)))) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ → (𝑥 ∈ (-∞(,)(𝑥 + 1)) ↔ (𝑥 ∈ ℝ ∧ 𝑥 < (𝑥 + 1)))) |
22 | 15, 16, 21 | mpbir2and 713 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → 𝑥 ∈ (-∞(,)(𝑥 + 1))) |
23 | | df-ov 7173 |
. . . . . . . . . . 11
⊢
(-∞(,)(𝑥 + 1))
= ((,)‘〈-∞, (𝑥 + 1)〉) |
24 | | mnfxr 10776 |
. . . . . . . . . . . . . . 15
⊢ -∞
∈ ℝ* |
25 | 24 | elexi 3417 |
. . . . . . . . . . . . . 14
⊢ -∞
∈ V |
26 | 25 | snid 4552 |
. . . . . . . . . . . . 13
⊢ -∞
∈ {-∞} |
27 | | opelxpi 5562 |
. . . . . . . . . . . . 13
⊢
((-∞ ∈ {-∞} ∧ (𝑥 + 1) ∈ ℝ) → 〈-∞,
(𝑥 + 1)〉 ∈
({-∞} × ℝ)) |
28 | 26, 18, 27 | sylancr 590 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ →
〈-∞, (𝑥 +
1)〉 ∈ ({-∞} × ℝ)) |
29 | | ioof 12921 |
. . . . . . . . . . . . . 14
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
30 | | ffun 6507 |
. . . . . . . . . . . . . 14
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → Fun (,)) |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ Fun
(,) |
32 | | snssi 4696 |
. . . . . . . . . . . . . . . 16
⊢ (-∞
∈ ℝ* → {-∞} ⊆
ℝ*) |
33 | 24, 32 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
{-∞} ⊆ ℝ* |
34 | | xpss12 5540 |
. . . . . . . . . . . . . . 15
⊢
(({-∞} ⊆ ℝ* ∧ ℝ ⊆
ℝ*) → ({-∞} × ℝ) ⊆
(ℝ* × ℝ*)) |
35 | 33, 17, 34 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢
({-∞} × ℝ) ⊆ (ℝ* ×
ℝ*) |
36 | 29 | fdmi 6516 |
. . . . . . . . . . . . . 14
⊢ dom (,) =
(ℝ* × ℝ*) |
37 | 35, 36 | sseqtrri 3914 |
. . . . . . . . . . . . 13
⊢
({-∞} × ℝ) ⊆ dom (,) |
38 | | funfvima2 7004 |
. . . . . . . . . . . . 13
⊢ ((Fun (,)
∧ ({-∞} × ℝ) ⊆ dom (,)) → (〈-∞,
(𝑥 + 1)〉 ∈
({-∞} × ℝ) → ((,)‘〈-∞, (𝑥 + 1)〉) ∈ ((,) “
({-∞} × ℝ)))) |
39 | 31, 37, 38 | mp2an 692 |
. . . . . . . . . . . 12
⊢
(〈-∞, (𝑥
+ 1)〉 ∈ ({-∞} × ℝ) →
((,)‘〈-∞, (𝑥 + 1)〉) ∈ ((,) “ ({-∞}
× ℝ))) |
40 | 28, 39 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ →
((,)‘〈-∞, (𝑥 + 1)〉) ∈ ((,) “ ({-∞}
× ℝ))) |
41 | 23, 40 | eqeltrid 2837 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ →
(-∞(,)(𝑥 + 1)) ∈
((,) “ ({-∞} × ℝ))) |
42 | | elunii 4801 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (-∞(,)(𝑥 + 1)) ∧ (-∞(,)(𝑥 + 1)) ∈ ((,) “
({-∞} × ℝ))) → 𝑥 ∈ ∪ ((,)
“ ({-∞} × ℝ))) |
43 | 22, 41, 42 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ → 𝑥 ∈ ∪ ((,) “ ({-∞} ×
ℝ))) |
44 | 43 | ssriv 3881 |
. . . . . . . 8
⊢ ℝ
⊆ ∪ ((,) “ ({-∞} ×
ℝ)) |
45 | 14, 44 | eqssi 3893 |
. . . . . . 7
⊢ ∪ ((,) “ ({-∞} × ℝ)) =
ℝ |
46 | 10, 45 | eqtrdi 2789 |
. . . . . 6
⊢ (𝑢 = ((,) “ ({-∞}
× ℝ)) → ∪ 𝑢 = ℝ) |
47 | 46 | sseq2d 3909 |
. . . . 5
⊢ (𝑢 = ((,) “ ({-∞}
× ℝ)) → (ran 𝐹 ⊆ ∪ 𝑢 ↔ ran 𝐹 ⊆ ℝ)) |
48 | | pweq 4504 |
. . . . . . 7
⊢ (𝑢 = ((,) “ ({-∞}
× ℝ)) → 𝒫 𝑢 = 𝒫 ((,) “ ({-∞} ×
ℝ))) |
49 | 48 | ineq1d 4102 |
. . . . . 6
⊢ (𝑢 = ((,) “ ({-∞}
× ℝ)) → (𝒫 𝑢 ∩ Fin) = (𝒫 ((,) “
({-∞} × ℝ)) ∩ Fin)) |
50 | 49 | rexeqdv 3317 |
. . . . 5
⊢ (𝑢 = ((,) “ ({-∞}
× ℝ)) → (∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 ⊆ ∪ 𝑣 ↔ ∃𝑣 ∈ (𝒫 ((,) “
({-∞} × ℝ)) ∩ Fin)ran 𝐹 ⊆ ∪ 𝑣)) |
51 | 47, 50 | imbi12d 348 |
. . . 4
⊢ (𝑢 = ((,) “ ({-∞}
× ℝ)) → ((ran 𝐹 ⊆ ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 ⊆ ∪ 𝑣) ↔ (ran 𝐹 ⊆ ℝ → ∃𝑣 ∈ (𝒫 ((,) “
({-∞} × ℝ)) ∩ Fin)ran 𝐹 ⊆ ∪ 𝑣))) |
52 | | bndth.3 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ Comp) |
53 | | rncmp 22147 |
. . . . . 6
⊢ ((𝐽 ∈ Comp ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → (𝐾 ↾t ran 𝐹) ∈ Comp) |
54 | 52, 1, 53 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (𝐾 ↾t ran 𝐹) ∈ Comp) |
55 | | retop 23514 |
. . . . . . 7
⊢
(topGen‘ran (,)) ∈ Top |
56 | 3, 55 | eqeltri 2829 |
. . . . . 6
⊢ 𝐾 ∈ Top |
57 | 6 | cmpsub 22151 |
. . . . . 6
⊢ ((𝐾 ∈ Top ∧ ran 𝐹 ⊆ ℝ) → ((𝐾 ↾t ran 𝐹) ∈ Comp ↔
∀𝑢 ∈ 𝒫
𝐾(ran 𝐹 ⊆ ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 ⊆ ∪ 𝑣))) |
58 | 56, 9, 57 | sylancr 590 |
. . . . 5
⊢ (𝜑 → ((𝐾 ↾t ran 𝐹) ∈ Comp ↔ ∀𝑢 ∈ 𝒫 𝐾(ran 𝐹 ⊆ ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 ⊆ ∪ 𝑣))) |
59 | 54, 58 | mpbid 235 |
. . . 4
⊢ (𝜑 → ∀𝑢 ∈ 𝒫 𝐾(ran 𝐹 ⊆ ∪ 𝑢 → ∃𝑣 ∈ (𝒫 𝑢 ∩ Fin)ran 𝐹 ⊆ ∪ 𝑣)) |
60 | | retopbas 23513 |
. . . . . . . . 9
⊢ ran (,)
∈ TopBases |
61 | | bastg 21717 |
. . . . . . . . 9
⊢ (ran (,)
∈ TopBases → ran (,) ⊆ (topGen‘ran (,))) |
62 | 60, 61 | ax-mp 5 |
. . . . . . . 8
⊢ ran (,)
⊆ (topGen‘ran (,)) |
63 | 62, 3 | sseqtrri 3914 |
. . . . . . 7
⊢ ran (,)
⊆ 𝐾 |
64 | 11, 63 | sstri 3886 |
. . . . . 6
⊢ ((,)
“ ({-∞} × ℝ)) ⊆ 𝐾 |
65 | 56, 64 | elpwi2 5214 |
. . . . 5
⊢ ((,)
“ ({-∞} × ℝ)) ∈ 𝒫 𝐾 |
66 | 65 | a1i 11 |
. . . 4
⊢ (𝜑 → ((,) “ ({-∞}
× ℝ)) ∈ 𝒫 𝐾) |
67 | 51, 59, 66 | rspcdva 3528 |
. . 3
⊢ (𝜑 → (ran 𝐹 ⊆ ℝ → ∃𝑣 ∈ (𝒫 ((,) “
({-∞} × ℝ)) ∩ Fin)ran 𝐹 ⊆ ∪ 𝑣)) |
68 | 9, 67 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)ran 𝐹 ⊆ ∪ 𝑣) |
69 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) → 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) |
70 | | elin 3859 |
. . . . . . 7
⊢ (𝑣 ∈ (𝒫 ((,) “
({-∞} × ℝ)) ∩ Fin) ↔ (𝑣 ∈ 𝒫 ((,) “ ({-∞}
× ℝ)) ∧ 𝑣
∈ Fin)) |
71 | 69, 70 | sylib 221 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) → (𝑣 ∈ 𝒫 ((,) “ ({-∞}
× ℝ)) ∧ 𝑣
∈ Fin)) |
72 | 71 | adantrr 717 |
. . . . 5
⊢ ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin) ∧ ran 𝐹 ⊆ ∪ 𝑣)) → (𝑣 ∈ 𝒫 ((,) “ ({-∞}
× ℝ)) ∧ 𝑣
∈ Fin)) |
73 | 72 | simprd 499 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin) ∧ ran 𝐹 ⊆ ∪ 𝑣)) → 𝑣 ∈ Fin) |
74 | 71 | simpld 498 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) → 𝑣 ∈ 𝒫 ((,) “ ({-∞}
× ℝ))) |
75 | 74 | elpwid 4499 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) → 𝑣 ⊆ ((,) “ ({-∞} ×
ℝ))) |
76 | 33 | sseli 3873 |
. . . . . . . . . . . 12
⊢ (𝑢 ∈ {-∞} → 𝑢 ∈
ℝ*) |
77 | 76 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → 𝑢 ∈
ℝ*) |
78 | 17 | sseli 3873 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ ℝ → 𝑤 ∈
ℝ*) |
79 | 78 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → 𝑤 ∈
ℝ*) |
80 | | mnflt 12601 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℝ → -∞
< 𝑤) |
81 | | xrltnle 10786 |
. . . . . . . . . . . . . . . 16
⊢
((-∞ ∈ ℝ* ∧ 𝑤 ∈ ℝ*) → (-∞
< 𝑤 ↔ ¬ 𝑤 ≤
-∞)) |
82 | 24, 78, 81 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ℝ → (-∞
< 𝑤 ↔ ¬ 𝑤 ≤
-∞)) |
83 | 80, 82 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ℝ → ¬
𝑤 ≤
-∞) |
84 | 83 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → ¬
𝑤 ≤
-∞) |
85 | | elsni 4533 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ {-∞} → 𝑢 = -∞) |
86 | 85 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → 𝑢 = -∞) |
87 | 86 | breq2d 5042 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → (𝑤 ≤ 𝑢 ↔ 𝑤 ≤ -∞)) |
88 | 84, 87 | mtbird 328 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → ¬
𝑤 ≤ 𝑢) |
89 | | ioo0 12846 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → ((𝑢(,)𝑤) = ∅ ↔ 𝑤 ≤ 𝑢)) |
90 | 76, 78, 89 | syl2an 599 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → ((𝑢(,)𝑤) = ∅ ↔ 𝑤 ≤ 𝑢)) |
91 | 90 | necon3abid 2970 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → ((𝑢(,)𝑤) ≠ ∅ ↔ ¬ 𝑤 ≤ 𝑢)) |
92 | 88, 91 | mpbird 260 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → (𝑢(,)𝑤) ≠ ∅) |
93 | | df-ioo 12825 |
. . . . . . . . . . . 12
⊢ (,) =
(𝑦 ∈
ℝ*, 𝑧
∈ ℝ* ↦ {𝑣 ∈ ℝ* ∣ (𝑦 < 𝑣 ∧ 𝑣 < 𝑧)}) |
94 | | idd 24 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝑥 < 𝑤 → 𝑥 < 𝑤)) |
95 | | xrltle 12625 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ*
∧ 𝑤 ∈
ℝ*) → (𝑥 < 𝑤 → 𝑥 ≤ 𝑤)) |
96 | | idd 24 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (𝑢 < 𝑥 → 𝑢 < 𝑥)) |
97 | | xrltle 12625 |
. . . . . . . . . . . 12
⊢ ((𝑢 ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → (𝑢 < 𝑥 → 𝑢 ≤ 𝑥)) |
98 | 93, 94, 95, 96, 97 | ixxub 12842 |
. . . . . . . . . . 11
⊢ ((𝑢 ∈ ℝ*
∧ 𝑤 ∈
ℝ* ∧ (𝑢(,)𝑤) ≠ ∅) → sup((𝑢(,)𝑤), ℝ*, < ) = 𝑤) |
99 | 77, 79, 92, 98 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) →
sup((𝑢(,)𝑤), ℝ*, < ) = 𝑤) |
100 | | simpr 488 |
. . . . . . . . . 10
⊢ ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) → 𝑤 ∈
ℝ) |
101 | 99, 100 | eqeltrd 2833 |
. . . . . . . . 9
⊢ ((𝑢 ∈ {-∞} ∧ 𝑤 ∈ ℝ) →
sup((𝑢(,)𝑤), ℝ*, < ) ∈
ℝ) |
102 | 101 | rgen2 3115 |
. . . . . . . 8
⊢
∀𝑢 ∈
{-∞}∀𝑤 ∈
ℝ sup((𝑢(,)𝑤), ℝ*, < )
∈ ℝ |
103 | | fveq2 6674 |
. . . . . . . . . . . 12
⊢ (𝑧 = 〈𝑢, 𝑤〉 → ((,)‘𝑧) = ((,)‘〈𝑢, 𝑤〉)) |
104 | | df-ov 7173 |
. . . . . . . . . . . 12
⊢ (𝑢(,)𝑤) = ((,)‘〈𝑢, 𝑤〉) |
105 | 103, 104 | eqtr4di 2791 |
. . . . . . . . . . 11
⊢ (𝑧 = 〈𝑢, 𝑤〉 → ((,)‘𝑧) = (𝑢(,)𝑤)) |
106 | 105 | supeq1d 8983 |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑢, 𝑤〉 → sup(((,)‘𝑧), ℝ*, < ) =
sup((𝑢(,)𝑤), ℝ*, <
)) |
107 | 106 | eleq1d 2817 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑢, 𝑤〉 → (sup(((,)‘𝑧), ℝ*, < )
∈ ℝ ↔ sup((𝑢(,)𝑤), ℝ*, < ) ∈
ℝ)) |
108 | 107 | ralxp 5684 |
. . . . . . . 8
⊢
(∀𝑧 ∈
({-∞} × ℝ)sup(((,)‘𝑧), ℝ*, < ) ∈ ℝ
↔ ∀𝑢 ∈
{-∞}∀𝑤 ∈
ℝ sup((𝑢(,)𝑤), ℝ*, < )
∈ ℝ) |
109 | 102, 108 | mpbir 234 |
. . . . . . 7
⊢
∀𝑧 ∈
({-∞} × ℝ)sup(((,)‘𝑧), ℝ*, < ) ∈
ℝ |
110 | | ffn 6504 |
. . . . . . . . 9
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
111 | 29, 110 | ax-mp 5 |
. . . . . . . 8
⊢ (,) Fn
(ℝ* × ℝ*) |
112 | | supeq1 8982 |
. . . . . . . . . 10
⊢ (𝑤 = ((,)‘𝑧) → sup(𝑤, ℝ*, < ) =
sup(((,)‘𝑧),
ℝ*, < )) |
113 | 112 | eleq1d 2817 |
. . . . . . . . 9
⊢ (𝑤 = ((,)‘𝑧) → (sup(𝑤, ℝ*, < ) ∈ ℝ
↔ sup(((,)‘𝑧),
ℝ*, < ) ∈ ℝ)) |
114 | 113 | ralima 7011 |
. . . . . . . 8
⊢ (((,) Fn
(ℝ* × ℝ*) ∧ ({-∞} ×
ℝ) ⊆ (ℝ* × ℝ*)) →
(∀𝑤 ∈ ((,)
“ ({-∞} × ℝ))sup(𝑤, ℝ*, < ) ∈ ℝ
↔ ∀𝑧 ∈
({-∞} × ℝ)sup(((,)‘𝑧), ℝ*, < ) ∈
ℝ)) |
115 | 111, 35, 114 | mp2an 692 |
. . . . . . 7
⊢
(∀𝑤 ∈
((,) “ ({-∞} × ℝ))sup(𝑤, ℝ*, < ) ∈ ℝ
↔ ∀𝑧 ∈
({-∞} × ℝ)sup(((,)‘𝑧), ℝ*, < ) ∈
ℝ) |
116 | 109, 115 | mpbir 234 |
. . . . . 6
⊢
∀𝑤 ∈
((,) “ ({-∞} × ℝ))sup(𝑤, ℝ*, < ) ∈
ℝ |
117 | | ssralv 3943 |
. . . . . 6
⊢ (𝑣 ⊆ ((,) “
({-∞} × ℝ)) → (∀𝑤 ∈ ((,) “ ({-∞} ×
ℝ))sup(𝑤,
ℝ*, < ) ∈ ℝ → ∀𝑤 ∈ 𝑣 sup(𝑤, ℝ*, < ) ∈
ℝ)) |
118 | 75, 116, 117 | mpisyl 21 |
. . . . 5
⊢ ((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) → ∀𝑤 ∈ 𝑣 sup(𝑤, ℝ*, < ) ∈
ℝ) |
119 | 118 | adantrr 717 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin) ∧ ran 𝐹 ⊆ ∪ 𝑣)) → ∀𝑤 ∈ 𝑣 sup(𝑤, ℝ*, < ) ∈
ℝ) |
120 | | fimaxre3 11664 |
. . . 4
⊢ ((𝑣 ∈ Fin ∧ ∀𝑤 ∈ 𝑣 sup(𝑤, ℝ*, < ) ∈ ℝ)
→ ∃𝑥 ∈
ℝ ∀𝑤 ∈
𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥) |
121 | 73, 119, 120 | syl2anc 587 |
. . 3
⊢ ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin) ∧ ran 𝐹 ⊆ ∪ 𝑣)) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥) |
122 | | simplrr 778 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin) ∧ ran 𝐹 ⊆ ∪ 𝑣)) ∧ 𝑥 ∈ ℝ) → ran 𝐹 ⊆ ∪ 𝑣) |
123 | 122 | sselda 3877 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin) ∧ ran 𝐹 ⊆ ∪ 𝑣)) ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ran 𝐹) → 𝑧 ∈ ∪ 𝑣) |
124 | | eluni2 4800 |
. . . . . . . 8
⊢ (𝑧 ∈ ∪ 𝑣
↔ ∃𝑤 ∈
𝑣 𝑧 ∈ 𝑤) |
125 | | r19.29r 3168 |
. . . . . . . . . 10
⊢
((∃𝑤 ∈
𝑣 𝑧 ∈ 𝑤 ∧ ∀𝑤 ∈ 𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥) → ∃𝑤 ∈ 𝑣 (𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) |
126 | | sspwuni 4985 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((,)
“ ({-∞} × ℝ)) ⊆ 𝒫 ℝ ↔ ∪ ((,) “ ({-∞} × ℝ)) ⊆
ℝ) |
127 | 14, 126 | mpbir 234 |
. . . . . . . . . . . . . . . . . 18
⊢ ((,)
“ ({-∞} × ℝ)) ⊆ 𝒫
ℝ |
128 | 75 | 3ad2ant1 1134 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣) ∧ (𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑣 ⊆ ((,) “ ({-∞} ×
ℝ))) |
129 | | simp2r 1201 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣) ∧ (𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤 ∈ 𝑣) |
130 | 128, 129 | sseldd 3878 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣) ∧ (𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤 ∈ ((,) “ ({-∞} ×
ℝ))) |
131 | 127, 130 | sseldi 3875 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣) ∧ (𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤 ∈ 𝒫 ℝ) |
132 | 131 | elpwid 4499 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣) ∧ (𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤 ⊆ ℝ) |
133 | | simp3l 1202 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣) ∧ (𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑧 ∈ 𝑤) |
134 | 132, 133 | sseldd 3878 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣) ∧ (𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑧 ∈ ℝ) |
135 | 118 | r19.21bi 3121 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ 𝑤 ∈ 𝑣) → sup(𝑤, ℝ*, < ) ∈
ℝ) |
136 | 135 | adantrl 716 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣)) → sup(𝑤, ℝ*, < ) ∈
ℝ) |
137 | 136 | 3adant3 1133 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣) ∧ (𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → sup(𝑤, ℝ*, < ) ∈
ℝ) |
138 | | simp2l 1200 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣) ∧ (𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑥 ∈ ℝ) |
139 | 132, 17 | sstrdi 3889 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣) ∧ (𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑤 ⊆
ℝ*) |
140 | | supxrub 12800 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ⊆ ℝ*
∧ 𝑧 ∈ 𝑤) → 𝑧 ≤ sup(𝑤, ℝ*, <
)) |
141 | 139, 133,
140 | syl2anc 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣) ∧ (𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑧 ≤ sup(𝑤, ℝ*, <
)) |
142 | | simp3r 1203 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣) ∧ (𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → sup(𝑤, ℝ*, < ) ≤ 𝑥) |
143 | 134, 137,
138, 141, 142 | letrd 10875 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣) ∧ (𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥)) → 𝑧 ≤ 𝑥) |
144 | 143 | 3expia 1122 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ (𝑥 ∈ ℝ ∧ 𝑤 ∈ 𝑣)) → ((𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧 ≤ 𝑥)) |
145 | 144 | anassrs 471 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ 𝑥 ∈ ℝ) ∧ 𝑤 ∈ 𝑣) → ((𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧 ≤ 𝑥)) |
146 | 145 | rexlimdva 3194 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin)) ∧ 𝑥 ∈ ℝ) → (∃𝑤 ∈ 𝑣 (𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧 ≤ 𝑥)) |
147 | 146 | adantlrr 721 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin) ∧ ran 𝐹 ⊆ ∪ 𝑣)) ∧ 𝑥 ∈ ℝ) → (∃𝑤 ∈ 𝑣 (𝑧 ∈ 𝑤 ∧ sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧 ≤ 𝑥)) |
148 | 125, 147 | syl5 34 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin) ∧ ran 𝐹 ⊆ ∪ 𝑣)) ∧ 𝑥 ∈ ℝ) → ((∃𝑤 ∈ 𝑣 𝑧 ∈ 𝑤 ∧ ∀𝑤 ∈ 𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥) → 𝑧 ≤ 𝑥)) |
149 | 148 | expdimp 456 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin) ∧ ran 𝐹 ⊆ ∪ 𝑣)) ∧ 𝑥 ∈ ℝ) ∧ ∃𝑤 ∈ 𝑣 𝑧 ∈ 𝑤) → (∀𝑤 ∈ 𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥 → 𝑧 ≤ 𝑥)) |
150 | 124, 149 | sylan2b 597 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin) ∧ ran 𝐹 ⊆ ∪ 𝑣)) ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ∪ 𝑣) → (∀𝑤 ∈ 𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥 → 𝑧 ≤ 𝑥)) |
151 | 123, 150 | syldan 594 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin) ∧ ran 𝐹 ⊆ ∪ 𝑣)) ∧ 𝑥 ∈ ℝ) ∧ 𝑧 ∈ ran 𝐹) → (∀𝑤 ∈ 𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥 → 𝑧 ≤ 𝑥)) |
152 | 151 | ralrimdva 3101 |
. . . . 5
⊢ (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin) ∧ ran 𝐹 ⊆ ∪ 𝑣)) ∧ 𝑥 ∈ ℝ) → (∀𝑤 ∈ 𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥 → ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥)) |
153 | 8 | ffnd 6505 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn 𝑋) |
154 | 153 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin) ∧ ran 𝐹 ⊆ ∪ 𝑣)) ∧ 𝑥 ∈ ℝ) → 𝐹 Fn 𝑋) |
155 | | breq1 5033 |
. . . . . . 7
⊢ (𝑧 = (𝐹‘𝑦) → (𝑧 ≤ 𝑥 ↔ (𝐹‘𝑦) ≤ 𝑥)) |
156 | 155 | ralrn 6864 |
. . . . . 6
⊢ (𝐹 Fn 𝑋 → (∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ↔ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ 𝑥)) |
157 | 154, 156 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin) ∧ ran 𝐹 ⊆ ∪ 𝑣)) ∧ 𝑥 ∈ ℝ) → (∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑥 ↔ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ 𝑥)) |
158 | 152, 157 | sylibd 242 |
. . . 4
⊢ (((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin) ∧ ran 𝐹 ⊆ ∪ 𝑣)) ∧ 𝑥 ∈ ℝ) → (∀𝑤 ∈ 𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥 → ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ 𝑥)) |
159 | 158 | reximdva 3184 |
. . 3
⊢ ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin) ∧ ran 𝐹 ⊆ ∪ 𝑣)) → (∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑣 sup(𝑤, ℝ*, < ) ≤ 𝑥 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ 𝑥)) |
160 | 121, 159 | mpd 15 |
. 2
⊢ ((𝜑 ∧ (𝑣 ∈ (𝒫 ((,) “ ({-∞}
× ℝ)) ∩ Fin) ∧ ran 𝐹 ⊆ ∪ 𝑣)) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ 𝑥) |
161 | 68, 160 | rexlimddv 3201 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝐹‘𝑦) ≤ 𝑥) |