Theorem restclsseplem

Description: Lemma for restclssep . (Contributed by Zhi Wang, 2-Sep-2024)

	Ref	Expression
Hypotheses	restcls2.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
	restcls2.2	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
	restcls2.3	⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
	restcls2.4	⊢ ( 𝜑 → 𝐾 = ( 𝐽 ↾t 𝑌 ) )
	restcls2.5	⊢ ( 𝜑 → 𝑆 ∈ ( Clsd ‘ 𝐾 ) )
	restclsseplem.6	⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ )
	restclsseplem.7	⊢ ( 𝜑 → 𝑇 ⊆ 𝑌 )
Assertion	restclsseplem	⊢ ( 𝜑 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		restcls2.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		restcls2.2	⊢ ( 𝜑 → 𝑋 = ∪ 𝐽 )
3		restcls2.3	⊢ ( 𝜑 → 𝑌 ⊆ 𝑋 )
4		restcls2.4	⊢ ( 𝜑 → 𝐾 = ( 𝐽 ↾t 𝑌 ) )
5		restcls2.5	⊢ ( 𝜑 → 𝑆 ∈ ( Clsd ‘ 𝐾 ) )
6		restclsseplem.6	⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ∅ )
7		restclsseplem.7	⊢ ( 𝜑 → 𝑇 ⊆ 𝑌 )
8	1 2 3 4 5	restcls2	⊢ ( 𝜑 → 𝑆 = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) )
9	8	ineq1d	⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ∩ 𝑇 ) )
10		inass	⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ∩ 𝑇 ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( 𝑌 ∩ 𝑇 ) )
11	9 10	eqtrdi	⊢ ( 𝜑 → ( 𝑆 ∩ 𝑇 ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( 𝑌 ∩ 𝑇 ) ) )
12		sseqin2	⊢ ( 𝑇 ⊆ 𝑌 ↔ ( 𝑌 ∩ 𝑇 ) = 𝑇 )
13	7 12	sylib	⊢ ( 𝜑 → ( 𝑌 ∩ 𝑇 ) = 𝑇 )
14	13	ineq2d	⊢ ( 𝜑 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ ( 𝑌 ∩ 𝑇 ) ) = ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) )
15	11 6 14	3eqtr3rd	⊢ ( 𝜑 → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑇 ) = ∅ )