Theorem iscnrm3rlem3

Description: Lemma for iscnrm3r . The designed subspace is a subset of the original set; the two sets are closed sets in the subspace. (Contributed by Zhi Wang, 5-Sep-2024)

	Ref	Expression
Assertion	iscnrm3rlem3	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ) → ( ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ∈ 𝒫 ∪ 𝐽 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		uniexg	⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ V )
2		difssd	⊢ ( 𝐽 ∈ Top → ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ⊆ ∪ 𝐽 )
3	1 2	sselpwd	⊢ ( 𝐽 ∈ Top → ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ∈ 𝒫 ∪ 𝐽 )
4	3	adantr	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ) → ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ∈ 𝒫 ∪ 𝐽 )
5		simpl	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ) → 𝐽 ∈ Top )
6		simprl	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ) → 𝑆 ∈ 𝒫 ∪ 𝐽 )
7	6	elpwid	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ) → 𝑆 ⊆ ∪ 𝐽 )
8	5 7	iscnrm3rlem2	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) )
9		simprr	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ) → 𝑇 ∈ 𝒫 ∪ 𝐽 )
10	9	elpwid	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ) → 𝑇 ⊆ ∪ 𝐽 )
11	5 10	iscnrm3rlem2	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) ) ) )
12		incom	⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
13	12	difeq2i	⊢ ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) = ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
14	13	oveq2i	⊢ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) = ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) )
15	14	fveq2i	⊢ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) = ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ) ) )
16	11 15	eleqtrrdi	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) )
17	4 8 16	3jca	⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∈ 𝒫 ∪ 𝐽 ∧ 𝑇 ∈ 𝒫 ∪ 𝐽 ) ) → ( ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ∈ 𝒫 ∪ 𝐽 ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ∖ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ∈ ( Clsd ‘ ( 𝐽 ↾t ( ∪ 𝐽 ∖ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( ( cls ‘ 𝐽 ) ‘ 𝑇 ) ) ) ) ) ) )