Metamath Proof Explorer

Theorem isnrm2

Description: An alternate characterization of normality. This is the important property in the proof of Urysohn's lemma. (Contributed by Jeff Hankins, 1-Feb-2010) (Proof shortened by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion isnrm2 ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ) ) )

Proof

Step Hyp Ref Expression
1 nrmtop ⊢ ( 𝐽 ∈ Nrm → 𝐽 ∈ Top )
2 nrmsep2 ⊢ ( ( 𝐽 ∈ Nrm ∧ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ∧ ( 𝑐 ∩ 𝑑 ) = ∅ ) ) → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) )
3 2 3exp2 ⊢ ( 𝐽 ∈ Nrm → ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) → ( 𝑑 ∈ ( Clsd ‘ 𝐽 ) → ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ) ) ) )
4 3 impd ⊢ ( 𝐽 ∈ Nrm → ( ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ) ) )
5 4 ralrimivv ⊢ ( 𝐽 ∈ Nrm → ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ) )
6 1 5 jca ⊢ ( 𝐽 ∈ Nrm → ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ) ) )
7 simpl ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ) ) → 𝐽 ∈ Top )
8 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
9 8 opncld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) → ( ∪ 𝐽 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
10 9 adantr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∪ 𝐽 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) )
11 ineq2 ⊢ ( 𝑑 = ( ∪ 𝐽 ∖ 𝑥 ) → ( 𝑐 ∩ 𝑑 ) = ( 𝑐 ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) )
12 11 eqeq1d ⊢ ( 𝑑 = ( ∪ 𝐽 ∖ 𝑥 ) → ( ( 𝑐 ∩ 𝑑 ) = ∅ ↔ ( 𝑐 ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ ) )
13 ineq2 ⊢ ( 𝑑 = ( ∪ 𝐽 ∖ 𝑥 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) )
14 13 eqeq1d ⊢ ( 𝑑 = ( ∪ 𝐽 ∖ 𝑥 ) → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ ) )
15 14 anbi2d ⊢ ( 𝑑 = ( ∪ 𝐽 ∖ 𝑥 ) → ( ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ↔ ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ ) ) )
16 15 rexbidv ⊢ ( 𝑑 = ( ∪ 𝐽 ∖ 𝑥 ) → ( ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ↔ ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ ) ) )
17 12 16 imbi12d ⊢ ( 𝑑 = ( ∪ 𝐽 ∖ 𝑥 ) → ( ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ) ↔ ( ( 𝑐 ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ ) ) ) )
18 17 rspcv ⊢ ( ( ∪ 𝐽 ∖ 𝑥 ) ∈ ( Clsd ‘ 𝐽 ) → ( ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ) → ( ( 𝑐 ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ ) ) ) )
19 10 18 syl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ) → ( ( 𝑐 ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ ) ) ) )
20 inssdif0 ⊢ ( ( 𝑐 ∩ ∪ 𝐽 ) ⊆ 𝑥 ↔ ( 𝑐 ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ )
21 8 cldss ⊢ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) → 𝑐 ⊆ ∪ 𝐽 )
22 21 adantl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ) → 𝑐 ⊆ ∪ 𝐽 )
23 df-ss ⊢ ( 𝑐 ⊆ ∪ 𝐽 ↔ ( 𝑐 ∩ ∪ 𝐽 ) = 𝑐 )
24 22 23 sylib ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ) → ( 𝑐 ∩ ∪ 𝐽 ) = 𝑐 )
25 24 sseq1d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑐 ∩ ∪ 𝐽 ) ⊆ 𝑥 ↔ 𝑐 ⊆ 𝑥 ) )
26 20 25 bitr3id ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( 𝑐 ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ ↔ 𝑐 ⊆ 𝑥 ) )
27 inssdif0 ⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ ∪ 𝐽 ) ⊆ 𝑥 ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ )
28 simpll ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ) → 𝐽 ∈ Top )
29 elssuni ⊢ ( 𝑜 ∈ 𝐽 → 𝑜 ⊆ ∪ 𝐽 )
30 8 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑜 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ ∪ 𝐽 )
31 28 29 30 syl2an ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑜 ∈ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ ∪ 𝐽 )
32 df-ss ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ ∪ 𝐽 ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ ∪ 𝐽 ) = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) )
33 31 32 sylib ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑜 ∈ 𝐽 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ ∪ 𝐽 ) = ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) )
34 33 sseq1d ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑜 ∈ 𝐽 ) → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ ∪ 𝐽 ) ⊆ 𝑥 ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) )
35 27 34 bitr3id ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑜 ∈ 𝐽 ) → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ ↔ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) )
36 35 anbi2d ⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ) ∧ 𝑜 ∈ 𝐽 ) → ( ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ ) ↔ ( 𝑐 ⊆ 𝑜 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) ) )
37 36 rexbidva ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ ) ↔ ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) ) )
38 26 37 imbi12d ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ( 𝑐 ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ ( ∪ 𝐽 ∖ 𝑥 ) ) = ∅ ) ) ↔ ( 𝑐 ⊆ 𝑥 → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) ) ) )
39 19 38 sylibd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ) → ( ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ) → ( 𝑐 ⊆ 𝑥 → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) ) ) )
40 39 ralimdva ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) → ( ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ) → ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ( 𝑐 ⊆ 𝑥 → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) ) ) )
41 elin ⊢ ( 𝑐 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑥 ) ↔ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑐 ∈ 𝒫 𝑥 ) )
42 velpw ⊢ ( 𝑐 ∈ 𝒫 𝑥 ↔ 𝑐 ⊆ 𝑥 )
43 42 anbi2i ⊢ ( ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑐 ∈ 𝒫 𝑥 ) ↔ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑐 ⊆ 𝑥 ) )
44 41 43 bitri ⊢ ( 𝑐 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑥 ) ↔ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑐 ⊆ 𝑥 ) )
45 44 imbi1i ⊢ ( ( 𝑐 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑥 ) → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) ) ↔ ( ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑐 ⊆ 𝑥 ) → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) ) )
46 impexp ⊢ ( ( ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑐 ⊆ 𝑥 ) → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) ) ↔ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) → ( 𝑐 ⊆ 𝑥 → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) ) ) )
47 45 46 bitri ⊢ ( ( 𝑐 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑥 ) → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) ) ↔ ( 𝑐 ∈ ( Clsd ‘ 𝐽 ) → ( 𝑐 ⊆ 𝑥 → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) ) ) )
48 47 ralbii2 ⊢ ( ∀ 𝑐 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑥 ) ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) ↔ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ( 𝑐 ⊆ 𝑥 → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) ) )
49 40 48 syl6ibr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ) → ( ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ) → ∀ 𝑐 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑥 ) ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) ) )
50 49 ralrimdva ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ) → ∀ 𝑥 ∈ 𝐽 ∀ 𝑐 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑥 ) ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) ) )
51 50 imp ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ) ) → ∀ 𝑥 ∈ 𝐽 ∀ 𝑐 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑥 ) ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) )
52 isnrm ⊢ ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ 𝐽 ∀ 𝑐 ∈ ( ( Clsd ‘ 𝐽 ) ∩ 𝒫 𝑥 ) ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ⊆ 𝑥 ) ) )
53 7 51 52 sylanbrc ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ) ) → 𝐽 ∈ Nrm )
54 6 53 impbii ⊢ ( 𝐽 ∈ Nrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ∀ 𝑑 ∈ ( Clsd ‘ 𝐽 ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑜 ∈ 𝐽 ( 𝑐 ⊆ 𝑜 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑜 ) ∩ 𝑑 ) = ∅ ) ) ) )