Theorem nnsucelrlem3 4427

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

Hypothesis

Ref	Expression
nnsucelrlem3.1	⊢ X ∈ V

Assertion

Ref	Expression
nnsucelrlem3	⊢ ((X ≠ Y ∧ (A ∪ {X}) = (B ∪ {Y}) ∧ ¬ Y ∈ B) → B = ((A ∖ {Y}) ∪ {X}))

Proof of Theorem nnsucelrlem3

Step	Hyp	Ref	Expression
1		indir 3504	. . . . 5 ⊢ ((B ∪ {Y}) ∩ ∼ {Y}) = ((B ∩ ∼ {Y}) ∪ ({Y} ∩ ∼ {Y}))
2		df-dif 3216	. . . . . . . 8 ⊢ (B ∖ {Y}) = (B ∩ ∼ {Y})
3	2	eqcomi 2357	. . . . . . 7 ⊢ (B ∩ ∼ {Y}) = (B ∖ {Y})
4		incompl 4074	. . . . . . 7 ⊢ ({Y} ∩ ∼ {Y}) = ∅
5	3, 4	uneq12i 3417	. . . . . 6 ⊢ ((B ∩ ∼ {Y}) ∪ ({Y} ∩ ∼ {Y})) = ((B ∖ {Y}) ∪ ∅)
6		un0 3576	. . . . . 6 ⊢ ((B ∖ {Y}) ∪ ∅) = (B ∖ {Y})
7	5, 6	eqtri 2373	. . . . 5 ⊢ ((B ∩ ∼ {Y}) ∪ ({Y} ∩ ∼ {Y})) = (B ∖ {Y})
8	1, 7	eqtri 2373	. . . 4 ⊢ ((B ∪ {Y}) ∩ ∼ {Y}) = (B ∖ {Y})
9		difsn 3846	. . . . 5 ⊢ (¬ Y ∈ B → (B ∖ {Y}) = B)
10	9	3ad2ant3 978	. . . 4 ⊢ ((X ≠ Y ∧ (A ∪ {X}) = (B ∪ {Y}) ∧ ¬ Y ∈ B) → (B ∖ {Y}) = B)
11	8, 10	syl5req 2398	. . 3 ⊢ ((X ≠ Y ∧ (A ∪ {X}) = (B ∪ {Y}) ∧ ¬ Y ∈ B) → B = ((B ∪ {Y}) ∩ ∼ {Y}))
12		simp2 956	. . . 4 ⊢ ((X ≠ Y ∧ (A ∪ {X}) = (B ∪ {Y}) ∧ ¬ Y ∈ B) → (A ∪ {X}) = (B ∪ {Y}))
13		df-ne 2519	. . . . . . . 8 ⊢ (X ≠ Y ↔ ¬ X = Y)
14	13	biimpi 186	. . . . . . 7 ⊢ (X ≠ Y → ¬ X = Y)
15	14	3ad2ant1 976	. . . . . 6 ⊢ ((X ≠ Y ∧ (A ∪ {X}) = (B ∪ {Y}) ∧ ¬ Y ∈ B) → ¬ X = Y)
16		nnsucelrlem3.1	. . . . . . . . 9 ⊢ X ∈ V
17	16	elcompl 3226	. . . . . . . 8 ⊢ (X ∈ ∼ {Y} ↔ ¬ X ∈ {Y})
18	16	elsnc 3757	. . . . . . . 8 ⊢ (X ∈ {Y} ↔ X = Y)
19	17, 18	xchbinx 301	. . . . . . 7 ⊢ (X ∈ ∼ {Y} ↔ ¬ X = Y)
20	16	snss 3839	. . . . . . 7 ⊢ (X ∈ ∼ {Y} ↔ {X} ⊆ ∼ {Y})
21	19, 20	bitr3i 242	. . . . . 6 ⊢ (¬ X = Y ↔ {X} ⊆ ∼ {Y})
22	15, 21	sylib 188	. . . . 5 ⊢ ((X ≠ Y ∧ (A ∪ {X}) = (B ∪ {Y}) ∧ ¬ Y ∈ B) → {X} ⊆ ∼ {Y})
23		ssequn2 3437	. . . . 5 ⊢ ({X} ⊆ ∼ {Y} ↔ ( ∼ {Y} ∪ {X}) = ∼ {Y})
24	22, 23	sylib 188	. . . 4 ⊢ ((X ≠ Y ∧ (A ∪ {X}) = (B ∪ {Y}) ∧ ¬ Y ∈ B) → ( ∼ {Y} ∪ {X}) = ∼ {Y})
25	12, 24	ineq12d 3459	. . 3 ⊢ ((X ≠ Y ∧ (A ∪ {X}) = (B ∪ {Y}) ∧ ¬ Y ∈ B) → ((A ∪ {X}) ∩ ( ∼ {Y} ∪ {X})) = ((B ∪ {Y}) ∩ ∼ {Y}))
26	11, 25	eqtr4d 2388	. 2 ⊢ ((X ≠ Y ∧ (A ∪ {X}) = (B ∪ {Y}) ∧ ¬ Y ∈ B) → B = ((A ∪ {X}) ∩ ( ∼ {Y} ∪ {X})))
27		df-dif 3216	. . . 4 ⊢ (A ∖ {Y}) = (A ∩ ∼ {Y})
28	27	uneq1i 3415	. . 3 ⊢ ((A ∖ {Y}) ∪ {X}) = ((A ∩ ∼ {Y}) ∪ {X})
29		undir 3505	. . 3 ⊢ ((A ∩ ∼ {Y}) ∪ {X}) = ((A ∪ {X}) ∩ ( ∼ {Y} ∪ {X}))
30	28, 29	eqtri 2373	. 2 ⊢ ((A ∖ {Y}) ∪ {X}) = ((A ∪ {X}) ∩ ( ∼ {Y} ∪ {X}))
31	26, 30	syl6eqr 2403	1 ⊢ ((X ≠ Y ∧ (A ∪ {X}) = (B ∪ {Y}) ∧ ¬ Y ∈ B) → B = ((A ∖ {Y}) ∪ {X}))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ w3a 934   = wceq 1642   ∈ wcel 1710   ≠ wne 2517  Vcvv 2860   ∼ ccompl 3206   ∖ cdif 3207   ∪ cun 3208   ∩ cin 3209   ⊆ wss 3258  ∅c0 3551  {csn 3738

This proof depends on 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 proof 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 2479  df-ne 2519  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-ss 3260  df-nul 3552  df-sn 3742

This theorem is used by:  nnsucelr  4429