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