Theorem uneqdifeq 3639

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.)

Assertion

Ref	Expression
uneqdifeq	|- ((A C_ C /\ (A i^i B) = (/)) -> ((A u. B) = C <-> (C \ A) = B))

Proof of Theorem uneqdifeq

Step	Hyp	Ref	Expression
1		uncom 3409	. . . . 5 |- (B u. A) = (A u. B)
2		eqtr 2370	. . . . . . 7 |- (((B u. A) = (A u. B) /\ (A u. B) = C) -> (B u. A) = C)
3	2	eqcomd 2358	. . . . . 6 |- (((B u. A) = (A u. B) /\ (A u. B) = C) -> C = (B u. A))
4		difeq1 3247	. . . . . . 7 |- (C = (B u. A) -> (C \ A) = ((B u. A) \ A))
5		difun2 3630	. . . . . . 7 |- ((B u. A) \ A) = (B \ A)
6		eqtr 2370	. . . . . . . 8 |- (((C \ A) = ((B u. A) \ A) /\ ((B u. A) \ A) = (B \ A)) -> (C \ A) = (B \ A))
7		incom 3449	. . . . . . . . . . 11 |- (A i^i B) = (B i^i A)
8	7	eqeq1i 2360	. . . . . . . . . 10 |- ((A i^i B) = (/) <-> (B i^i A) = (/))
9		disj3 3596	. . . . . . . . . 10 |- ((B i^i A) = (/) <-> B = (B \ A))
10	8, 9	bitri 240	. . . . . . . . 9 |- ((A i^i B) = (/) <-> B = (B \ A))
11		eqtr 2370	. . . . . . . . . . 11 |- (((C \ A) = (B \ A) /\ (B \ A) = B) -> (C \ A) = B)
12	11	expcom 424	. . . . . . . . . 10 |- ((B \ A) = B -> ((C \ A) = (B \ A) -> (C \ A) = B))
13	12	eqcoms 2356	. . . . . . . . 9 |- (B = (B \ A) -> ((C \ A) = (B \ A) -> (C \ A) = B))
14	10, 13	sylbi 187	. . . . . . . 8 |- ((A i^i B) = (/) -> ((C \ A) = (B \ A) -> (C \ A) = B))
15	6, 14	syl5com 26	. . . . . . 7 |- (((C \ A) = ((B u. A) \ A) /\ ((B u. A) \ A) = (B \ A)) -> ((A i^i B) = (/) -> (C \ A) = B))
16	4, 5, 15	sylancl 643	. . . . . 6 |- (C = (B u. A) -> ((A i^i B) = (/) -> (C \ A) = B))
17	3, 16	syl 15	. . . . 5 |- (((B u. A) = (A u. B) /\ (A u. B) = C) -> ((A i^i B) = (/) -> (C \ A) = B))
18	1, 17	mpan 651	. . . 4 |- ((A u. B) = C -> ((A i^i B) = (/) -> (C \ A) = B))
19	18	com12 27	. . 3 |- ((A i^i B) = (/) -> ((A u. B) = C -> (C \ A) = B))
20	19	adantl 452	. 2 |- ((A C_ C /\ (A i^i B) = (/)) -> ((A u. B) = C -> (C \ A) = B))
21		difss 3394	. . . . . . . 8 |- (C \ A) C_ C
22		sseq1 3293	. . . . . . . . 9 |- ((C \ A) = B -> ((C \ A) C_ C <-> B C_ C))
23		unss 3438	. . . . . . . . . . 11 |- ((A C_ C /\ B C_ C) <-> (A u. B) C_ C)
24	23	biimpi 186	. . . . . . . . . 10 |- ((A C_ C /\ B C_ C) -> (A u. B) C_ C)
25	24	expcom 424	. . . . . . . . 9 |- (B C_ C -> (A C_ C -> (A u. B) C_ C))
26	22, 25	syl6bi 219	. . . . . . . 8 |- ((C \ A) = B -> ((C \ A) C_ C -> (A C_ C -> (A u. B) C_ C)))
27	21, 26	mpi 16	. . . . . . 7 |- ((C \ A) = B -> (A C_ C -> (A u. B) C_ C))
28	27	com12 27	. . . . . 6 |- (A C_ C -> ((C \ A) = B -> (A u. B) C_ C))
29	28	adantr 451	. . . . 5 |- ((A C_ C /\ (A i^i B) = (/)) -> ((C \ A) = B -> (A u. B) C_ C))
30	29	imp 418	. . . 4 |- (((A C_ C /\ (A i^i B) = (/)) /\ (C \ A) = B) -> (A u. B) C_ C)
31		eqimss 3324	. . . . . . 7 |- ((C \ A) = B -> (C \ A) C_ B)
32	31	adantl 452	. . . . . 6 |- ((A C_ C /\ (C \ A) = B) -> (C \ A) C_ B)
33		ssundif 3634	. . . . . 6 |- (C C_ (A u. B) <-> (C \ A) C_ B)
34	32, 33	sylibr 203	. . . . 5 |- ((A C_ C /\ (C \ A) = B) -> C C_ (A u. B))
35	34	adantlr 695	. . . 4 |- (((A C_ C /\ (A i^i B) = (/)) /\ (C \ A) = B) -> C C_ (A u. B))
36	30, 35	eqssd 3290	. . 3 |- (((A C_ C /\ (A i^i B) = (/)) /\ (C \ A) = B) -> (A u. B) = C)
37	36	ex 423	. 2 |- ((A C_ C /\ (A i^i B) = (/)) -> ((C \ A) = B -> (A u. B) = C))
38	20, 37	impbid 183	1 |- ((A C_ C /\ (A i^i B) = (/)) -> ((A u. B) = C <-> (C \ A) = B))

Syntax hints:   -> wi 4   <-> wb 176   /\ wa 358   = wceq 1642   \ cdif 3207   u. cun 3208   i^i cin 3209   C_ wss 3258  (/)c0 3551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-ss 3260  df-nul 3552

This theorem is referenced by: (None)