Step |
Hyp |
Ref |
Expression |
1 |
|
nrmtop |
⊢ ( 𝐽 ∈ Nrm → 𝐽 ∈ Top ) |
2 |
|
nrmsep |
⊢ ( ( 𝐽 ∈ Nrm ∧ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑐 ∩ 𝑑 ) = ∅ ) ) → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) |
3 |
2
|
3exp2 |
⊢ ( 𝐽 ∈ Nrm → ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) → ( 𝑑 ∈ ( Clsd ‘ 𝐽 ) → ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) ) ) |
4 |
3
|
impd |
⊢ ( 𝐽 ∈ Nrm → ( ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) ) |
5 |
4
|
ralrimivv |
⊢ ( 𝐽 ∈ Nrm → ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) |
6 |
1 5
|
jca |
⊢ ( 𝐽 ∈ Nrm → ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) ) |
7 |
|
simpl |
⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) → 𝐽 ∈ Top ) |
8 |
|
simpr1 |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑐 ⊆ 𝑥 ) |
9 |
|
simpr2 |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑑 ⊆ 𝑦 ) |
10 |
|
sslin |
⊢ ( 𝑑 ⊆ 𝑦 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) ⊆ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑦 ) ) |
11 |
9 10
|
syl |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) ⊆ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑦 ) ) |
12 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
13 |
12
|
opncld |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑦 ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) ) |
14 |
13
|
ad4ant13 |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( ∪ 𝐽 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) ) |
15 |
|
simpr3 |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( 𝑥 ∩ 𝑦 ) = ∅ ) |
16 |
|
simpllr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑥 ∈ 𝐽 ) |
17 |
|
elssuni |
⊢ ( 𝑥 ∈ 𝐽 → 𝑥 ⊆ ∪ 𝐽 ) |
18 |
|
reldisj |
⊢ ( 𝑥 ⊆ ∪ 𝐽 → ( ( 𝑥 ∩ 𝑦 ) = ∅ ↔ 𝑥 ⊆ ( ∪ 𝐽 ∖ 𝑦 ) ) ) |
19 |
16 17 18
|
3syl |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( ( 𝑥 ∩ 𝑦 ) = ∅ ↔ 𝑥 ⊆ ( ∪ 𝐽 ∖ 𝑦 ) ) ) |
20 |
15 19
|
mpbid |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → 𝑥 ⊆ ( ∪ 𝐽 ∖ 𝑦 ) ) |
21 |
12
|
clsss2 |
⊢ ( ( ( ∪ 𝐽 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 ⊆ ( ∪ 𝐽 ∖ 𝑦 ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ ( ∪ 𝐽 ∖ 𝑦 ) ) |
22 |
|
ssdifin0 |
⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ⊆ ( ∪ 𝐽 ∖ 𝑦 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑦 ) = ∅ ) |
23 |
21 22
|
syl |
⊢ ( ( ( ∪ 𝐽 ∖ 𝑦 ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑥 ⊆ ( ∪ 𝐽 ∖ 𝑦 ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑦 ) = ∅ ) |
24 |
14 20 23
|
syl2anc |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑦 ) = ∅ ) |
25 |
|
sseq0 |
⊢ ( ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) ⊆ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑦 ) ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑦 ) = ∅ ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) |
26 |
11 24 25
|
syl2anc |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) |
27 |
8 26
|
jca |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝐽 ) ∧ ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( 𝑐 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) ) |
28 |
27
|
rexlimdva2 |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) → ( ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ( 𝑐 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) ) ) |
29 |
28
|
reximdva |
⊢ ( 𝐽 ∈ Top → ( ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) → ∃ 𝑥 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) ) ) |
30 |
29
|
imim2d |
⊢ ( 𝐽 ∈ Top → ( ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) ) ) ) |
31 |
30
|
ralimdv |
⊢ ( 𝐽 ∈ Top → ( ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) ) ) ) |
32 |
31
|
ralimdv |
⊢ ( 𝐽 ∈ Top → ( ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) → ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) ) ) ) |
33 |
32
|
imp |
⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) → ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) ) ) |
34 |
|
isnrm2 |
⊢ ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑥 ) ∩ 𝑑 ) = ∅ ) ) ) ) |
35 |
7 33 34
|
sylanbrc |
⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) → 𝐽 ∈ Nrm ) |
36 |
6 35
|
impbii |
⊢ ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑥 ∈ 𝐽 ∃ 𝑦 ∈ 𝐽 ( 𝑐 ⊆ 𝑥 ∧ 𝑑 ⊆ 𝑦 ∧ ( 𝑥 ∩ 𝑦 ) = ∅ ) ) ) ) |