Theorem iscnrm3

Description: A completely normal topology is a topology in which two separated sets can be separated by open neighborhoods. (Contributed by Zhi Wang, 5-Sep-2024)

	Ref	Expression
Assertion	iscnrm3	⊢ ( 𝐽 ∈ CNrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ∪ 𝐽 ∀ 𝑡 ∈ 𝒫 ∪ 𝐽 ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
2	1	iscnrm	⊢ ( 𝐽 ∈ CNrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑧 ∈ 𝒫 ∪ 𝐽 ( 𝐽 ↾t 𝑧 ) ∈ Nrm ) )
3		iscnrm3lem1	⊢ ( 𝐽 ∈ Top → ( ∀ 𝑧 ∈ 𝒫 ∪ 𝐽 ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑧 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ↔ ∀ 𝑧 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑧 ) ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑧 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ) ) )
4		isnrm3	⊢ ( ( 𝐽 ↾t 𝑧 ) ∈ Nrm ↔ ( ( 𝐽 ↾t 𝑧 ) ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑧 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ) )
5	4	ralbii	⊢ ( ∀ 𝑧 ∈ 𝒫 ∪ 𝐽 ( 𝐽 ↾t 𝑧 ) ∈ Nrm ↔ ∀ 𝑧 ∈ 𝒫 ∪ 𝐽 ( ( 𝐽 ↾t 𝑧 ) ∈ Top ∧ ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑧 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ) )
6	3 5	bitr4di	⊢ ( 𝐽 ∈ Top → ( ∀ 𝑧 ∈ 𝒫 ∪ 𝐽 ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑧 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ↔ ∀ 𝑧 ∈ 𝒫 ∪ 𝐽 ( 𝐽 ↾t 𝑧 ) ∈ Nrm ) )
7		iscnrm3r	⊢ ( 𝐽 ∈ Top → ( ∀ 𝑧 ∈ 𝒫 ∪ 𝐽 ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑧 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) → ( ( 𝑠 ∈ 𝒫 ∪ 𝐽 ∧ 𝑡 ∈ 𝒫 ∪ 𝐽 ) → ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) ) )
8		iscnrm3l	⊢ ( 𝐽 ∈ Top → ( ∀ 𝑠 ∈ 𝒫 ∪ 𝐽 ∀ 𝑡 ∈ 𝒫 ∪ 𝐽 ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) → ( ( 𝑧 ∈ 𝒫 ∪ 𝐽 ∧ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ∧ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ) → ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑧 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ) ) )
9	7 8	iscnrm3lem2	⊢ ( 𝐽 ∈ Top → ( ∀ 𝑧 ∈ 𝒫 ∪ 𝐽 ∀ 𝑐 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ∀ 𝑑 ∈ ( Clsd ‘ ( 𝐽 ↾t 𝑧 ) ) ( ( 𝑐 ∩ 𝑑 ) = ∅ → ∃ 𝑙 ∈ ( 𝐽 ↾t 𝑧 ) ∃ 𝑘 ∈ ( 𝐽 ↾t 𝑧 ) ( 𝑐 ⊆ 𝑙 ∧ 𝑑 ⊆ 𝑘 ∧ ( 𝑙 ∩ 𝑘 ) = ∅ ) ) ↔ ∀ 𝑠 ∈ 𝒫 ∪ 𝐽 ∀ 𝑡 ∈ 𝒫 ∪ 𝐽 ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )
10	6 9	bitr3d	⊢ ( 𝐽 ∈ Top → ( ∀ 𝑧 ∈ 𝒫 ∪ 𝐽 ( 𝐽 ↾t 𝑧 ) ∈ Nrm ↔ ∀ 𝑠 ∈ 𝒫 ∪ 𝐽 ∀ 𝑡 ∈ 𝒫 ∪ 𝐽 ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )
11	10	pm5.32i	⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑧 ∈ 𝒫 ∪ 𝐽 ( 𝐽 ↾t 𝑧 ) ∈ Nrm ) ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ∪ 𝐽 ∀ 𝑡 ∈ 𝒫 ∪ 𝐽 ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )
12	2 11	bitri	⊢ ( 𝐽 ∈ CNrm ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑠 ∈ 𝒫 ∪ 𝐽 ∀ 𝑡 ∈ 𝒫 ∪ 𝐽 ( ( ( 𝑠 ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑡 ) ) = ∅ ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑠 ) ∩ 𝑡 ) = ∅ ) → ∃ 𝑛 ∈ 𝐽 ∃ 𝑚 ∈ 𝐽 ( 𝑠 ⊆ 𝑛 ∧ 𝑡 ⊆ 𝑚 ∧ ( 𝑛 ∩ 𝑚 ) = ∅ ) ) ) )