| Step | Hyp | Ref
| Expression |
| 1 | | islptre.1 |
. . . . . 6
⊢ 𝐽 = (topGen‘ran
(,)) |
| 2 | | retopon 24784 |
. . . . . 6
⊢
(topGen‘ran (,)) ∈ (TopOn‘ℝ) |
| 3 | 1, 2 | eqeltri 2837 |
. . . . 5
⊢ 𝐽 ∈
(TopOn‘ℝ) |
| 4 | 3 | topontopi 22921 |
. . . 4
⊢ 𝐽 ∈ Top |
| 5 | 4 | a1i 11 |
. . 3
⊢ (𝜑 → 𝐽 ∈ Top) |
| 6 | | islptre.2 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
| 7 | | islptre.3 |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 8 | 3 | toponunii 22922 |
. . . 4
⊢ ℝ =
∪ 𝐽 |
| 9 | 8 | islp2 23153 |
. . 3
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
| 10 | 5, 6, 7, 9 | syl3anc 1373 |
. 2
⊢ (𝜑 → (𝐵 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
| 11 | | simp1r 1199 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*)
∧ 𝐵 ∈ (𝑎(,)𝑏)) → ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
| 12 | | iooretop 24786 |
. . . . . . . . . . . 12
⊢ (𝑎(,)𝑏) ∈ (topGen‘ran
(,)) |
| 13 | 12, 1 | eleqtrri 2840 |
. . . . . . . . . . 11
⊢ (𝑎(,)𝑏) ∈ 𝐽 |
| 14 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → (𝑎(,)𝑏) ∈ 𝐽) |
| 15 | | snssi 4808 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (𝑎(,)𝑏) → {𝐵} ⊆ (𝑎(,)𝑏)) |
| 16 | 15 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → {𝐵} ⊆ (𝑎(,)𝑏)) |
| 17 | | ssidd 4007 |
. . . . . . . . . 10
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → (𝑎(,)𝑏) ⊆ (𝑎(,)𝑏)) |
| 18 | | sseq2 4010 |
. . . . . . . . . . . 12
⊢ (𝑣 = (𝑎(,)𝑏) → ({𝐵} ⊆ 𝑣 ↔ {𝐵} ⊆ (𝑎(,)𝑏))) |
| 19 | | sseq1 4009 |
. . . . . . . . . . . 12
⊢ (𝑣 = (𝑎(,)𝑏) → (𝑣 ⊆ (𝑎(,)𝑏) ↔ (𝑎(,)𝑏) ⊆ (𝑎(,)𝑏))) |
| 20 | 18, 19 | anbi12d 632 |
. . . . . . . . . . 11
⊢ (𝑣 = (𝑎(,)𝑏) → (({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏)) ↔ ({𝐵} ⊆ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑎(,)𝑏)))) |
| 21 | 20 | rspcev 3622 |
. . . . . . . . . 10
⊢ (((𝑎(,)𝑏) ∈ 𝐽 ∧ ({𝐵} ⊆ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ (𝑎(,)𝑏))) → ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏))) |
| 22 | 14, 16, 17, 21 | syl12anc 837 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏))) |
| 23 | | ioossre 13448 |
. . . . . . . . 9
⊢ (𝑎(,)𝑏) ⊆ ℝ |
| 24 | 22, 23 | jctil 519 |
. . . . . . . 8
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ⊆ ℝ ∧ ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏)))) |
| 25 | | elioore 13417 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (𝑎(,)𝑏) → 𝐵 ∈ ℝ) |
| 26 | 25 | snssd 4809 |
. . . . . . . . . 10
⊢ (𝐵 ∈ (𝑎(,)𝑏) → {𝐵} ⊆ ℝ) |
| 27 | 26 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → {𝐵} ⊆ ℝ) |
| 28 | 8 | isnei 23111 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ {𝐵} ⊆ ℝ) →
((𝑎(,)𝑏) ∈ ((nei‘𝐽)‘{𝐵}) ↔ ((𝑎(,)𝑏) ⊆ ℝ ∧ ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏))))) |
| 29 | 4, 27, 28 | sylancr 587 |
. . . . . . . 8
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∈ ((nei‘𝐽)‘{𝐵}) ↔ ((𝑎(,)𝑏) ⊆ ℝ ∧ ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ (𝑎(,)𝑏))))) |
| 30 | 24, 29 | mpbird 257 |
. . . . . . 7
⊢ (((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) ∧ 𝐵 ∈ (𝑎(,)𝑏)) → (𝑎(,)𝑏) ∈ ((nei‘𝐽)‘{𝐵})) |
| 31 | 30 | 3adant1 1131 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*)
∧ 𝐵 ∈ (𝑎(,)𝑏)) → (𝑎(,)𝑏) ∈ ((nei‘𝐽)‘{𝐵})) |
| 32 | | ineq1 4213 |
. . . . . . . 8
⊢ (𝑛 = (𝑎(,)𝑏) → (𝑛 ∩ (𝐴 ∖ {𝐵})) = ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵}))) |
| 33 | 32 | neeq1d 3000 |
. . . . . . 7
⊢ (𝑛 = (𝑎(,)𝑏) → ((𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅ ↔ ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
| 34 | 33 | rspccva 3621 |
. . . . . 6
⊢
((∀𝑛 ∈
((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅ ∧ (𝑎(,)𝑏) ∈ ((nei‘𝐽)‘{𝐵})) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
| 35 | 11, 31, 34 | syl2anc 584 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) ∧ (𝑎 ∈ ℝ* ∧ 𝑏 ∈ ℝ*)
∧ 𝐵 ∈ (𝑎(,)𝑏)) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
| 36 | 35 | 3exp 1120 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) → ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |
| 37 | 36 | ralrimivv 3200 |
. . 3
⊢ ((𝜑 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) → ∀𝑎 ∈ ℝ*
∀𝑏 ∈
ℝ* (𝐵
∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
| 38 | 7 | snssd 4809 |
. . . . . . . . 9
⊢ (𝜑 → {𝐵} ⊆ ℝ) |
| 39 | 8 | isnei 23111 |
. . . . . . . . 9
⊢ ((𝐽 ∈ Top ∧ {𝐵} ⊆ ℝ) → (𝑛 ∈ ((nei‘𝐽)‘{𝐵}) ↔ (𝑛 ⊆ ℝ ∧ ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)))) |
| 40 | 4, 38, 39 | sylancr 587 |
. . . . . . . 8
⊢ (𝜑 → (𝑛 ∈ ((nei‘𝐽)‘{𝐵}) ↔ (𝑛 ⊆ ℝ ∧ ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)))) |
| 41 | 40 | simplbda 499 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → ∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) |
| 42 | 1 | eleq2i 2833 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ∈ 𝐽 ↔ 𝑣 ∈ (topGen‘ran
(,))) |
| 43 | 42 | biimpi 216 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ 𝐽 → 𝑣 ∈ (topGen‘ran
(,))) |
| 44 | 43 | 3ad2ant2 1135 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → 𝑣 ∈ (topGen‘ran
(,))) |
| 45 | | simp1 1137 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → 𝜑) |
| 46 | | simp3l 1202 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → {𝐵} ⊆ 𝑣) |
| 47 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ {𝐵} ⊆ 𝑣) → {𝐵} ⊆ 𝑣) |
| 48 | 7 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ {𝐵} ⊆ 𝑣) → 𝐵 ∈ ℝ) |
| 49 | | snssg 4783 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ ℝ → (𝐵 ∈ 𝑣 ↔ {𝐵} ⊆ 𝑣)) |
| 50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ {𝐵} ⊆ 𝑣) → (𝐵 ∈ 𝑣 ↔ {𝐵} ⊆ 𝑣)) |
| 51 | 47, 50 | mpbird 257 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ {𝐵} ⊆ 𝑣) → 𝐵 ∈ 𝑣) |
| 52 | 45, 46, 51 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → 𝐵 ∈ 𝑣) |
| 53 | 44, 52 | jca 511 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → (𝑣 ∈ (topGen‘ran (,)) ∧ 𝐵 ∈ 𝑣)) |
| 54 | | tg2 22972 |
. . . . . . . . . . . 12
⊢ ((𝑣 ∈ (topGen‘ran (,))
∧ 𝐵 ∈ 𝑣) → ∃𝑢 ∈ ran (,)(𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) |
| 55 | | ioof 13487 |
. . . . . . . . . . . . . . . . 17
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
| 56 | | ffn 6736 |
. . . . . . . . . . . . . . . . 17
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
| 57 | | ovelrn 7609 |
. . . . . . . . . . . . . . . . 17
⊢ ((,) Fn
(ℝ* × ℝ*) → (𝑢 ∈ ran (,) ↔ ∃𝑎 ∈ ℝ*
∃𝑏 ∈
ℝ* 𝑢 =
(𝑎(,)𝑏))) |
| 58 | 55, 56, 57 | mp2b 10 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 ∈ ran (,) ↔
∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑢 = (𝑎(,)𝑏)) |
| 59 | 58 | biimpi 216 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 ∈ ran (,) →
∃𝑎 ∈
ℝ* ∃𝑏 ∈ ℝ* 𝑢 = (𝑎(,)𝑏)) |
| 60 | 59 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ ran (,) ∧ (𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
𝑢 = (𝑎(,)𝑏)) |
| 61 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → 𝐵 ∈ 𝑢) |
| 62 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → 𝑢 = (𝑎(,)𝑏)) |
| 63 | 61, 62 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → 𝐵 ∈ (𝑎(,)𝑏)) |
| 64 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → 𝑢 ⊆ 𝑣) |
| 65 | 62, 64 | eqsstrrd 4019 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → (𝑎(,)𝑏) ⊆ 𝑣) |
| 66 | 63, 65 | jca 511 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) ∧ 𝑢 = (𝑎(,)𝑏)) → (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) |
| 67 | 66 | ex 412 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) → (𝑢 = (𝑎(,)𝑏) → (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣))) |
| 68 | 67 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑢 ∈ ran (,) ∧ (𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) → (𝑢 = (𝑎(,)𝑏) → (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣))) |
| 69 | 68 | reximdv 3170 |
. . . . . . . . . . . . . . 15
⊢ ((𝑢 ∈ ran (,) ∧ (𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) → (∃𝑏 ∈ ℝ* 𝑢 = (𝑎(,)𝑏) → ∃𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣))) |
| 70 | 69 | reximdv 3170 |
. . . . . . . . . . . . . 14
⊢ ((𝑢 ∈ ran (,) ∧ (𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) → (∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
𝑢 = (𝑎(,)𝑏) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣))) |
| 71 | 60, 70 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝑢 ∈ ran (,) ∧ (𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣)) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) |
| 72 | 71 | rexlimiva 3147 |
. . . . . . . . . . . 12
⊢
(∃𝑢 ∈ ran
(,)(𝐵 ∈ 𝑢 ∧ 𝑢 ⊆ 𝑣) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) |
| 73 | 53, 54, 72 | 3syl 18 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣)) |
| 74 | | simpl3r 1230 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) ∧ 𝑎 ∈ ℝ*) → 𝑣 ⊆ 𝑛) |
| 75 | 74 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*)
→ 𝑣 ⊆ 𝑛) |
| 76 | | sstr 3992 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑎(,)𝑏) ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛) → (𝑎(,)𝑏) ⊆ 𝑛) |
| 77 | 76 | expcom 413 |
. . . . . . . . . . . . . . 15
⊢ (𝑣 ⊆ 𝑛 → ((𝑎(,)𝑏) ⊆ 𝑣 → (𝑎(,)𝑏) ⊆ 𝑛)) |
| 78 | 75, 77 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*)
→ ((𝑎(,)𝑏) ⊆ 𝑣 → (𝑎(,)𝑏) ⊆ 𝑛)) |
| 79 | 78 | anim2d 612 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*)
→ ((𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣) → (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛))) |
| 80 | 79 | reximdva 3168 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) ∧ 𝑎 ∈ ℝ*) →
(∃𝑏 ∈
ℝ* (𝐵
∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣) → ∃𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛))) |
| 81 | 80 | reximdva 3168 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → (∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑣) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛))) |
| 82 | 73, 81 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐽 ∧ ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛)) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) |
| 83 | 82 | 3exp 1120 |
. . . . . . . . 9
⊢ (𝜑 → (𝑣 ∈ 𝐽 → (({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)))) |
| 84 | 83 | rexlimdv 3153 |
. . . . . . . 8
⊢ (𝜑 → (∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛))) |
| 85 | 84 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → (∃𝑣 ∈ 𝐽 ({𝐵} ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑛) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛))) |
| 86 | 41, 85 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) |
| 87 | 86 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → ∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) |
| 88 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑎𝜑 |
| 89 | | nfra1 3284 |
. . . . . . . 8
⊢
Ⅎ𝑎∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
| 90 | 88, 89 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑎(𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
| 91 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎ𝑎 𝑛 ∈ ((nei‘𝐽)‘{𝐵}) |
| 92 | 90, 91 | nfan 1899 |
. . . . . 6
⊢
Ⅎ𝑎((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) |
| 93 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑎(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅ |
| 94 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏𝜑 |
| 95 | | nfra2w 3299 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
| 96 | 94, 95 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑏(𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
| 97 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑏 𝑛 ∈ ((nei‘𝐽)‘{𝐵}) |
| 98 | 96, 97 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑏((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) |
| 99 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑏 𝑎 ∈
ℝ* |
| 100 | 98, 99 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑏(((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) |
| 101 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑏(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅ |
| 102 | | inss1 4237 |
. . . . . . . . . . . 12
⊢ ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑎(,)𝑏) |
| 103 | | simp3r 1203 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → (𝑎(,)𝑏) ⊆ 𝑛) |
| 104 | 102, 103 | sstrid 3995 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ 𝑛) |
| 105 | | inss2 4238 |
. . . . . . . . . . . 12
⊢ ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝐴 ∖ {𝐵}) |
| 106 | 105 | a1i 11 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝐴 ∖ {𝐵})) |
| 107 | 104, 106 | ssind 4241 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑛 ∩ (𝐴 ∖ {𝐵}))) |
| 108 | | simpllr 776 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) →
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
| 109 | 108 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
| 110 | | simp1r 1199 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → 𝑎 ∈ ℝ*) |
| 111 | | simp2 1138 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → 𝑏 ∈ ℝ*) |
| 112 | 110, 111 | jca 511 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → (𝑎 ∈ ℝ* ∧ 𝑏 ∈
ℝ*)) |
| 113 | | simp3l 1202 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → 𝐵 ∈ (𝑎(,)𝑏)) |
| 114 | | rsp2 3277 |
. . . . . . . . . . 11
⊢
(∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) → ((𝑎 ∈ ℝ*
∧ 𝑏 ∈
ℝ*) → (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |
| 115 | 109, 112,
113, 114 | syl3c 66 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
| 116 | | ssn0 4404 |
. . . . . . . . . 10
⊢ ((((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ⊆ (𝑛 ∩ (𝐴 ∖ {𝐵})) ∧ ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
| 117 | 107, 115,
116 | syl2anc 584 |
. . . . . . . . 9
⊢
(((((𝜑 ∧
∀𝑎 ∈
ℝ* ∀𝑏 ∈ ℝ* (𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) ∧ 𝑏 ∈ ℝ*
∧ (𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛)) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
| 118 | 117 | 3exp 1120 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) → (𝑏 ∈ ℝ*
→ ((𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |
| 119 | 100, 101,
118 | rexlimd 3266 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) ∧ 𝑎 ∈ ℝ*) →
(∃𝑏 ∈
ℝ* (𝐵
∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
| 120 | 119 | ex 412 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → (𝑎 ∈ ℝ* →
(∃𝑏 ∈
ℝ* (𝐵
∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |
| 121 | 92, 93, 120 | rexlimd 3266 |
. . . . 5
⊢ (((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → (∃𝑎 ∈ ℝ* ∃𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) ∧ (𝑎(,)𝑏) ⊆ 𝑛) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) |
| 122 | 87, 121 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐵})) → (𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
| 123 | 122 | ralrimiva 3146 |
. . 3
⊢ ((𝜑 ∧ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅)) → ∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅) |
| 124 | 37, 123 | impbida 801 |
. 2
⊢ (𝜑 → (∀𝑛 ∈ ((nei‘𝐽)‘{𝐵})(𝑛 ∩ (𝐴 ∖ {𝐵})) ≠ ∅ ↔ ∀𝑎 ∈ ℝ*
∀𝑏 ∈
ℝ* (𝐵
∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |
| 125 | 10, 124 | bitrd 279 |
1
⊢ (𝜑 → (𝐵 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑎 ∈ ℝ* ∀𝑏 ∈ ℝ*
(𝐵 ∈ (𝑎(,)𝑏) → ((𝑎(,)𝑏) ∩ (𝐴 ∖ {𝐵})) ≠ ∅))) |