Theorem ssunsn2 3866

Description: The property of being sandwiched between two sets naturally splits under union with a singleton. This is the induction hypothesis for the determination of large powersets such as pwtp 3885. (Contributed by Mario Carneiro, 2-Jul-2016.)

Assertion

Ref	Expression
ssunsn2	|- ((B C_ A /\ A C_ (C u. {D})) <-> ((B C_ A /\ A C_ C) \/ ((B u. {D}) C_ A /\ A C_ (C u. {D}))))

Proof of Theorem ssunsn2

Step	Hyp	Ref	Expression
1		snssi 3853	. . . . 5 |- (D e. A -> {D} C_ A)
2		unss 3438	. . . . . . 7 |- ((B C_ A /\ {D} C_ A) <-> (B u. {D}) C_ A)
3	2	bicomi 193	. . . . . 6 |- ((B u. {D}) C_ A <-> (B C_ A /\ {D} C_ A))
4	3	rbaibr 874	. . . . 5 |- ({D} C_ A -> (B C_ A <-> (B u. {D}) C_ A))
5	1, 4	syl 15	. . . 4 |- (D e. A -> (B C_ A <-> (B u. {D}) C_ A))
6	5	anbi1d 685	. . 3 |- (D e. A -> ((B C_ A /\ A C_ (C u. {D})) <-> ((B u. {D}) C_ A /\ A C_ (C u. {D}))))
7	2	biimpi 186	. . . . . . 7 |- ((B C_ A /\ {D} C_ A) -> (B u. {D}) C_ A)
8	7	expcom 424	. . . . . 6 |- ({D} C_ A -> (B C_ A -> (B u. {D}) C_ A))
9	1, 8	syl 15	. . . . 5 |- (D e. A -> (B C_ A -> (B u. {D}) C_ A))
10		ssun3 3429	. . . . . 6 |- (A C_ C -> A C_ (C u. {D}))
11	10	a1i 10	. . . . 5 |- (D e. A -> (A C_ C -> A C_ (C u. {D})))
12	9, 11	anim12d 546	. . . 4 |- (D e. A -> ((B C_ A /\ A C_ C) -> ((B u. {D}) C_ A /\ A C_ (C u. {D}))))
13		pm4.72 846	. . . 4 |- (((B C_ A /\ A C_ C) -> ((B u. {D}) C_ A /\ A C_ (C u. {D}))) <-> (((B u. {D}) C_ A /\ A C_ (C u. {D})) <-> ((B C_ A /\ A C_ C) \/ ((B u. {D}) C_ A /\ A C_ (C u. {D})))))
14	12, 13	sylib 188	. . 3 |- (D e. A -> (((B u. {D}) C_ A /\ A C_ (C u. {D})) <-> ((B C_ A /\ A C_ C) \/ ((B u. {D}) C_ A /\ A C_ (C u. {D})))))
15	6, 14	bitrd 244	. 2 |- (D e. A -> ((B C_ A /\ A C_ (C u. {D})) <-> ((B C_ A /\ A C_ C) \/ ((B u. {D}) C_ A /\ A C_ (C u. {D})))))
16		disjsn 3787	. . . . . . 7 |- ((A i^i {D}) = (/) <-> -. D e. A)
17		disj3 3596	. . . . . . 7 |- ((A i^i {D}) = (/) <-> A = (A \ {D}))
18	16, 17	bitr3i 242	. . . . . 6 |- (-. D e. A <-> A = (A \ {D}))
19		sseq1 3293	. . . . . 6 |- (A = (A \ {D}) -> (A C_ C <-> (A \ {D}) C_ C))
20	18, 19	sylbi 187	. . . . 5 |- (-. D e. A -> (A C_ C <-> (A \ {D}) C_ C))
21		uncom 3409	. . . . . . 7 |- ({D} u. C) = (C u. {D})
22	21	sseq2i 3297	. . . . . 6 |- (A C_ ({D} u. C) <-> A C_ (C u. {D}))
23		ssundif 3634	. . . . . 6 |- (A C_ ({D} u. C) <-> (A \ {D}) C_ C)
24	22, 23	bitr3i 242	. . . . 5 |- (A C_ (C u. {D}) <-> (A \ {D}) C_ C)
25	20, 24	syl6rbbr 255	. . . 4 |- (-. D e. A -> (A C_ (C u. {D}) <-> A C_ C))
26	25	anbi2d 684	. . 3 |- (-. D e. A -> ((B C_ A /\ A C_ (C u. {D})) <-> (B C_ A /\ A C_ C)))
27	3	simplbi 446	. . . . . . 7 |- ((B u. {D}) C_ A -> B C_ A)
28	27	a1i 10	. . . . . 6 |- (-. D e. A -> ((B u. {D}) C_ A -> B C_ A))
29	25	biimpd 198	. . . . . 6 |- (-. D e. A -> (A C_ (C u. {D}) -> A C_ C))
30	28, 29	anim12d 546	. . . . 5 |- (-. D e. A -> (((B u. {D}) C_ A /\ A C_ (C u. {D})) -> (B C_ A /\ A C_ C)))
31		pm4.72 846	. . . . 5 |- ((((B u. {D}) C_ A /\ A C_ (C u. {D})) -> (B C_ A /\ A C_ C)) <-> ((B C_ A /\ A C_ C) <-> (((B u. {D}) C_ A /\ A C_ (C u. {D})) \/ (B C_ A /\ A C_ C))))
32	30, 31	sylib 188	. . . 4 |- (-. D e. A -> ((B C_ A /\ A C_ C) <-> (((B u. {D}) C_ A /\ A C_ (C u. {D})) \/ (B C_ A /\ A C_ C))))
33		orcom 376	. . . 4 |- ((((B u. {D}) C_ A /\ A C_ (C u. {D})) \/ (B C_ A /\ A C_ C)) <-> ((B C_ A /\ A C_ C) \/ ((B u. {D}) C_ A /\ A C_ (C u. {D}))))
34	32, 33	syl6bb 252	. . 3 |- (-. D e. A -> ((B C_ A /\ A C_ C) <-> ((B C_ A /\ A C_ C) \/ ((B u. {D}) C_ A /\ A C_ (C u. {D})))))
35	26, 34	bitrd 244	. 2 |- (-. D e. A -> ((B C_ A /\ A C_ (C u. {D})) <-> ((B C_ A /\ A C_ C) \/ ((B u. {D}) C_ A /\ A C_ (C u. {D})))))
36	15, 35	pm2.61i 156	1 |- ((B C_ A /\ A C_ (C u. {D})) <-> ((B C_ A /\ A C_ C) \/ ((B u. {D}) C_ A /\ A C_ (C u. {D}))))

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   \/ wo 357   /\ wa 358   = wceq 1642   e. wcel 1710   \ cdif 3207   u. cun 3208   i^i cin 3209   C_ wss 3258  (/)c0 3551  {csn 3738

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  df-sn 3742

This theorem is referenced by:  ssunsn  3867  ssunpr  3869  sstp  3871