ssunsn2 - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > ssunsn2		Unicode version

Theorem ssunsn2 3865

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 3884. (Contributed by Mario Carneiro, 2-Jul-2016.)

**Assertion**
Ref	Expression
ssunsn2	$/\$ $/\$ $\/$ $/\$

**Proof of Theorem ssunsn2**
Step	Hyp	Ref	Expression
1		snssi 3852	. . . . 5
2		unss 3437	. . . . . . 7 $/\$
3	2	bicomi 193	. . . . . 6 $/\$
4	3	rbaibr 874	. . . . 5
5	1, 4	syl 15	. . . 4
6	5	anbi1d 685	. . 3 $/\$ $/\$
7	2	biimpi 186	. . . . . . 7 $/\$
8	7	expcom 424	. . . . . 6
9	1, 8	syl 15	. . . . 5
10		ssun3 3428	. . . . . 6
11	10	a1i 10	. . . . 5
12	9, 11	anim12d 546	. . . 4 $/\$ $/\$
13		pm4.72 846	. . . 4 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
14	12, 13	sylib 188	. . 3 $/\$ $/\$ $\/$ $/\$
15	6, 14	bitrd 244	. 2 $/\$ $/\$ $\/$ $/\$
16		disjsn 3786	. . . . . . 7
17		disj3 3595	. . . . . . 7
18	16, 17	bitr3i 242	. . . . . 6
19		sseq1 3292	. . . . . 6
20	18, 19	sylbi 187	. . . . 5
21		uncom 3408	. . . . . . 7
22	21	sseq2i 3296	. . . . . 6
23		ssundif 3633	. . . . . 6
24	22, 23	bitr3i 242	. . . . 5
25	20, 24	syl6rbbr 255	. . . 4
26	25	anbi2d 684	. . 3 $/\$ $/\$
27	3	simplbi 446	. . . . . . 7
28	27	a1i 10	. . . . . 6
29	25	biimpd 198	. . . . . 6
30	28, 29	anim12d 546	. . . . 5 $/\$ $/\$
31		pm4.72 846	. . . . 5 $/\$ $/\$ $/\$ $/\$ $\/$ $/\$
32	30, 31	sylib 188	. . . 4 $/\$ $/\$ $\/$ $/\$
33		orcom 376	. . . 4 $/\$ $\/$ $/\$ $/\$ $\/$ $/\$
34	32, 33	syl6bb 252	. . 3 $/\$ $/\$ $\/$ $/\$
35	26, 34	bitrd 244	. 2 $/\$ $/\$ $\/$ $/\$
36	15, 35	pm2.61i 156	1 $/\$ $/\$ $\/$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 176 $\/$ wo 357 $/\$ wa 358

wceq 1642

wcel 1710

cdif 3206

cun 3207

cin 3208

wss 3257

c0 3550

csn 3737

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 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 2478 df-ne 2518 df-ral 2619 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: ssunsn 3866 ssunpr 3868 sstp 3870

W3C validator