Step | Hyp | Ref
| Expression |
1 | | islptre.1 |
. . . . . 6
⊢ 𝐽 = (topGen‘ran
(,)) |
2 | | retopon 22567 |
. . . . . 6
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
3 | 1, 2 | eqeltri 2697 |
. . . . 5
⊢ 𝐽 ∈
(TopOn‘ℝ) |
4 | 3 | topontopi 20720 |
. . . 4
⊢ 𝐽 ∈ Top |
5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐽 ∈ Top) |
6 | | islptre.2 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
7 | | islptre.3 |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) |
8 | 3 | toponunii 20721 |
. . . 4
⊢ ℝ =
∪ 𝐽 |
9 | 8 | islp2 20949 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
10 | 5, 6, 7, 9 | syl3anc 1326 |
. 2
⊢ (𝜑 → (𝐵 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
11 | | simp1r 1086 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*)
∧ 𝐵 ∈ (𝑎(,)𝑏)) → ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
12 | | iooretop 22569 |
. . . . . . . . . . . 12
⊢ (𝑎(,)𝑏) ∈ (topGen‘ran
(,)) |
13 | 12, 1 | eleqtrri 2700 |
. . . . . . . . . . 11
⊢ (𝑎(,)𝑏) ∈ 𝐽 |
14 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → (𝑎(,)𝑏) ∈ 𝐽) |
15 | | snssi 4339 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (𝑎(,)𝑏) → {𝐵} ⊆ (𝑎(,)𝑏)) |
16 | 15 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → {𝐵} ⊆ (𝑎(,)𝑏)) |
17 | | ssid 3624 |
. . . . . . . . . . 11
⊢ (𝑎(,)𝑏) ⊆ (𝑎(,)𝑏) |
18 | 17 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → (𝑎(,)𝑏) ⊆ (𝑎(,)𝑏)) |
19 | | sseq2 3627 |
. . . . . . . . . . . 12
⊢ (𝑣 = (𝑎(,)𝑏) → ({𝐵} ⊆ 𝑣 ↔ {𝐵} ⊆ (𝑎(,)𝑏))) |
20 | | sseq1 3626 |
. . . . . . . . . . . 12
⊢ (𝑣 = (𝑎(,)𝑏) → (𝑣 ⊆ (𝑎(,)𝑏) ↔ (𝑎(,)𝑏) ⊆ (𝑎(,)𝑏))) |
21 | 19, 20 | anbi12d 747 |
. . . . . . . . . . 11
⊢ (𝑣 = (𝑎(,)𝑏) → (({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏)) ↔ ({𝐵} ⊆ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑎(,)𝑏)))) |
22 | 21 | rspcev 3309 |
. . . . . . . . . 10
⊢ (((𝑎(,)𝑏) ∈ 𝐽 ∧ ({𝐵} ⊆ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑎(,)𝑏))) → ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏))) |
23 | 14, 16, 18, 22 | syl12anc 1324 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏))) |
24 | | ioossre 12235 |
. . . . . . . . 9
⊢ (𝑎(,)𝑏) ⊆ ℝ |
25 | 23, 24 | jctil 560 |
. . . . . . . 8
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ⊆ ℝ ∧ ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏)))) |
26 | | elioore 12205 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (𝑎(,)𝑏) → 𝐵 ∈ ℝ) |
27 | 26 | snssd 4340 |
. . . . . . . . . 10
⊢ (𝐵 ∈ (𝑎(,)𝑏) → {𝐵} ⊆ ℝ) |
28 | 27 | adantl 482 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → {𝐵} ⊆ ℝ) |
29 | 8 | isnei 20907 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ {𝐵} ⊆ ℝ) →
((𝑎(,)𝑏) ∈ ((nei‘𝐽)‘{𝐵}) ↔ ((𝑎(,)𝑏) ⊆ ℝ ∧ ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏))))) |
30 | 4, 28, 29 | sylancr 695 |
. . . . . . . 8
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∈ ((nei‘𝐽)‘{𝐵}) ↔ ((𝑎(,)𝑏) ⊆ ℝ ∧ ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏))))) |
31 | 25, 30 | mpbird 247 |
. . . . . . 7
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → (𝑎(,)𝑏) ∈ ((nei‘𝐽)‘{𝐵})) |
32 | 31 | 3adant1 1079 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*)
∧ 𝐵 ∈ (𝑎(,)𝑏)) → (𝑎(,)𝑏) ∈ ((nei‘𝐽)‘{𝐵})) |
33 | | ineq1 3807 |
. . . . . . . 8
⊢ (𝑛 = (𝑎(,)𝑏) → (𝑛 ∩ (𝐴 ∖ {𝐵})) = ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵}))) |
34 | 33 | neeq1d 2853 |
. . . . . . 7
⊢ (𝑛 = (𝑎(,)𝑏) → ((𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅ ↔ ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
35 | 34 | rspccva 3308 |
. . . . . 6
⊢
((∀𝑛 ∈
((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅ ∧ (𝑎(,)𝑏) ∈ ((nei‘𝐽)‘{𝐵})) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
36 | 11, 32, 35 | syl2anc 693 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*)
∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
37 | 36 | 3exp 1264 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) → ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |
38 | 37 | ralrimivv 2970 |
. . 3
⊢ ((𝜑 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) → ∀𝑎 ∈ ℝ*
∀𝑏 ∈
ℝ* (𝐵
∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
39 | 7 | snssd 4340 |
. . . . . . . . 9
⊢ (𝜑 → {𝐵} ⊆ ℝ) |
40 | 8 | isnei 20907 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ {𝐵} ⊆ ℝ) → (𝑛 ∈ ((nei‘𝐽)‘{𝐵}) ↔ (𝑛 ⊆ ℝ ∧ ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)))) |
41 | 4, 39, 40 | sylancr 695 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ ((nei‘𝐽)‘{𝐵}) ↔ (𝑛 ⊆ ℝ ∧ ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)))) |
42 | 41 | simplbda 654 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) |
43 | 1 | eleq2i 2693 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ 𝐽 ↔ 𝑣 ∈ (topGen‘ran
(,))) |
44 | 43 | biimpi 206 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ 𝐽 → 𝑣 ∈ (topGen‘ran
(,))) |
45 | 44 | 3ad2ant2 1083 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → 𝑣 ∈ (topGen‘ran
(,))) |
46 | | simp1 1061 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → 𝜑) |
47 | | simp3l 1089 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → {𝐵} ⊆ 𝑣) |
48 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ {𝐵} ⊆ 𝑣) → {𝐵} ⊆ 𝑣) |
49 | 7 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ {𝐵} ⊆ 𝑣) → 𝐵 ∈ ℝ) |
50 | | snssg 4327 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ ℝ → (𝐵 ∈ 𝑣 ↔ {𝐵} ⊆ 𝑣)) |
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ {𝐵} ⊆ 𝑣) → (𝐵 ∈ 𝑣 ↔ {𝐵} ⊆ 𝑣)) |
52 | 48, 51 | mpbird 247 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ {𝐵} ⊆ 𝑣) → 𝐵 ∈ 𝑣) |
53 | 46, 47, 52 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → 𝐵 ∈ 𝑣) |
54 | 45, 53 | jca 554 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → (𝑣 ∈ (topGen‘ran (,)) ∧ 𝐵 ∈ 𝑣)) |
55 | | tg2 20769 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ (topGen‘ran (,))
∧ 𝐵 ∈ 𝑣) → ∃𝑢 ∈ ran (,)(𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) |
56 | | ioof 12271 |
. . . . . . . . . . . . . . . . 17
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
57 | | ffn 6045 |
. . . . . . . . . . . . . . . . 17
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
58 | | ovelrn 6810 |
. . . . . . . . . . . . . . . . 17
⊢ ((,) Fn
(ℝ* × ℝ*) → (𝑢 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ*
∃𝑏 ∈
ℝ* 𝑢 =
(𝑎(,)𝑏))) |
59 | 56, 57, 58 | mp2b 10 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ran (,) ↔
∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑢 = (𝑎(,)𝑏)) |
60 | 59 | biimpi 206 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ran (,) →
∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑢 = (𝑎(,)𝑏)) |
61 | 60 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ ran (,) ∧ (𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
𝑢 = (𝑎(,)𝑏)) |
62 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → 𝐵 ∈ 𝑢) |
63 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → 𝑢 = (𝑎(,)𝑏)) |
64 | 62, 63 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → 𝐵 ∈ (𝑎(,)𝑏)) |
65 | | simplr 792 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → 𝑢 ⊆ 𝑣) |
66 | 63, 65 | eqsstr3d 3640 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → (𝑎(,)𝑏) ⊆ 𝑣) |
67 | 64, 66 | jca 554 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) |
68 | 67 | ex 450 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) → (𝑢 = (𝑎(,)𝑏) → (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣))) |
69 | 68 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ran (,) ∧ (𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) → (𝑢 = (𝑎(,)𝑏) → (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣))) |
70 | 69 | reximdv 3016 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ ran (,) ∧ (𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) → (∃𝑏 ∈ ℝ* 𝑢 = (𝑎(,)𝑏) → ∃𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣))) |
71 | 70 | reximdv 3016 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ ran (,) ∧ (𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) → (∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
𝑢 = (𝑎(,)𝑏) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣))) |
72 | 61, 71 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ ran (,) ∧ (𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) |
73 | 72 | rexlimiva 3028 |
. . . . . . . . . . . 12
⊢
(∃𝑢 ∈ ran
(,)(𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) |
74 | 54, 55, 73 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) |
75 | | simpl3r 1117 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) ∧ 𝑎 ∈ ℝ*) → 𝑣 ⊆ 𝑛) |
76 | 75 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*)
→ 𝑣 ⊆ 𝑛) |
77 | | sstr 3611 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎(,)𝑏) ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛) → (𝑎(,)𝑏) ⊆ 𝑛) |
78 | 77 | expcom 451 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ⊆ 𝑛 → ((𝑎(,)𝑏) ⊆ 𝑣 → (𝑎(,)𝑏) ⊆ 𝑛)) |
79 | 76, 78 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*)
→ ((𝑎(,)𝑏) ⊆ 𝑣 → (𝑎(,)𝑏) ⊆ 𝑛)) |
80 | 79 | anim2d 589 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*)
→ ((𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣) → (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛))) |
81 | 80 | reximdva 3017 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) ∧ 𝑎 ∈ ℝ*) →
(∃𝑏 ∈
ℝ* (𝐵
∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣) → ∃𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛))) |
82 | 81 | reximdva 3017 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → (∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛))) |
83 | 74, 82 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) |
84 | 83 | 3exp 1264 |
. . . . . . . . 9
⊢ (𝜑 → (𝑣 ∈ 𝐽 → (({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)))) |
85 | 84 | rexlimdv 3030 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛))) |
86 | 85 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → (∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛))) |
87 | 42, 86 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) |
88 | 87 | adantlr 751 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) |
89 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑎𝜑 |
90 | | nfra1 2941 |
. . . . . . . 8
⊢
Ⅎ𝑎∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
91 | 89, 90 | nfan 1828 |
. . . . . . 7
⊢
Ⅎ𝑎(𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
92 | | nfv 1843 |
. . . . . . 7
⊢
Ⅎ𝑎 𝑛 ∈ ((nei‘𝐽)‘{𝐵}) |
93 | 91, 92 | nfan 1828 |
. . . . . 6
⊢
Ⅎ𝑎((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) |
94 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑎(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅ |
95 | | nfv 1843 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏𝜑 |
96 | | nfra2 2946 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
97 | 95, 96 | nfan 1828 |
. . . . . . . . . 10
⊢
Ⅎ𝑏(𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
98 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑏 𝑛 ∈ ((nei‘𝐽)‘{𝐵}) |
99 | 97, 98 | nfan 1828 |
. . . . . . . . 9
⊢
Ⅎ𝑏((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) |
100 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑏 𝑎 ∈
ℝ* |
101 | 99, 100 | nfan 1828 |
. . . . . . . 8
⊢
Ⅎ𝑏(((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) |
102 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑏(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅ |
103 | | inss1 3833 |
. . . . . . . . . . . 12
⊢ ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑎(,)𝑏) |
104 | | simp3r 1090 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → (𝑎(,)𝑏) ⊆ 𝑛) |
105 | 103, 104 | syl5ss 3614 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ 𝑛) |
106 | | inss2 3834 |
. . . . . . . . . . . 12
⊢ ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝐴 ∖ {𝐵}) |
107 | 106 | a1i 11 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝐴 ∖ {𝐵})) |
108 | 105, 107 | ssind 3837 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑛 ∩ (𝐴 ∖ {𝐵}))) |
109 | | simpllr 799 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) →
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
110 | 109 | 3ad2ant1 1082 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
111 | | simp1r 1086 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → 𝑎 ∈ ℝ*) |
112 | | simp2 1062 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → 𝑏 ∈ ℝ*) |
113 | 111, 112 | jca 554 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → (𝑎 ∈ ℝ* ∧ 𝑏 ∈
ℝ*)) |
114 | | simp3l 1089 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → 𝐵 ∈ (𝑎(,)𝑏)) |
115 | | rsp2 2936 |
. . . . . . . . . . 11
⊢
(∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) → ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |
116 | 110, 113,
114, 115 | syl3c 66 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
117 | | ssn0 3976 |
. . . . . . . . . 10
⊢ ((((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑛 ∩ (𝐴 ∖ {𝐵})) ∧ ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
118 | 108, 116,
117 | syl2anc 693 |
. . . . . . . . 9
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
119 | 118 | 3exp 1264 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) → (𝑏 ∈ ℝ*
→ ((𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |
120 | 101, 102,
119 | rexlimd 3026 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) →
(∃𝑏 ∈
ℝ* (𝐵
∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
121 | 120 | ex 450 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → (𝑎 ∈ ℝ* →
(∃𝑏 ∈
ℝ* (𝐵
∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |
122 | 93, 94, 121 | rexlimd 3026 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → (∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
123 | 88, 122 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
124 | 123 | ralrimiva 2966 |
. . 3
⊢ ((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) → ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
125 | 38, 124 | impbida 877 |
. 2
⊢ (𝜑 → (∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅ ↔ ∀𝑎 ∈ ℝ*
∀𝑏 ∈
ℝ* (𝐵
∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |
126 | 10, 125 | bitrd 268 |
1
⊢ (𝜑 → (𝐵 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |