Theorem compssiso

Description: Complementation is an antiautomorphism on power set lattices. (Contributed by Stefan O'Rear, 4-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

	Ref	Expression
Hypothesis	compss.a	$$⊢F=\left(x\in 𝒫A⟼A\setminus x\right)$$
Assertion	compssiso	$$⊢A\in V\to F{Isom}_{[\subset ],{[\subset ]}^{-1}}\left(𝒫A,𝒫A\right)$$

Proof

Step	Hyp	Ref	Expression
1		compss.a	$$⊢F=\left(x\in 𝒫A⟼A\setminus x\right)$$
2		difexg	$$⊢A\in V\to A\setminus x\in \mathrm{V}$$
3	2	ralrimivw	$$⊢A\in V\to \forall x\in 𝒫AA\setminus x\in \mathrm{V}$$
4	1	fnmpt	$$⊢\forall x\in 𝒫AA\setminus x\in \mathrm{V}\to FFn𝒫A$$
5	3 4	syl	$$⊢A\in V\to FFn𝒫A$$
6	1	compsscnv	$$⊢F^{-1}=F$$
7	6	fneq1i	$$⊢F^{-1}Fn𝒫A\leftrightarrow FFn𝒫A$$
8	5 7	sylibr	$$⊢A\in V\to F^{-1}Fn𝒫A$$
9		dff1o4	$$⊢F:𝒫A\underset{1-1\; onto}{⟶}𝒫A\leftrightarrow \left(FFn𝒫A\wedge F^{-1}Fn𝒫A\right)$$
10	5 8 9	sylanbrc	$$⊢A\in V\to F:𝒫A\underset{1-1\; onto}{⟶}𝒫A$$
11		elpwi	$$⊢b\in 𝒫A\to b\subseteq A$$
12	11	ad2antll	$$⊢\left(A\in V\wedge \left(a\in 𝒫A\wedge b\in 𝒫A\right)\right)\to b\subseteq A$$
13	1	isf34lem1	$$⊢\left(A\in V\wedge b\subseteq A\right)\to F\left(b\right)=A\setminus b$$
14	12 13	syldan	$$⊢\left(A\in V\wedge \left(a\in 𝒫A\wedge b\in 𝒫A\right)\right)\to F\left(b\right)=A\setminus b$$
15		elpwi	$$⊢a\in 𝒫A\to a\subseteq A$$
16	15	ad2antrl	$$⊢\left(A\in V\wedge \left(a\in 𝒫A\wedge b\in 𝒫A\right)\right)\to a\subseteq A$$
17	1	isf34lem1	$$⊢\left(A\in V\wedge a\subseteq A\right)\to F\left(a\right)=A\setminus a$$
18	16 17	syldan	$$⊢\left(A\in V\wedge \left(a\in 𝒫A\wedge b\in 𝒫A\right)\right)\to F\left(a\right)=A\setminus a$$
19	14 18	psseq12d	$$⊢\left(A\in V\wedge \left(a\in 𝒫A\wedge b\in 𝒫A\right)\right)\to \left(F\left(b\right)\subset F\left(a\right)\leftrightarrow A\setminus b\subset A\setminus a\right)$$
20		difss	$$⊢A\setminus a\subseteq A$$
21		pssdifcom1	$$⊢\left(b\subseteq A\wedge A\setminus a\subseteq A\right)\to \left(A\setminus b\subset A\setminus a\leftrightarrow A\setminus \left(A\setminus a\right)\subset b\right)$$
22	12 20 21	sylancl	$$⊢\left(A\in V\wedge \left(a\in 𝒫A\wedge b\in 𝒫A\right)\right)\to \left(A\setminus b\subset A\setminus a\leftrightarrow A\setminus \left(A\setminus a\right)\subset b\right)$$
23		dfss4	$$⊢a\subseteq A\leftrightarrow A\setminus \left(A\setminus a\right)=a$$
24	16 23	sylib	$$⊢\left(A\in V\wedge \left(a\in 𝒫A\wedge b\in 𝒫A\right)\right)\to A\setminus \left(A\setminus a\right)=a$$
25	24	psseq1d	$$⊢\left(A\in V\wedge \left(a\in 𝒫A\wedge b\in 𝒫A\right)\right)\to \left(A\setminus \left(A\setminus a\right)\subset b\leftrightarrow a\subset b\right)$$
26	19 22 25	3bitrrd	$$⊢\left(A\in V\wedge \left(a\in 𝒫A\wedge b\in 𝒫A\right)\right)\to \left(a\subset b\leftrightarrow F\left(b\right)\subset F\left(a\right)\right)$$
27		vex	$$⊢b\in \mathrm{V}$$
28	27	brrpss	$$⊢a[\subset ]b\leftrightarrow a\subset b$$
29		fvex	$$⊢F\left(a\right)\in \mathrm{V}$$
30	29	brrpss	$$⊢F\left(b\right)[\subset ]F\left(a\right)\leftrightarrow F\left(b\right)\subset F\left(a\right)$$
31	26 28 30	3bitr4g	$$⊢\left(A\in V\wedge \left(a\in 𝒫A\wedge b\in 𝒫A\right)\right)\to \left(a[\subset ]b\leftrightarrow F\left(b\right)[\subset ]F\left(a\right)\right)$$
32		relrpss	$$⊢\mathrm{Rel}[\subset ]$$
33	32	relbrcnv	$$⊢F\left(a\right){[\subset ]}^{-1}F\left(b\right)\leftrightarrow F\left(b\right)[\subset ]F\left(a\right)$$
34	31 33	bitr4di	$$⊢\left(A\in V\wedge \left(a\in 𝒫A\wedge b\in 𝒫A\right)\right)\to \left(a[\subset ]b\leftrightarrow F\left(a\right){[\subset ]}^{-1}F\left(b\right)\right)$$
35	34	ralrimivva	$$⊢A\in V\to \forall a\in 𝒫A\forall b\in 𝒫A\left(a[\subset ]b\leftrightarrow F\left(a\right){[\subset ]}^{-1}F\left(b\right)\right)$$
36		df-isom	$$⊢F{Isom}_{[\subset ],{[\subset ]}^{-1}}\left(𝒫A,𝒫A\right)\leftrightarrow \left(F:𝒫A\underset{1-1\; onto}{⟶}𝒫A\wedge \forall a\in 𝒫A\forall b\in 𝒫A\left(a[\subset ]b\leftrightarrow F\left(a\right){[\subset ]}^{-1}F\left(b\right)\right)\right)$$
37	10 35 36	sylanbrc	$$⊢A\in V\to F{Isom}_{[\subset ],{[\subset ]}^{-1}}\left(𝒫A,𝒫A\right)$$