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

Metamath Proof Explorer

Theorem uneqdifeq

Description: Two ways to say that A and B partition C (when A and B don't overlap and A is a part of C ). (Contributed by FL, 17-Nov-2008) (Proof shortened by JJ, 14-Jul-2021)

Ref Expression
Assertion uneqdifeq ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐴 ∪ 𝐵 ) = 𝐶 ↔ ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 uncom ⊢ ( 𝐵 ∪ 𝐴 ) = ( 𝐴 ∪ 𝐵 )
2 eqtr ⊢ ( ( ( 𝐵 ∪ 𝐴 ) = ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) = 𝐶 ) → ( 𝐵 ∪ 𝐴 ) = 𝐶 )
3 2 eqcomd ⊢ ( ( ( 𝐵 ∪ 𝐴 ) = ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) = 𝐶 ) → 𝐶 = ( 𝐵 ∪ 𝐴 ) )
4 difeq1 ⊢ ( 𝐶 = ( 𝐵 ∪ 𝐴 ) → ( 𝐶 ∖ 𝐴 ) = ( ( 𝐵 ∪ 𝐴 ) ∖ 𝐴 ) )
5 difun2 ⊢ ( ( 𝐵 ∪ 𝐴 ) ∖ 𝐴 ) = ( 𝐵 ∖ 𝐴 )
6 eqtr ⊢ ( ( ( 𝐶 ∖ 𝐴 ) = ( ( 𝐵 ∪ 𝐴 ) ∖ 𝐴 ) ∧ ( ( 𝐵 ∪ 𝐴 ) ∖ 𝐴 ) = ( 𝐵 ∖ 𝐴 ) ) → ( 𝐶 ∖ 𝐴 ) = ( 𝐵 ∖ 𝐴 ) )
7 incom ⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
8 7 eqeq1i ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ( 𝐵 ∩ 𝐴 ) = ∅ )
9 disj3 ⊢ ( ( 𝐵 ∩ 𝐴 ) = ∅ ↔ 𝐵 = ( 𝐵 ∖ 𝐴 ) )
10 8 9 bitri ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ 𝐵 = ( 𝐵 ∖ 𝐴 ) )
11 eqtr ⊢ ( ( ( 𝐶 ∖ 𝐴 ) = ( 𝐵 ∖ 𝐴 ) ∧ ( 𝐵 ∖ 𝐴 ) = 𝐵 ) → ( 𝐶 ∖ 𝐴 ) = 𝐵 )
12 11 expcom ⊢ ( ( 𝐵 ∖ 𝐴 ) = 𝐵 → ( ( 𝐶 ∖ 𝐴 ) = ( 𝐵 ∖ 𝐴 ) → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
13 12 eqcoms ⊢ ( 𝐵 = ( 𝐵 ∖ 𝐴 ) → ( ( 𝐶 ∖ 𝐴 ) = ( 𝐵 ∖ 𝐴 ) → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
14 10 13 sylbi ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐶 ∖ 𝐴 ) = ( 𝐵 ∖ 𝐴 ) → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
15 6 14 syl5com ⊢ ( ( ( 𝐶 ∖ 𝐴 ) = ( ( 𝐵 ∪ 𝐴 ) ∖ 𝐴 ) ∧ ( ( 𝐵 ∪ 𝐴 ) ∖ 𝐴 ) = ( 𝐵 ∖ 𝐴 ) ) → ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
16 4 5 15 sylancl ⊢ ( 𝐶 = ( 𝐵 ∪ 𝐴 ) → ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
17 3 16 syl ⊢ ( ( ( 𝐵 ∪ 𝐴 ) = ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) = 𝐶 ) → ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
18 1 17 mpan ⊢ ( ( 𝐴 ∪ 𝐵 ) = 𝐶 → ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
19 18 com12 ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 ∪ 𝐵 ) = 𝐶 → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
20 19 adantl ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐴 ∪ 𝐵 ) = 𝐶 → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
21 simpl ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐶 ∖ 𝐴 ) = 𝐵 ) → 𝐴 ⊆ 𝐶 )
22 difssd ⊢ ( ( 𝐶 ∖ 𝐴 ) = 𝐵 → ( 𝐶 ∖ 𝐴 ) ⊆ 𝐶 )
23 sseq1 ⊢ ( ( 𝐶 ∖ 𝐴 ) = 𝐵 → ( ( 𝐶 ∖ 𝐴 ) ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶 ) )
24 22 23 mpbid ⊢ ( ( 𝐶 ∖ 𝐴 ) = 𝐵 → 𝐵 ⊆ 𝐶 )
25 24 adantl ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐶 ∖ 𝐴 ) = 𝐵 ) → 𝐵 ⊆ 𝐶 )
26 21 25 unssd ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐶 ∖ 𝐴 ) = 𝐵 ) → ( 𝐴 ∪ 𝐵 ) ⊆ 𝐶 )
27 eqimss ⊢ ( ( 𝐶 ∖ 𝐴 ) = 𝐵 → ( 𝐶 ∖ 𝐴 ) ⊆ 𝐵 )
28 ssundif ⊢ ( 𝐶 ⊆ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝐶 ∖ 𝐴 ) ⊆ 𝐵 )
29 27 28 sylibr ⊢ ( ( 𝐶 ∖ 𝐴 ) = 𝐵 → 𝐶 ⊆ ( 𝐴 ∪ 𝐵 ) )
30 29 adantl ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐶 ∖ 𝐴 ) = 𝐵 ) → 𝐶 ⊆ ( 𝐴 ∪ 𝐵 ) )
31 26 30 eqssd ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐶 ∖ 𝐴 ) = 𝐵 ) → ( 𝐴 ∪ 𝐵 ) = 𝐶 )
32 31 ex ⊢ ( 𝐴 ⊆ 𝐶 → ( ( 𝐶 ∖ 𝐴 ) = 𝐵 → ( 𝐴 ∪ 𝐵 ) = 𝐶 ) )
33 32 adantr ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐶 ∖ 𝐴 ) = 𝐵 → ( 𝐴 ∪ 𝐵 ) = 𝐶 ) )
34 20 33 impbid ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐴 ∪ 𝐵 ) = 𝐶 ↔ ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )