Theorem psdmullem

Description: Lemma for psdmul . Transitive law for union of class difference. (Contributed by SN, 5-May-2025)

	Ref	Expression
Hypotheses	psdmullem.cb	⊢ ( 𝜑 → 𝐶 ⊆ 𝐵 )
	psdmullem.ba	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
Assertion	psdmullem	⊢ ( 𝜑 → ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐶 ) ) = ( 𝐴 ∖ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		psdmullem.cb	⊢ ( 𝜑 → 𝐶 ⊆ 𝐵 )
2		psdmullem.ba	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
3		undif3	⊢ ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐶 ) ) = ( ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ∖ ( 𝐶 ∖ ( 𝐴 ∖ 𝐵 ) ) )
4		undifr	⊢ ( 𝐵 ⊆ 𝐴 ↔ ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) = 𝐴 )
5	2 4	sylib	⊢ ( 𝜑 → ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) = 𝐴 )
6		difdif2	⊢ ( 𝐶 ∖ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝐶 ∖ 𝐴 ) ∪ ( 𝐶 ∩ 𝐵 ) )
7	1 2	sstrd	⊢ ( 𝜑 → 𝐶 ⊆ 𝐴 )
8		ssdif0	⊢ ( 𝐶 ⊆ 𝐴 ↔ ( 𝐶 ∖ 𝐴 ) = ∅ )
9	7 8	sylib	⊢ ( 𝜑 → ( 𝐶 ∖ 𝐴 ) = ∅ )
10		dfss2	⊢ ( 𝐶 ⊆ 𝐵 ↔ ( 𝐶 ∩ 𝐵 ) = 𝐶 )
11	1 10	sylib	⊢ ( 𝜑 → ( 𝐶 ∩ 𝐵 ) = 𝐶 )
12	9 11	uneq12d	⊢ ( 𝜑 → ( ( 𝐶 ∖ 𝐴 ) ∪ ( 𝐶 ∩ 𝐵 ) ) = ( ∅ ∪ 𝐶 ) )
13		0un	⊢ ( ∅ ∪ 𝐶 ) = 𝐶
14	12 13	eqtrdi	⊢ ( 𝜑 → ( ( 𝐶 ∖ 𝐴 ) ∪ ( 𝐶 ∩ 𝐵 ) ) = 𝐶 )
15	6 14	eqtrid	⊢ ( 𝜑 → ( 𝐶 ∖ ( 𝐴 ∖ 𝐵 ) ) = 𝐶 )
16	5 15	difeq12d	⊢ ( 𝜑 → ( ( ( 𝐴 ∖ 𝐵 ) ∪ 𝐵 ) ∖ ( 𝐶 ∖ ( 𝐴 ∖ 𝐵 ) ) ) = ( 𝐴 ∖ 𝐶 ) )
17	3 16	eqtrid	⊢ ( 𝜑 → ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐶 ) ) = ( 𝐴 ∖ 𝐶 ) )