Step | Hyp | Ref
| Expression |
1 | | islptre.1 |
. . . . . 6
⊢ 𝐽 = (topGen‘ran
(,)) |
2 | | retopon 22975 |
. . . . . 6
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
3 | 1, 2 | eqeltri 2854 |
. . . . 5
⊢ 𝐽 ∈
(TopOn‘ℝ) |
4 | 3 | topontopi 21127 |
. . . 4
⊢ 𝐽 ∈ Top |
5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐽 ∈ Top) |
6 | | islptre.2 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
7 | | islptre.3 |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) |
8 | 3 | toponunii 21128 |
. . . 4
⊢ ℝ =
∪ 𝐽 |
9 | 8 | islp2 21357 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
10 | 5, 6, 7, 9 | syl3anc 1439 |
. 2
⊢ (𝜑 → (𝐵 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
11 | | simp1r 1212 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*)
∧ 𝐵 ∈ (𝑎(,)𝑏)) → ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
12 | | iooretop 22977 |
. . . . . . . . . . . 12
⊢ (𝑎(,)𝑏) ∈ (topGen‘ran
(,)) |
13 | 12, 1 | eleqtrri 2857 |
. . . . . . . . . . 11
⊢ (𝑎(,)𝑏) ∈ 𝐽 |
14 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → (𝑎(,)𝑏) ∈ 𝐽) |
15 | | snssi 4570 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (𝑎(,)𝑏) → {𝐵} ⊆ (𝑎(,)𝑏)) |
16 | 15 | adantl 475 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → {𝐵} ⊆ (𝑎(,)𝑏)) |
17 | | ssidd 3842 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → (𝑎(,)𝑏) ⊆ (𝑎(,)𝑏)) |
18 | | sseq2 3845 |
. . . . . . . . . . . 12
⊢ (𝑣 = (𝑎(,)𝑏) → ({𝐵} ⊆ 𝑣 ↔ {𝐵} ⊆ (𝑎(,)𝑏))) |
19 | | sseq1 3844 |
. . . . . . . . . . . 12
⊢ (𝑣 = (𝑎(,)𝑏) → (𝑣 ⊆ (𝑎(,)𝑏) ↔ (𝑎(,)𝑏) ⊆ (𝑎(,)𝑏))) |
20 | 18, 19 | anbi12d 624 |
. . . . . . . . . . 11
⊢ (𝑣 = (𝑎(,)𝑏) → (({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏)) ↔ ({𝐵} ⊆ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑎(,)𝑏)))) |
21 | 20 | rspcev 3510 |
. . . . . . . . . 10
⊢ (((𝑎(,)𝑏) ∈ 𝐽 ∧ ({𝐵} ⊆ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑎(,)𝑏))) → ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏))) |
22 | 14, 16, 17, 21 | syl12anc 827 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏))) |
23 | | ioossre 12547 |
. . . . . . . . 9
⊢ (𝑎(,)𝑏) ⊆ ℝ |
24 | 22, 23 | jctil 515 |
. . . . . . . 8
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ⊆ ℝ ∧ ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏)))) |
25 | | elioore 12517 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (𝑎(,)𝑏) → 𝐵 ∈ ℝ) |
26 | 25 | snssd 4571 |
. . . . . . . . . 10
⊢ (𝐵 ∈ (𝑎(,)𝑏) → {𝐵} ⊆ ℝ) |
27 | 26 | adantl 475 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → {𝐵} ⊆ ℝ) |
28 | 8 | isnei 21315 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ {𝐵} ⊆ ℝ) →
((𝑎(,)𝑏) ∈ ((nei‘𝐽)‘{𝐵}) ↔ ((𝑎(,)𝑏) ⊆ ℝ ∧ ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏))))) |
29 | 4, 27, 28 | sylancr 581 |
. . . . . . . 8
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∈ ((nei‘𝐽)‘{𝐵}) ↔ ((𝑎(,)𝑏) ⊆ ℝ ∧ ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏))))) |
30 | 24, 29 | mpbird 249 |
. . . . . . 7
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → (𝑎(,)𝑏) ∈ ((nei‘𝐽)‘{𝐵})) |
31 | 30 | 3adant1 1121 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*)
∧ 𝐵 ∈ (𝑎(,)𝑏)) → (𝑎(,)𝑏) ∈ ((nei‘𝐽)‘{𝐵})) |
32 | | ineq1 4029 |
. . . . . . . 8
⊢ (𝑛 = (𝑎(,)𝑏) → (𝑛 ∩ (𝐴 ∖ {𝐵})) = ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵}))) |
33 | 32 | neeq1d 3027 |
. . . . . . 7
⊢ (𝑛 = (𝑎(,)𝑏) → ((𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅ ↔ ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
34 | 33 | rspccva 3509 |
. . . . . 6
⊢
((∀𝑛 ∈
((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅ ∧ (𝑎(,)𝑏) ∈ ((nei‘𝐽)‘{𝐵})) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
35 | 11, 31, 34 | syl2anc 579 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*)
∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
36 | 35 | 3exp 1109 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) → ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |
37 | 36 | ralrimivv 3151 |
. . 3
⊢ ((𝜑 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) → ∀𝑎 ∈ ℝ*
∀𝑏 ∈
ℝ* (𝐵
∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
38 | 7 | snssd 4571 |
. . . . . . . . 9
⊢ (𝜑 → {𝐵} ⊆ ℝ) |
39 | 8 | isnei 21315 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ {𝐵} ⊆ ℝ) → (𝑛 ∈ ((nei‘𝐽)‘{𝐵}) ↔ (𝑛 ⊆ ℝ ∧ ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)))) |
40 | 4, 38, 39 | sylancr 581 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ ((nei‘𝐽)‘{𝐵}) ↔ (𝑛 ⊆ ℝ ∧ ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)))) |
41 | 40 | simplbda 495 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) |
42 | 1 | eleq2i 2850 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ 𝐽 ↔ 𝑣 ∈ (topGen‘ran
(,))) |
43 | 42 | biimpi 208 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ 𝐽 → 𝑣 ∈ (topGen‘ran
(,))) |
44 | 43 | 3ad2ant2 1125 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → 𝑣 ∈ (topGen‘ran
(,))) |
45 | | simp1 1127 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → 𝜑) |
46 | | simp3l 1215 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → {𝐵} ⊆ 𝑣) |
47 | | simpr 479 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ {𝐵} ⊆ 𝑣) → {𝐵} ⊆ 𝑣) |
48 | 7 | adantr 474 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ {𝐵} ⊆ 𝑣) → 𝐵 ∈ ℝ) |
49 | | snssg 4547 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ ℝ → (𝐵 ∈ 𝑣 ↔ {𝐵} ⊆ 𝑣)) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ {𝐵} ⊆ 𝑣) → (𝐵 ∈ 𝑣 ↔ {𝐵} ⊆ 𝑣)) |
51 | 47, 50 | mpbird 249 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ {𝐵} ⊆ 𝑣) → 𝐵 ∈ 𝑣) |
52 | 45, 46, 51 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → 𝐵 ∈ 𝑣) |
53 | 44, 52 | jca 507 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → (𝑣 ∈ (topGen‘ran (,)) ∧ 𝐵 ∈ 𝑣)) |
54 | | tg2 21177 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ (topGen‘ran (,))
∧ 𝐵 ∈ 𝑣) → ∃𝑢 ∈ ran (,)(𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) |
55 | | ioof 12584 |
. . . . . . . . . . . . . . . . 17
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
56 | | ffn 6291 |
. . . . . . . . . . . . . . . . 17
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
57 | | ovelrn 7087 |
. . . . . . . . . . . . . . . . 17
⊢ ((,) Fn
(ℝ* × ℝ*) → (𝑢 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ*
∃𝑏 ∈
ℝ* 𝑢 =
(𝑎(,)𝑏))) |
58 | 55, 56, 57 | mp2b 10 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ran (,) ↔
∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑢 = (𝑎(,)𝑏)) |
59 | 58 | biimpi 208 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ran (,) →
∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑢 = (𝑎(,)𝑏)) |
60 | 59 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ ran (,) ∧ (𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
𝑢 = (𝑎(,)𝑏)) |
61 | | simpll 757 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → 𝐵 ∈ 𝑢) |
62 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → 𝑢 = (𝑎(,)𝑏)) |
63 | 61, 62 | eleqtrd 2860 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → 𝐵 ∈ (𝑎(,)𝑏)) |
64 | | simplr 759 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → 𝑢 ⊆ 𝑣) |
65 | 62, 64 | eqsstr3d 3858 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → (𝑎(,)𝑏) ⊆ 𝑣) |
66 | 63, 65 | jca 507 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) |
67 | 66 | ex 403 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) → (𝑢 = (𝑎(,)𝑏) → (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣))) |
68 | 67 | adantl 475 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ran (,) ∧ (𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) → (𝑢 = (𝑎(,)𝑏) → (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣))) |
69 | 68 | reximdv 3196 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ ran (,) ∧ (𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) → (∃𝑏 ∈ ℝ* 𝑢 = (𝑎(,)𝑏) → ∃𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣))) |
70 | 69 | reximdv 3196 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ ran (,) ∧ (𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) → (∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
𝑢 = (𝑎(,)𝑏) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣))) |
71 | 60, 70 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ ran (,) ∧ (𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) |
72 | 71 | rexlimiva 3209 |
. . . . . . . . . . . 12
⊢
(∃𝑢 ∈ ran
(,)(𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) |
73 | 53, 54, 72 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) |
74 | | simpl3r 1260 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) ∧ 𝑎 ∈ ℝ*) → 𝑣 ⊆ 𝑛) |
75 | 74 | adantr 474 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*)
→ 𝑣 ⊆ 𝑛) |
76 | | sstr 3828 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎(,)𝑏) ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛) → (𝑎(,)𝑏) ⊆ 𝑛) |
77 | 76 | expcom 404 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ⊆ 𝑛 → ((𝑎(,)𝑏) ⊆ 𝑣 → (𝑎(,)𝑏) ⊆ 𝑛)) |
78 | 75, 77 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*)
→ ((𝑎(,)𝑏) ⊆ 𝑣 → (𝑎(,)𝑏) ⊆ 𝑛)) |
79 | 78 | anim2d 605 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*)
→ ((𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣) → (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛))) |
80 | 79 | reximdva 3197 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) ∧ 𝑎 ∈ ℝ*) →
(∃𝑏 ∈
ℝ* (𝐵
∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣) → ∃𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛))) |
81 | 80 | reximdva 3197 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → (∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛))) |
82 | 73, 81 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) |
83 | 82 | 3exp 1109 |
. . . . . . . . 9
⊢ (𝜑 → (𝑣 ∈ 𝐽 → (({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)))) |
84 | 83 | rexlimdv 3211 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛))) |
85 | 84 | adantr 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → (∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛))) |
86 | 41, 85 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) |
87 | 86 | adantlr 705 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) |
88 | | nfv 1957 |
. . . . . . . 8
⊢
Ⅎ𝑎𝜑 |
89 | | nfra1 3122 |
. . . . . . . 8
⊢
Ⅎ𝑎∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
90 | 88, 89 | nfan 1946 |
. . . . . . 7
⊢
Ⅎ𝑎(𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
91 | | nfv 1957 |
. . . . . . 7
⊢
Ⅎ𝑎 𝑛 ∈ ((nei‘𝐽)‘{𝐵}) |
92 | 90, 91 | nfan 1946 |
. . . . . 6
⊢
Ⅎ𝑎((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) |
93 | | nfv 1957 |
. . . . . 6
⊢
Ⅎ𝑎(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅ |
94 | | nfv 1957 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏𝜑 |
95 | | nfra2 3127 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
96 | 94, 95 | nfan 1946 |
. . . . . . . . . 10
⊢
Ⅎ𝑏(𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
97 | | nfv 1957 |
. . . . . . . . . 10
⊢
Ⅎ𝑏 𝑛 ∈ ((nei‘𝐽)‘{𝐵}) |
98 | 96, 97 | nfan 1946 |
. . . . . . . . 9
⊢
Ⅎ𝑏((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) |
99 | | nfv 1957 |
. . . . . . . . 9
⊢
Ⅎ𝑏 𝑎 ∈
ℝ* |
100 | 98, 99 | nfan 1946 |
. . . . . . . 8
⊢
Ⅎ𝑏(((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) |
101 | | nfv 1957 |
. . . . . . . 8
⊢
Ⅎ𝑏(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅ |
102 | | inss1 4052 |
. . . . . . . . . . . 12
⊢ ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑎(,)𝑏) |
103 | | simp3r 1216 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → (𝑎(,)𝑏) ⊆ 𝑛) |
104 | 102, 103 | syl5ss 3831 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ 𝑛) |
105 | | inss2 4053 |
. . . . . . . . . . . 12
⊢ ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝐴 ∖ {𝐵}) |
106 | 105 | a1i 11 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝐴 ∖ {𝐵})) |
107 | 104, 106 | ssind 4056 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑛 ∩ (𝐴 ∖ {𝐵}))) |
108 | | simpllr 766 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) →
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
109 | 108 | 3ad2ant1 1124 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
110 | | simp1r 1212 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → 𝑎 ∈ ℝ*) |
111 | | simp2 1128 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → 𝑏 ∈ ℝ*) |
112 | 110, 111 | jca 507 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → (𝑎 ∈ ℝ* ∧ 𝑏 ∈
ℝ*)) |
113 | | simp3l 1215 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → 𝐵 ∈ (𝑎(,)𝑏)) |
114 | | rsp2 3117 |
. . . . . . . . . . 11
⊢
(∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) → ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |
115 | 109, 112,
113, 114 | syl3c 66 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
116 | | ssn0 4201 |
. . . . . . . . . 10
⊢ ((((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑛 ∩ (𝐴 ∖ {𝐵})) ∧ ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
117 | 107, 115,
116 | syl2anc 579 |
. . . . . . . . 9
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
118 | 117 | 3exp 1109 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) → (𝑏 ∈ ℝ*
→ ((𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |
119 | 100, 101,
118 | rexlimd 3207 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) →
(∃𝑏 ∈
ℝ* (𝐵
∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
120 | 119 | ex 403 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → (𝑎 ∈ ℝ* →
(∃𝑏 ∈
ℝ* (𝐵
∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |
121 | 92, 93, 120 | rexlimd 3207 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → (∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
122 | 87, 121 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
123 | 122 | ralrimiva 3147 |
. . 3
⊢ ((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) → ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
124 | 37, 123 | impbida 791 |
. 2
⊢ (𝜑 → (∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅ ↔ ∀𝑎 ∈ ℝ*
∀𝑏 ∈
ℝ* (𝐵
∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |
125 | 10, 124 | bitrd 271 |
1
⊢ (𝜑 → (𝐵 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |