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 
|- ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) = C <-> ( C \ A ) = B ) )

Proof

Step Hyp Ref Expression
1 uncom 
 |-  ( B u. A ) = ( A u. B )
2 eqtr 
 |-  ( ( ( B u. A ) = ( A u. B ) /\ ( A u. B ) = C ) -> ( B u. A ) = C )
3 2 eqcomd 
 |-  ( ( ( B u. A ) = ( A u. B ) /\ ( A u. B ) = C ) -> C = ( B u. A ) )
4 difeq1 
 |-  ( C = ( B u. A ) -> ( C \ A ) = ( ( B u. A ) \ A ) )
5 difun2 
 |-  ( ( B u. A ) \ A ) = ( B \ A )
6 eqtr 
 |-  ( ( ( C \ A ) = ( ( B u. A ) \ A ) /\ ( ( B u. A ) \ A ) = ( B \ A ) ) -> ( C \ A ) = ( B \ A ) )
7 incom 
 |-  ( A i^i B ) = ( B i^i A )
8 7 eqeq1i 
 |-  ( ( A i^i B ) = (/) <-> ( B i^i A ) = (/) )
9 disj3 
 |-  ( ( B i^i A ) = (/) <-> B = ( B \ A ) )
10 8 9 bitri 
 |-  ( ( A i^i B ) = (/) <-> B = ( B \ A ) )
11 eqtr 
 |-  ( ( ( C \ A ) = ( B \ A ) /\ ( B \ A ) = B ) -> ( C \ A ) = B )
12 11 expcom 
 |-  ( ( B \ A ) = B -> ( ( C \ A ) = ( B \ A ) -> ( C \ A ) = B ) )
13 12 eqcoms 
 |-  ( B = ( B \ A ) -> ( ( C \ A ) = ( B \ A ) -> ( C \ A ) = B ) )
14 10 13 sylbi 
 |-  ( ( A i^i B ) = (/) -> ( ( C \ A ) = ( B \ A ) -> ( C \ A ) = B ) )
15 6 14 syl5com 
 |-  ( ( ( C \ A ) = ( ( B u. A ) \ A ) /\ ( ( B u. A ) \ A ) = ( B \ A ) ) -> ( ( A i^i B ) = (/) -> ( C \ A ) = B ) )
16 4 5 15 sylancl 
 |-  ( C = ( B u. A ) -> ( ( A i^i B ) = (/) -> ( C \ A ) = B ) )
17 3 16 syl 
 |-  ( ( ( B u. A ) = ( A u. B ) /\ ( A u. B ) = C ) -> ( ( A i^i B ) = (/) -> ( C \ A ) = B ) )
18 1 17 mpan 
 |-  ( ( A u. B ) = C -> ( ( A i^i B ) = (/) -> ( C \ A ) = B ) )
19 18 com12 
 |-  ( ( A i^i B ) = (/) -> ( ( A u. B ) = C -> ( C \ A ) = B ) )
20 19 adantl 
 |-  ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) = C -> ( C \ A ) = B ) )
21 simpl 
 |-  ( ( A C_ C /\ ( C \ A ) = B ) -> A C_ C )
22 difssd 
 |-  ( ( C \ A ) = B -> ( C \ A ) C_ C )
23 sseq1 
 |-  ( ( C \ A ) = B -> ( ( C \ A ) C_ C <-> B C_ C ) )
24 22 23 mpbid 
 |-  ( ( C \ A ) = B -> B C_ C )
25 24 adantl 
 |-  ( ( A C_ C /\ ( C \ A ) = B ) -> B C_ C )
26 21 25 unssd 
 |-  ( ( A C_ C /\ ( C \ A ) = B ) -> ( A u. B ) C_ C )
27 eqimss 
 |-  ( ( C \ A ) = B -> ( C \ A ) C_ B )
28 ssundif 
 |-  ( C C_ ( A u. B ) <-> ( C \ A ) C_ B )
29 27 28 sylibr 
 |-  ( ( C \ A ) = B -> C C_ ( A u. B ) )
30 29 adantl 
 |-  ( ( A C_ C /\ ( C \ A ) = B ) -> C C_ ( A u. B ) )
31 26 30 eqssd 
 |-  ( ( A C_ C /\ ( C \ A ) = B ) -> ( A u. B ) = C )
32 31 ex 
 |-  ( A C_ C -> ( ( C \ A ) = B -> ( A u. B ) = C ) )
33 32 adantr 
 |-  ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( C \ A ) = B -> ( A u. B ) = C ) )
34 20 33 impbid 
 |-  ( ( A C_ C /\ ( A i^i B ) = (/) ) -> ( ( A u. B ) = C <-> ( C \ A ) = B ) )