Theorem iscnrm3rlem5

Description: Lemma for iscnrm3rlem6 . (Contributed by Zhi Wang, 5-Sep-2024)

	Ref	Expression
Hypotheses	iscnrm3rlem4.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
	iscnrm3rlem4.2	⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝐽 )
	iscnrm3rlem5.3	⊢ ( 𝜑 → 𝑇 ⊆ ∪ 𝐽 )
Assertion	iscnrm3rlem5	⊢ ( 𝜑 → ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ∈ 𝐽 )

Proof

Step	Hyp	Ref	Expression
1		iscnrm3rlem4.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		iscnrm3rlem4.2	⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝐽 )
3		iscnrm3rlem5.3	⊢ ( 𝜑 → 𝑇 ⊆ ∪ 𝐽 )
4		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
5	4	clscld	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )
6	1 2 5	syl2anc	⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )
7	4	clscld	⊢ ( ( 𝐽 ∈ Top ∧ 𝑇 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∈ ( Clsd ‘ 𝐽 ) )
8	1 3 7	syl2anc	⊢ ( 𝜑 → ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∈ ( Clsd ‘ 𝐽 ) )
9		incld	⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∈ ( Clsd ‘ 𝐽 ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∈ ( Clsd ‘ 𝐽 ) )
10	6 8 9	syl2anc	⊢ ( 𝜑 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∈ ( Clsd ‘ 𝐽 ) )
11	4	cldopn	⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∈ ( Clsd ‘ 𝐽 ) → ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ∈ 𝐽 )
12	10 11	syl	⊢ ( 𝜑 → ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ∈ 𝐽 )