Theorem iscnrm3rlem2

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

	Ref	Expression
Hypotheses	iscnrm3rlem2.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
	iscnrm3rlem2.2	⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝐽 )
Assertion	iscnrm3rlem2	⊢ ( 𝜑 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscnrm3rlem2.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		iscnrm3rlem2.2	⊢ ( 𝜑 → 𝑆 ⊆ ∪ 𝐽 )
3		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
4	3	clscld	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) )
5	3	clsss3	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ∪ 𝐽 )
6	5	iscnrm3rlem1	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) ) ) )
7		ineq1	⊢ ( 𝑐 = ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) → ( 𝑐 ∩ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) ) ) )
8	7	rspceeqv	⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) ) ) ) → ∃ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) = ( 𝑐 ∩ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) ) ) )
9	4 6 8	syl2anc	⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ∃ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) = ( 𝑐 ∩ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) ) ) )
10	1 2 9	syl2anc	⊢ ( 𝜑 → ∃ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) = ( 𝑐 ∩ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) ) ) )
11		difss	⊢ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) ) ⊆ ∪ 𝐽
12	3	restcld	⊢ ( ( 𝐽 ∈ Top ∧ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) ) ⊆ ∪ 𝐽 ) → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) ) ) ) ↔ ∃ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) = ( 𝑐 ∩ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) ) ) ) )
13	1 11 12	sylancl	⊢ ( 𝜑 → ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) ) ) ) ↔ ∃ 𝑐 ∈ ( Clsd ‘ 𝐽 ) ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) = ( 𝑐 ∩ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) ) ) ) )
14	10 13	mpbird	⊢ ( 𝜑 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ 𝑇 ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) ) ) ) )