Theorem sorpsscmpl

Description: The componentwise complement of a chain of sets is also a chain of sets. (Contributed by Stefan O'Rear, 2-Nov-2014)

	Ref	Expression
Assertion	sorpsscmpl	$$⊢[\subset ]\mathrm{Or}Y\to [\subset ]\mathrm{Or}\left\{u\in 𝒫A|A\setminus u\in Y\right\}$$

Proof

Step	Hyp	Ref	Expression
1		difeq2	$$⊢u=x\to A\setminus u=A\setminus x$$
2	1	eleq1d	$$⊢u=x\to \left(A\setminus u\in Y\leftrightarrow A\setminus x\in Y\right)$$
3	2	elrab	$$⊢x\in \left\{u\in 𝒫A|A\setminus u\in Y\right\}\leftrightarrow \left(x\in 𝒫A\wedge A\setminus x\in Y\right)$$
4		difeq2	$$⊢u=y\to A\setminus u=A\setminus y$$
5	4	eleq1d	$$⊢u=y\to \left(A\setminus u\in Y\leftrightarrow A\setminus y\in Y\right)$$
6	5	elrab	$$⊢y\in \left\{u\in 𝒫A|A\setminus u\in Y\right\}\leftrightarrow \left(y\in 𝒫A\wedge A\setminus y\in Y\right)$$
7		an4	$$⊢\left(\left(x\in 𝒫A\wedge A\setminus x\in Y\right)\wedge \left(y\in 𝒫A\wedge A\setminus y\in Y\right)\right)\leftrightarrow \left(\left(x\in 𝒫A\wedge y\in 𝒫A\right)\wedge \left(A\setminus x\in Y\wedge A\setminus y\in Y\right)\right)$$
8	7	biimpi	$$⊢\left(\left(x\in 𝒫A\wedge A\setminus x\in Y\right)\wedge \left(y\in 𝒫A\wedge A\setminus y\in Y\right)\right)\to \left(\left(x\in 𝒫A\wedge y\in 𝒫A\right)\wedge \left(A\setminus x\in Y\wedge A\setminus y\in Y\right)\right)$$
9	3 6 8	syl2anb	$$⊢\left(x\in \left\{u\in 𝒫A|A\setminus u\in Y\right\}\wedge y\in \left\{u\in 𝒫A|A\setminus u\in Y\right\}\right)\to \left(\left(x\in 𝒫A\wedge y\in 𝒫A\right)\wedge \left(A\setminus x\in Y\wedge A\setminus y\in Y\right)\right)$$
10		sorpssi	$$⊢\left([\subset ]\mathrm{Or}Y\wedge \left(A\setminus x\in Y\wedge A\setminus y\in Y\right)\right)\to \left(A\setminus x\subseteq A\setminus y\vee A\setminus y\subseteq A\setminus x\right)$$
11	10	expcom	$$⊢\left(A\setminus x\in Y\wedge A\setminus y\in Y\right)\to \left([\subset ]\mathrm{Or}Y\to \left(A\setminus x\subseteq A\setminus y\vee A\setminus y\subseteq A\setminus x\right)\right)$$
12		velpw	$$⊢x\in 𝒫A\leftrightarrow x\subseteq A$$
13		dfss4	$$⊢x\subseteq A\leftrightarrow A\setminus \left(A\setminus x\right)=x$$
14	12 13	bitri	$$⊢x\in 𝒫A\leftrightarrow A\setminus \left(A\setminus x\right)=x$$
15		velpw	$$⊢y\in 𝒫A\leftrightarrow y\subseteq A$$
16		dfss4	$$⊢y\subseteq A\leftrightarrow A\setminus \left(A\setminus y\right)=y$$
17	15 16	bitri	$$⊢y\in 𝒫A\leftrightarrow A\setminus \left(A\setminus y\right)=y$$
18		sscon	$$⊢A\setminus y\subseteq A\setminus x\to A\setminus \left(A\setminus x\right)\subseteq A\setminus \left(A\setminus y\right)$$
19		sseq12	$$⊢\left(A\setminus \left(A\setminus x\right)=x\wedge A\setminus \left(A\setminus y\right)=y\right)\to \left(A\setminus \left(A\setminus x\right)\subseteq A\setminus \left(A\setminus y\right)\leftrightarrow x\subseteq y\right)$$
20	18 19	syl5ib	$$⊢\left(A\setminus \left(A\setminus x\right)=x\wedge A\setminus \left(A\setminus y\right)=y\right)\to \left(A\setminus y\subseteq A\setminus x\to x\subseteq y\right)$$
21		sscon	$$⊢A\setminus x\subseteq A\setminus y\to A\setminus \left(A\setminus y\right)\subseteq A\setminus \left(A\setminus x\right)$$
22		sseq12	$$⊢\left(A\setminus \left(A\setminus y\right)=y\wedge A\setminus \left(A\setminus x\right)=x\right)\to \left(A\setminus \left(A\setminus y\right)\subseteq A\setminus \left(A\setminus x\right)\leftrightarrow y\subseteq x\right)$$
23	22	ancoms	$$⊢\left(A\setminus \left(A\setminus x\right)=x\wedge A\setminus \left(A\setminus y\right)=y\right)\to \left(A\setminus \left(A\setminus y\right)\subseteq A\setminus \left(A\setminus x\right)\leftrightarrow y\subseteq x\right)$$
24	21 23	syl5ib	$$⊢\left(A\setminus \left(A\setminus x\right)=x\wedge A\setminus \left(A\setminus y\right)=y\right)\to \left(A\setminus x\subseteq A\setminus y\to y\subseteq x\right)$$
25	20 24	orim12d	$$⊢\left(A\setminus \left(A\setminus x\right)=x\wedge A\setminus \left(A\setminus y\right)=y\right)\to \left(\left(A\setminus y\subseteq A\setminus x\vee A\setminus x\subseteq A\setminus y\right)\to \left(x\subseteq y\vee y\subseteq x\right)\right)$$
26	14 17 25	syl2anb	$$⊢\left(x\in 𝒫A\wedge y\in 𝒫A\right)\to \left(\left(A\setminus y\subseteq A\setminus x\vee A\setminus x\subseteq A\setminus y\right)\to \left(x\subseteq y\vee y\subseteq x\right)\right)$$
27	26	com12	$$⊢\left(A\setminus y\subseteq A\setminus x\vee A\setminus x\subseteq A\setminus y\right)\to \left(\left(x\in 𝒫A\wedge y\in 𝒫A\right)\to \left(x\subseteq y\vee y\subseteq x\right)\right)$$
28	27	orcoms	$$⊢\left(A\setminus x\subseteq A\setminus y\vee A\setminus y\subseteq A\setminus x\right)\to \left(\left(x\in 𝒫A\wedge y\in 𝒫A\right)\to \left(x\subseteq y\vee y\subseteq x\right)\right)$$
29	11 28	syl6	$$⊢\left(A\setminus x\in Y\wedge A\setminus y\in Y\right)\to \left([\subset ]\mathrm{Or}Y\to \left(\left(x\in 𝒫A\wedge y\in 𝒫A\right)\to \left(x\subseteq y\vee y\subseteq x\right)\right)\right)$$
30	29	com3l	$$⊢[\subset ]\mathrm{Or}Y\to \left(\left(x\in 𝒫A\wedge y\in 𝒫A\right)\to \left(\left(A\setminus x\in Y\wedge A\setminus y\in Y\right)\to \left(x\subseteq y\vee y\subseteq x\right)\right)\right)$$
31	30	impd	$$⊢[\subset ]\mathrm{Or}Y\to \left(\left(\left(x\in 𝒫A\wedge y\in 𝒫A\right)\wedge \left(A\setminus x\in Y\wedge A\setminus y\in Y\right)\right)\to \left(x\subseteq y\vee y\subseteq x\right)\right)$$
32	9 31	syl5	$$⊢[\subset ]\mathrm{Or}Y\to \left(\left(x\in \left\{u\in 𝒫A|A\setminus u\in Y\right\}\wedge y\in \left\{u\in 𝒫A|A\setminus u\in Y\right\}\right)\to \left(x\subseteq y\vee y\subseteq x\right)\right)$$
33	32	ralrimivv	$$⊢[\subset ]\mathrm{Or}Y\to \forall x\in \left\{u\in 𝒫A|A\setminus u\in Y\right\}\forall y\in \left\{u\in 𝒫A|A\setminus u\in Y\right\}\left(x\subseteq y\vee y\subseteq x\right)$$
34		sorpss	$$⊢[\subset ]\mathrm{Or}\left\{u\in 𝒫A|A\setminus u\in Y\right\}\leftrightarrow \forall x\in \left\{u\in 𝒫A|A\setminus u\in Y\right\}\forall y\in \left\{u\in 𝒫A|A\setminus u\in Y\right\}\left(x\subseteq y\vee y\subseteq x\right)$$
35	33 34	sylibr	$$⊢[\subset ]\mathrm{Or}Y\to [\subset ]\mathrm{Or}\left\{u\in 𝒫A|A\setminus u\in Y\right\}$$