Theorem nnsucelrlem3 4426

Description: Lemma for nnsucelr 4428. Rearrange union and difference for a particular group of classes. (Contributed by SF, 15-Jan-2015.)

Hypothesis

Ref	Expression
nnsucelrlem3.1	|- X e. _V

Assertion

Ref	Expression
nnsucelrlem3	|- ((X =/= Y /\ (A u. {X}) = (B u. {Y}) /\ -. Y e. B) -> B = ((A \ {Y}) u. {X}))

Proof of Theorem nnsucelrlem3

Step	Hyp	Ref	Expression
1		indir 3503	. . . . 5 |- ((B u. {Y}) i^i ∼ {Y}) = ((B i^i ∼ {Y}) u. ({Y} i^i ∼ {Y}))
2		df-dif 3215	. . . . . . . 8 |- (B \ {Y}) = (B i^i ∼ {Y})
3	2	eqcomi 2357	. . . . . . 7 |- (B i^i ∼ {Y}) = (B \ {Y})
4		incompl 4073	. . . . . . 7 |- ({Y} i^i ∼ {Y}) = (/)
5	3, 4	uneq12i 3416	. . . . . 6 |- ((B i^i ∼ {Y}) u. ({Y} i^i ∼ {Y})) = ((B \ {Y}) u. (/))
6		un0 3575	. . . . . 6 |- ((B \ {Y}) u. (/)) = (B \ {Y})
7	5, 6	eqtri 2373	. . . . 5 |- ((B i^i ∼ {Y}) u. ({Y} i^i ∼ {Y})) = (B \ {Y})
8	1, 7	eqtri 2373	. . . 4 |- ((B u. {Y}) i^i ∼ {Y}) = (B \ {Y})
9		difsn 3845	. . . . 5 |- (-. Y e. B -> (B \ {Y}) = B)
10	9	3ad2ant3 978	. . . 4 |- ((X =/= Y /\ (A u. {X}) = (B u. {Y}) /\ -. Y e. B) -> (B \ {Y}) = B)
11	8, 10	syl5req 2398	. . 3 |- ((X =/= Y /\ (A u. {X}) = (B u. {Y}) /\ -. Y e. B) -> B = ((B u. {Y}) i^i ∼ {Y}))
12		simp2 956	. . . 4 |- ((X =/= Y /\ (A u. {X}) = (B u. {Y}) /\ -. Y e. B) -> (A u. {X}) = (B u. {Y}))
13		df-ne 2518	. . . . . . . 8 |- (X =/= Y <-> -. X = Y)
14	13	biimpi 186	. . . . . . 7 |- (X =/= Y -> -. X = Y)
15	14	3ad2ant1 976	. . . . . 6 |- ((X =/= Y /\ (A u. {X}) = (B u. {Y}) /\ -. Y e. B) -> -. X = Y)
16		nnsucelrlem3.1	. . . . . . . . 9 |- X e. _V
17	16	elcompl 3225	. . . . . . . 8 |- (X e. ∼ {Y} <-> -. X e. {Y})
18	16	elsnc 3756	. . . . . . . 8 |- (X e. {Y} <-> X = Y)
19	17, 18	xchbinx 301	. . . . . . 7 |- (X e. ∼ {Y} <-> -. X = Y)
20	16	snss 3838	. . . . . . 7 |- (X e. ∼ {Y} <-> {X} C_ ∼ {Y})
21	19, 20	bitr3i 242	. . . . . 6 |- (-. X = Y <-> {X} C_ ∼ {Y})
22	15, 21	sylib 188	. . . . 5 |- ((X =/= Y /\ (A u. {X}) = (B u. {Y}) /\ -. Y e. B) -> {X} C_ ∼ {Y})
23		ssequn2 3436	. . . . 5 |- ({X} C_ ∼ {Y} <-> ( ∼ {Y} u. {X}) = ∼ {Y})
24	22, 23	sylib 188	. . . 4 |- ((X =/= Y /\ (A u. {X}) = (B u. {Y}) /\ -. Y e. B) -> ( ∼ {Y} u. {X}) = ∼ {Y})
25	12, 24	ineq12d 3458	. . 3 |- ((X =/= Y /\ (A u. {X}) = (B u. {Y}) /\ -. Y e. B) -> ((A u. {X}) i^i ( ∼ {Y} u. {X})) = ((B u. {Y}) i^i ∼ {Y}))
26	11, 25	eqtr4d 2388	. 2 |- ((X =/= Y /\ (A u. {X}) = (B u. {Y}) /\ -. Y e. B) -> B = ((A u. {X}) i^i ( ∼ {Y} u. {X})))
27		df-dif 3215	. . . 4 |- (A \ {Y}) = (A i^i ∼ {Y})
28	27	uneq1i 3414	. . 3 |- ((A \ {Y}) u. {X}) = ((A i^i ∼ {Y}) u. {X})
29		undir 3504	. . 3 |- ((A i^i ∼ {Y}) u. {X}) = ((A u. {X}) i^i ( ∼ {Y} u. {X}))
30	28, 29	eqtri 2373	. 2 |- ((A \ {Y}) u. {X}) = ((A u. {X}) i^i ( ∼ {Y} u. {X}))
31	26, 30	syl6eqr 2403	1 |- ((X =/= Y /\ (A u. {X}) = (B u. {Y}) /\ -. Y e. B) -> B = ((A \ {Y}) u. {X}))

Syntax hints:  -. wn 3   -> wi 4   /\ w3a 934   = wceq 1642   e. wcel 1710   =/= wne 2516  _Vcvv 2859   ∼ ccompl 3205   \ cdif 3206   u. cun 3207   i^i cin 3208   C_ wss 3257  (/)c0 3550  {csn 3737

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-3an 936  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 2478  df-ne 2518  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-ss 3259  df-nul 3551  df-sn 3741

This theorem is referenced by:  nnsucelr  4428