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 ineqcom ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ ( 𝐵 ∩ 𝐴 ) = ∅ )
8 disj3 ⊢ ( ( 𝐵 ∩ 𝐴 ) = ∅ ↔ 𝐵 = ( 𝐵 ∖ 𝐴 ) )
9 7 8 bitri ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ ↔ 𝐵 = ( 𝐵 ∖ 𝐴 ) )
10 eqtr ⊢ ( ( ( 𝐶 ∖ 𝐴 ) = ( 𝐵 ∖ 𝐴 ) ∧ ( 𝐵 ∖ 𝐴 ) = 𝐵 ) → ( 𝐶 ∖ 𝐴 ) = 𝐵 )
11 10 expcom ⊢ ( ( 𝐵 ∖ 𝐴 ) = 𝐵 → ( ( 𝐶 ∖ 𝐴 ) = ( 𝐵 ∖ 𝐴 ) → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
12 11 eqcoms ⊢ ( 𝐵 = ( 𝐵 ∖ 𝐴 ) → ( ( 𝐶 ∖ 𝐴 ) = ( 𝐵 ∖ 𝐴 ) → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
13 9 12 sylbi ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐶 ∖ 𝐴 ) = ( 𝐵 ∖ 𝐴 ) → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
14 6 13 syl5com ⊢ ( ( ( 𝐶 ∖ 𝐴 ) = ( ( 𝐵 ∪ 𝐴 ) ∖ 𝐴 ) ∧ ( ( 𝐵 ∪ 𝐴 ) ∖ 𝐴 ) = ( 𝐵 ∖ 𝐴 ) ) → ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
15 4 5 14 sylancl ⊢ ( 𝐶 = ( 𝐵 ∪ 𝐴 ) → ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
16 3 15 syl ⊢ ( ( ( 𝐵 ∪ 𝐴 ) = ( 𝐴 ∪ 𝐵 ) ∧ ( 𝐴 ∪ 𝐵 ) = 𝐶 ) → ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
17 1 16 mpan ⊢ ( ( 𝐴 ∪ 𝐵 ) = 𝐶 → ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
18 17 com12 ⊢ ( ( 𝐴 ∩ 𝐵 ) = ∅ → ( ( 𝐴 ∪ 𝐵 ) = 𝐶 → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
19 18 adantl ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐴 ∪ 𝐵 ) = 𝐶 → ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )
20 simpl ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐶 ∖ 𝐴 ) = 𝐵 ) → 𝐴 ⊆ 𝐶 )
21 difssd ⊢ ( ( 𝐶 ∖ 𝐴 ) = 𝐵 → ( 𝐶 ∖ 𝐴 ) ⊆ 𝐶 )
22 sseq1 ⊢ ( ( 𝐶 ∖ 𝐴 ) = 𝐵 → ( ( 𝐶 ∖ 𝐴 ) ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶 ) )
23 21 22 mpbid ⊢ ( ( 𝐶 ∖ 𝐴 ) = 𝐵 → 𝐵 ⊆ 𝐶 )
24 23 adantl ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐶 ∖ 𝐴 ) = 𝐵 ) → 𝐵 ⊆ 𝐶 )
25 20 24 unssd ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐶 ∖ 𝐴 ) = 𝐵 ) → ( 𝐴 ∪ 𝐵 ) ⊆ 𝐶 )
26 eqimss ⊢ ( ( 𝐶 ∖ 𝐴 ) = 𝐵 → ( 𝐶 ∖ 𝐴 ) ⊆ 𝐵 )
27 ssundif ⊢ ( 𝐶 ⊆ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝐶 ∖ 𝐴 ) ⊆ 𝐵 )
28 26 27 sylibr ⊢ ( ( 𝐶 ∖ 𝐴 ) = 𝐵 → 𝐶 ⊆ ( 𝐴 ∪ 𝐵 ) )
29 28 adantl ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐶 ∖ 𝐴 ) = 𝐵 ) → 𝐶 ⊆ ( 𝐴 ∪ 𝐵 ) )
30 25 29 eqssd ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐶 ∖ 𝐴 ) = 𝐵 ) → ( 𝐴 ∪ 𝐵 ) = 𝐶 )
31 30 ex ⊢ ( 𝐴 ⊆ 𝐶 → ( ( 𝐶 ∖ 𝐴 ) = 𝐵 → ( 𝐴 ∪ 𝐵 ) = 𝐶 ) )
32 31 adantr ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐶 ∖ 𝐴 ) = 𝐵 → ( 𝐴 ∪ 𝐵 ) = 𝐶 ) )
33 19 32 impbid ⊢ ( ( 𝐴 ⊆ 𝐶 ∧ ( 𝐴 ∩ 𝐵 ) = ∅ ) → ( ( 𝐴 ∪ 𝐵 ) = 𝐶 ↔ ( 𝐶 ∖ 𝐴 ) = 𝐵 ) )