This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( 𝜑 → ( ( 𝐴 ∖ 𝐵 ) ∪ ( 𝐵 ∖ 𝐶 ) ) = ( 𝐴 ∖ 𝐶 ) )