Theorem uneqdifeq 4432

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

Assertion

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

Proof of Theorem uneqdifeq

Step	Hyp	Ref	Expression
1		uncom 4098	. . . . 5 ⊢ (𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵)
2		eqtr 2756	. . . . . . 7 ⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → (𝐵 ∪ 𝐴) = 𝐶)
3	2	eqcomd 2742	. . . . . 6 ⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → 𝐶 = (𝐵 ∪ 𝐴))
4		difeq1 4059	. . . . . . 7 ⊢ (𝐶 = (𝐵 ∪ 𝐴) → (𝐶 ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴))
5		difun2 4421	. . . . . . 7 ⊢ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴)
6		eqtr 2756	. . . . . . . 8 ⊢ (((𝐶 ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴) ∧ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴)) → (𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴))
7		ineqcom 4150	. . . . . . . . . 10 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ (𝐵 ∩ 𝐴) = ∅)
8		disj3 4394	. . . . . . . . . 10 ⊢ ((𝐵 ∩ 𝐴) = ∅ ↔ 𝐵 = (𝐵 ∖ 𝐴))
9	7, 8	bitri 275	. . . . . . . . 9 ⊢ ((𝐴 ∩ 𝐵) = ∅ ↔ 𝐵 = (𝐵 ∖ 𝐴))
10		eqtr 2756	. . . . . . . . . . 11 ⊢ (((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) ∧ (𝐵 ∖ 𝐴) = 𝐵) → (𝐶 ∖ 𝐴) = 𝐵)
11	10	expcom 413	. . . . . . . . . 10 ⊢ ((𝐵 ∖ 𝐴) = 𝐵 → ((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) → (𝐶 ∖ 𝐴) = 𝐵))
12	11	eqcoms 2744	. . . . . . . . 9 ⊢ (𝐵 = (𝐵 ∖ 𝐴) → ((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) → (𝐶 ∖ 𝐴) = 𝐵))
13	9, 12	sylbi 217	. . . . . . . 8 ⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐶 ∖ 𝐴) = (𝐵 ∖ 𝐴) → (𝐶 ∖ 𝐴) = 𝐵))
14	6, 13	syl5com 31	. . . . . . 7 ⊢ (((𝐶 ∖ 𝐴) = ((𝐵 ∪ 𝐴) ∖ 𝐴) ∧ ((𝐵 ∪ 𝐴) ∖ 𝐴) = (𝐵 ∖ 𝐴)) → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
15	4, 5, 14	sylancl 587	. . . . . 6 ⊢ (𝐶 = (𝐵 ∪ 𝐴) → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
16	3, 15	syl 17	. . . . 5 ⊢ (((𝐵 ∪ 𝐴) = (𝐴 ∪ 𝐵) ∧ (𝐴 ∪ 𝐵) = 𝐶) → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
17	1, 16	mpan 691	. . . 4 ⊢ ((𝐴 ∪ 𝐵) = 𝐶 → ((𝐴 ∩ 𝐵) = ∅ → (𝐶 ∖ 𝐴) = 𝐵))
18	17	com12 32	. . 3 ⊢ ((𝐴 ∩ 𝐵) = ∅ → ((𝐴 ∪ 𝐵) = 𝐶 → (𝐶 ∖ 𝐴) = 𝐵))
19	18	adantl 481	. 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 → (𝐶 ∖ 𝐴) = 𝐵))
20		simpl 482	. . . . . 6 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → 𝐴 ⊆ 𝐶)
21		difssd 4077	. . . . . . . 8 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → (𝐶 ∖ 𝐴) ⊆ 𝐶)
22		sseq1 3947	. . . . . . . 8 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → ((𝐶 ∖ 𝐴) ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶))
23	21, 22	mpbid 232	. . . . . . 7 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → 𝐵 ⊆ 𝐶)
24	23	adantl 481	. . . . . 6 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → 𝐵 ⊆ 𝐶)
25	20, 24	unssd 4132	. . . . 5 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → (𝐴 ∪ 𝐵) ⊆ 𝐶)
26		eqimss 3980	. . . . . . 7 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → (𝐶 ∖ 𝐴) ⊆ 𝐵)
27		ssundif 4427	. . . . . . 7 ⊢ (𝐶 ⊆ (𝐴 ∪ 𝐵) ↔ (𝐶 ∖ 𝐴) ⊆ 𝐵)
28	26, 27	sylibr 234	. . . . . 6 ⊢ ((𝐶 ∖ 𝐴) = 𝐵 → 𝐶 ⊆ (𝐴 ∪ 𝐵))
29	28	adantl 481	. . . . 5 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → 𝐶 ⊆ (𝐴 ∪ 𝐵))
30	25, 29	eqssd 3939	. . . 4 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐶 ∖ 𝐴) = 𝐵) → (𝐴 ∪ 𝐵) = 𝐶)
31	30	ex 412	. . 3 ⊢ (𝐴 ⊆ 𝐶 → ((𝐶 ∖ 𝐴) = 𝐵 → (𝐴 ∪ 𝐵) = 𝐶))
32	31	adantr 480	. 2 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐶 ∖ 𝐴) = 𝐵 → (𝐴 ∪ 𝐵) = 𝐶))
33	19, 32	impbid 212	1 ⊢ ((𝐴 ⊆ 𝐶 ∧ (𝐴 ∩ 𝐵) = ∅) → ((𝐴 ∪ 𝐵) = 𝐶 ↔ (𝐶 ∖ 𝐴) = 𝐵))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∖ cdif 3886   ∪ cun 3887   ∩ cin 3888   ⊆ wss 3889  ∅c0 4273

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274

This theorem is referenced by:  fzdifsuc  13538  hashbclem  14414  lecldbas  23184  conndisj  23381  ptuncnv  23772  ptunhmeo  23773  cldsubg  24076  icopnfcld  24732  iocmnfcld  24733  voliunlem1  25517  icombl  25531  ioombl  25532  uniioombllem4  25553  ismbf3d  25621  lhop  25983  symgcom  33144  f1resfz0f1d  35296  subfacp1lem3  35364  subfacp1lem5  35366  pconnconn  35413  cvmscld  35455