Step |
Hyp |
Ref |
Expression |
1 |
|
sepnsepolem2.1 |
⊢ ( 𝜑 → 𝐽 ∈ Top ) |
2 |
|
id |
⊢ ( 𝐽 ∈ Top → 𝐽 ∈ Top ) |
3 |
2
|
sepnsepolem2 |
⊢ ( 𝐽 ∈ Top → ( ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑦 ∈ 𝐽 ( 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) |
4 |
3
|
anbi2d |
⊢ ( 𝐽 ∈ Top → ( ( 𝐶 ⊆ 𝑥 ∧ ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ( 𝐶 ⊆ 𝑥 ∧ ∃ 𝑦 ∈ 𝐽 ( 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) ) |
5 |
4
|
rexbidv |
⊢ ( 𝐽 ∈ Top → ( ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ ∃ 𝑦 ∈ 𝐽 ( 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) ) |
6 |
|
ssrin |
⊢ ( 𝑧 ⊆ 𝑥 → ( 𝑧 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ) |
7 |
|
sseq0 |
⊢ ( ( ( 𝑧 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑧 ∩ 𝑦 ) = ∅ ) |
8 |
7
|
ex |
⊢ ( ( 𝑧 ∩ 𝑦 ) ⊆ ( 𝑥 ∩ 𝑦 ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ → ( 𝑧 ∩ 𝑦 ) = ∅ ) ) |
9 |
6 8
|
syl |
⊢ ( 𝑧 ⊆ 𝑥 → ( ( 𝑥 ∩ 𝑦 ) = ∅ → ( 𝑧 ∩ 𝑦 ) = ∅ ) ) |
10 |
9
|
adantl |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑧 ⊆ 𝑥 ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ → ( 𝑧 ∩ 𝑦 ) = ∅ ) ) |
11 |
10
|
reximdv |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑧 ⊆ 𝑥 ) → ( ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥 ∩ 𝑦 ) = ∅ → ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑧 ∩ 𝑦 ) = ∅ ) ) |
12 |
|
simpr |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 = 𝑧 ) → 𝑥 = 𝑧 ) |
13 |
12
|
ineq1d |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 = 𝑧 ) → ( 𝑥 ∩ 𝑦 ) = ( 𝑧 ∩ 𝑦 ) ) |
14 |
13
|
eqeq1d |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 = 𝑧 ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ( 𝑧 ∩ 𝑦 ) = ∅ ) ) |
15 |
14
|
rexbidv |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 = 𝑧 ) → ( ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑧 ∩ 𝑦 ) = ∅ ) ) |
16 |
2 11 15
|
opnneieqv |
⊢ ( 𝐽 ∈ Top → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) |
17 |
|
sepnsepolem1 |
⊢ ( ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ ∃ 𝑦 ∈ 𝐽 ( 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) |
18 |
17
|
a1i |
⊢ ( 𝐽 ∈ Top → ( ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ↔ ∃ 𝑥 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ ∃ 𝑦 ∈ 𝐽 ( 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) ) |
19 |
5 16 18
|
3bitr4d |
⊢ ( 𝐽 ∈ Top → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) |
20 |
1 19
|
syl |
⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∃ 𝑦 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐷 ) ( 𝑥 ∩ 𝑦 ) = ∅ ↔ ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝐶 ⊆ 𝑥 ∧ 𝐷 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) |