Theorem ssunpr

Description: Possible values for a set sandwiched between another set and it plus a singleton. (Contributed by Mario Carneiro, 2-Jul-2016)

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

Proof

Step	Hyp	Ref	Expression
1		df-pr	$$⊢\left\{C,D\right\}=\left\{C\right\}\cup \left\{D\right\}$$
2	1	uneq2i	$$⊢B\cup \left\{C,D\right\}=B\cup \left(\left\{C\right\}\cup \left\{D\right\}\right)$$
3		unass	$$⊢\left(B\cup \left\{C\right\}\right)\cup \left\{D\right\}=B\cup \left(\left\{C\right\}\cup \left\{D\right\}\right)$$
4	2 3	eqtr4i	$$⊢B\cup \left\{C,D\right\}=\left(B\cup \left\{C\right\}\right)\cup \left\{D\right\}$$
5	4	sseq2i	$$⊢A\subseteq B\cup \left\{C,D\right\}\leftrightarrow A\subseteq \left(B\cup \left\{C\right\}\right)\cup \left\{D\right\}$$
6	5	anbi2i	$$⊢\left(B\subseteq A\wedge A\subseteq B\cup \left\{C,D\right\}\right)\leftrightarrow \left(B\subseteq A\wedge A\subseteq \left(B\cup \left\{C\right\}\right)\cup \left\{D\right\}\right)$$
7		ssunsn2	$$⊢\left(B\subseteq A\wedge A\subseteq \left(B\cup \left\{C\right\}\right)\cup \left\{D\right\}\right)\leftrightarrow \left(\left(B\subseteq A\wedge A\subseteq B\cup \left\{C\right\}\right)\vee \left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq \left(B\cup \left\{C\right\}\right)\cup \left\{D\right\}\right)\right)$$
8		ssunsn	$$⊢\left(B\subseteq A\wedge A\subseteq B\cup \left\{C\right\}\right)\leftrightarrow \left(A=B\vee A=B\cup \left\{C\right\}\right)$$
9		un23	$$⊢\left(B\cup \left\{C\right\}\right)\cup \left\{D\right\}=\left(B\cup \left\{D\right\}\right)\cup \left\{C\right\}$$
10	9	sseq2i	$$⊢A\subseteq \left(B\cup \left\{C\right\}\right)\cup \left\{D\right\}\leftrightarrow A\subseteq \left(B\cup \left\{D\right\}\right)\cup \left\{C\right\}$$
11	10	anbi2i	$$⊢\left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq \left(B\cup \left\{C\right\}\right)\cup \left\{D\right\}\right)\leftrightarrow \left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq \left(B\cup \left\{D\right\}\right)\cup \left\{C\right\}\right)$$
12		ssunsn	$$⊢\left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq \left(B\cup \left\{D\right\}\right)\cup \left\{C\right\}\right)\leftrightarrow \left(A=B\cup \left\{D\right\}\vee A=\left(B\cup \left\{D\right\}\right)\cup \left\{C\right\}\right)$$
13	4 9	eqtr2i	$$⊢\left(B\cup \left\{D\right\}\right)\cup \left\{C\right\}=B\cup \left\{C,D\right\}$$
14	13	eqeq2i	$$⊢A=\left(B\cup \left\{D\right\}\right)\cup \left\{C\right\}\leftrightarrow A=B\cup \left\{C,D\right\}$$
15	14	orbi2i	$$⊢\left(A=B\cup \left\{D\right\}\vee A=\left(B\cup \left\{D\right\}\right)\cup \left\{C\right\}\right)\leftrightarrow \left(A=B\cup \left\{D\right\}\vee A=B\cup \left\{C,D\right\}\right)$$
16	11 12 15	3bitri	$$⊢\left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq \left(B\cup \left\{C\right\}\right)\cup \left\{D\right\}\right)\leftrightarrow \left(A=B\cup \left\{D\right\}\vee A=B\cup \left\{C,D\right\}\right)$$
17	8 16	orbi12i	$$⊢\left(\left(B\subseteq A\wedge A\subseteq B\cup \left\{C\right\}\right)\vee \left(B\cup \left\{D\right\}\subseteq A\wedge A\subseteq \left(B\cup \left\{C\right\}\right)\cup \left\{D\right\}\right)\right)\leftrightarrow \left(\left(A=B\vee A=B\cup \left\{C\right\}\right)\vee \left(A=B\cup \left\{D\right\}\vee A=B\cup \left\{C,D\right\}\right)\right)$$
18	6 7 17	3bitri	$$⊢\left(B\subseteq A\wedge A\subseteq B\cup \left\{C,D\right\}\right)\leftrightarrow \left(\left(A=B\vee A=B\cup \left\{C\right\}\right)\vee \left(A=B\cup \left\{D\right\}\vee A=B\cup \left\{C,D\right\}\right)\right)$$