Theorem iscnrm3rlem1

Description: Lemma for iscnrm3rlem2 . The hypothesis could be generalized to ( ph -> ( S \ T ) C_ X ) . (Contributed by Zhi Wang, 5-Sep-2024)

	Ref	Expression
Hypothesis	iscnrm3rlem1.1	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
Assertion	iscnrm3rlem1	⊢ ( 𝜑 → ( 𝑆 ∖ 𝑇 ) = ( 𝑆 ∩ ( 𝑋 ∖ ( 𝑆 ∩ 𝑇 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		iscnrm3rlem1.1	⊢ ( 𝜑 → 𝑆 ⊆ 𝑋 )
2		difindi	⊢ ( 𝑋 ∖ ( 𝑆 ∩ 𝑇 ) ) = ( ( 𝑋 ∖ 𝑆 ) ∪ ( 𝑋 ∖ 𝑇 ) )
3	2	ineq2i	⊢ ( 𝑆 ∩ ( 𝑋 ∖ ( 𝑆 ∩ 𝑇 ) ) ) = ( 𝑆 ∩ ( ( 𝑋 ∖ 𝑆 ) ∪ ( 𝑋 ∖ 𝑇 ) ) )
4		indi	⊢ ( 𝑆 ∩ ( ( 𝑋 ∖ 𝑆 ) ∪ ( 𝑋 ∖ 𝑇 ) ) ) = ( ( 𝑆 ∩ ( 𝑋 ∖ 𝑆 ) ) ∪ ( 𝑆 ∩ ( 𝑋 ∖ 𝑇 ) ) )
5		disjdif	⊢ ( 𝑆 ∩ ( 𝑋 ∖ 𝑆 ) ) = ∅
6	5	uneq1i	⊢ ( ( 𝑆 ∩ ( 𝑋 ∖ 𝑆 ) ) ∪ ( 𝑆 ∩ ( 𝑋 ∖ 𝑇 ) ) ) = ( ∅ ∪ ( 𝑆 ∩ ( 𝑋 ∖ 𝑇 ) ) )
7		0un	⊢ ( ∅ ∪ ( 𝑆 ∩ ( 𝑋 ∖ 𝑇 ) ) ) = ( 𝑆 ∩ ( 𝑋 ∖ 𝑇 ) )
8		indif2	⊢ ( 𝑆 ∩ ( 𝑋 ∖ 𝑇 ) ) = ( ( 𝑆 ∩ 𝑋 ) ∖ 𝑇 )
9	6 7 8	3eqtri	⊢ ( ( 𝑆 ∩ ( 𝑋 ∖ 𝑆 ) ) ∪ ( 𝑆 ∩ ( 𝑋 ∖ 𝑇 ) ) ) = ( ( 𝑆 ∩ 𝑋 ) ∖ 𝑇 )
10	3 4 9	3eqtri	⊢ ( 𝑆 ∩ ( 𝑋 ∖ ( 𝑆 ∩ 𝑇 ) ) ) = ( ( 𝑆 ∩ 𝑋 ) ∖ 𝑇 )
11		dfss2	⊢ ( 𝑆 ⊆ 𝑋 ↔ ( 𝑆 ∩ 𝑋 ) = 𝑆 )
12	1 11	sylib	⊢ ( 𝜑 → ( 𝑆 ∩ 𝑋 ) = 𝑆 )
13	12	difeq1d	⊢ ( 𝜑 → ( ( 𝑆 ∩ 𝑋 ) ∖ 𝑇 ) = ( 𝑆 ∖ 𝑇 ) )
14	10 13	eqtr2id	⊢ ( 𝜑 → ( 𝑆 ∖ 𝑇 ) = ( 𝑆 ∩ ( 𝑋 ∖ ( 𝑆 ∩ 𝑇 ) ) ) )