Theorem ssunsn2

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

	Ref	Expression
Assertion	ssunsn2	$$⊢\left(B\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\leftrightarrow \left(\left(B\subseteq A\wedge A\subseteq C\right)\vee \left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		snssi	$$⊢D\in A\to \left\{D\right\}\subseteq A$$
2		unss	$$⊢\left(B\subseteq A\wedge \left\{D\right\}\subseteq A\right)\leftrightarrow B\cup \left\{D\right\}\subseteq A$$
3	2	bicomi	$$⊢B\cup \left\{D\right\}\subseteq A\leftrightarrow \left(B\subseteq A\wedge \left\{D\right\}\subseteq A\right)$$
4	3	rbaibr	$$⊢\left\{D\right\}\subseteq A\to \left(B\subseteq A\leftrightarrow B\cup \left\{D\right\}\subseteq A\right)$$
5	1 4	syl	$$⊢D\in A\to \left(B\subseteq A\leftrightarrow B\cup \left\{D\right\}\subseteq A\right)$$
6	5	anbi1d	$$⊢D\in A\to \left(\left(B\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\leftrightarrow \left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\right)$$
7	2	biimpi	$$⊢\left(B\subseteq A\wedge \left\{D\right\}\subseteq A\right)\to B\cup \left\{D\right\}\subseteq A$$
8	7	expcom	$$⊢\left\{D\right\}\subseteq A\to \left(B\subseteq A\to B\cup \left\{D\right\}\subseteq A\right)$$
9	1 8	syl	$$⊢D\in A\to \left(B\subseteq A\to B\cup \left\{D\right\}\subseteq A\right)$$
10		ssun3	$$⊢A\subseteq C\to A\subseteq C\cup \left\{D\right\}$$
11	10	a1i	$$⊢D\in A\to \left(A\subseteq C\to A\subseteq C\cup \left\{D\right\}\right)$$
12	9 11	anim12d	$$⊢D\in A\to \left(\left(B\subseteq A\wedge A\subseteq C\right)\to \left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\right)$$
13		pm4.72	$$⊢\left(\left(B\subseteq A\wedge A\subseteq C\right)\to \left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\right)\leftrightarrow \left(\left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\leftrightarrow \left(\left(B\subseteq A\wedge A\subseteq C\right)\vee \left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\right)\right)$$
14	12 13	sylib	$$⊢D\in A\to \left(\left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\leftrightarrow \left(\left(B\subseteq A\wedge A\subseteq C\right)\vee \left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\right)\right)$$
15	6 14	bitrd	$$⊢D\in A\to \left(\left(B\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\leftrightarrow \left(\left(B\subseteq A\wedge A\subseteq C\right)\vee \left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\right)\right)$$
16		uncom	$$⊢\left\{D\right\}\cup C=C\cup \left\{D\right\}$$
17	16	sseq2i	$$⊢A\subseteq \left\{D\right\}\cup C\leftrightarrow A\subseteq C\cup \left\{D\right\}$$
18		ssundif	$$⊢A\subseteq \left\{D\right\}\cup C\leftrightarrow A\setminus \left\{D\right\}\subseteq C$$
19	17 18	bitr3i	$$⊢A\subseteq C\cup \left\{D\right\}\leftrightarrow A\setminus \left\{D\right\}\subseteq C$$
20		disjsn	$$⊢A\cap \left\{D\right\}=\varnothing \leftrightarrow \neg D\in A$$
21		disj3	$$⊢A\cap \left\{D\right\}=\varnothing \leftrightarrow A=A\setminus \left\{D\right\}$$
22	20 21	bitr3i	$$⊢\neg D\in A\leftrightarrow A=A\setminus \left\{D\right\}$$
23		sseq1	$$⊢A=A\setminus \left\{D\right\}\to \left(A\subseteq C\leftrightarrow A\setminus \left\{D\right\}\subseteq C\right)$$
24	22 23	sylbi	$$⊢\neg D\in A\to \left(A\subseteq C\leftrightarrow A\setminus \left\{D\right\}\subseteq C\right)$$
25	19 24	bitr4id	$$⊢\neg D\in A\to \left(A\subseteq C\cup \left\{D\right\}\leftrightarrow A\subseteq C\right)$$
26	25	anbi2d	$$⊢\neg D\in A\to \left(\left(B\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\leftrightarrow \left(B\subseteq A\wedge A\subseteq C\right)\right)$$
27	3	simplbi	$$⊢B\cup \left\{D\right\}\subseteq A\to B\subseteq A$$
28	27	a1i	$$⊢\neg D\in A\to \left(B\cup \left\{D\right\}\subseteq A\to B\subseteq A\right)$$
29	25	biimpd	$$⊢\neg D\in A\to \left(A\subseteq C\cup \left\{D\right\}\to A\subseteq C\right)$$
30	28 29	anim12d	$$⊢\neg D\in A\to \left(\left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\to \left(B\subseteq A\wedge A\subseteq C\right)\right)$$
31		pm4.72	$$⊢\left(\left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\to \left(B\subseteq A\wedge A\subseteq C\right)\right)\leftrightarrow \left(\left(B\subseteq A\wedge A\subseteq C\right)\leftrightarrow \left(\left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\vee \left(B\subseteq A\wedge A\subseteq C\right)\right)\right)$$
32	30 31	sylib	$$⊢\neg D\in A\to \left(\left(B\subseteq A\wedge A\subseteq C\right)\leftrightarrow \left(\left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\vee \left(B\subseteq A\wedge A\subseteq C\right)\right)\right)$$
33		orcom	$$⊢\left(\left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\vee \left(B\subseteq A\wedge A\subseteq C\right)\right)\leftrightarrow \left(\left(B\subseteq A\wedge A\subseteq C\right)\vee \left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\right)$$
34	32 33	bitrdi	$$⊢\neg D\in A\to \left(\left(B\subseteq A\wedge A\subseteq C\right)\leftrightarrow \left(\left(B\subseteq A\wedge A\subseteq C\right)\vee \left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\right)\right)$$
35	26 34	bitrd	$$⊢\neg D\in A\to \left(\left(B\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\leftrightarrow \left(\left(B\subseteq A\wedge A\subseteq C\right)\vee \left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\right)\right)$$
36	15 35	pm2.61i	$$⊢\left(B\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\leftrightarrow \left(\left(B\subseteq A\wedge A\subseteq C\right)\vee \left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq C\cup \left\{D\right\}\right)\right)$$