Theorem compsscnvlem

Description: Lemma for compsscnv . (Contributed by Mario Carneiro, 17-May-2015)

	Ref	Expression
Assertion	compsscnvlem	$$⊢\left(x\in 𝒫A\wedge y=A\setminus x\right)\to \left(y\in 𝒫A\wedge x=A\setminus y\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(x\in 𝒫A\wedge y=A\setminus x\right)\to y=A\setminus x$$
2		difss	$$⊢A\setminus x\subseteq A$$
3	1 2	eqsstrdi	$$⊢\left(x\in 𝒫A\wedge y=A\setminus x\right)\to y\subseteq A$$
4		velpw	$$⊢y\in 𝒫A\leftrightarrow y\subseteq A$$
5	3 4	sylibr	$$⊢\left(x\in 𝒫A\wedge y=A\setminus x\right)\to y\in 𝒫A$$
6	1	difeq2d	$$⊢\left(x\in 𝒫A\wedge y=A\setminus x\right)\to A\setminus y=A\setminus \left(A\setminus x\right)$$
7		elpwi	$$⊢x\in 𝒫A\to x\subseteq A$$
8	7	adantr	$$⊢\left(x\in 𝒫A\wedge y=A\setminus x\right)\to x\subseteq A$$
9		dfss4	$$⊢x\subseteq A\leftrightarrow A\setminus \left(A\setminus x\right)=x$$
10	8 9	sylib	$$⊢\left(x\in 𝒫A\wedge y=A\setminus x\right)\to A\setminus \left(A\setminus x\right)=x$$
11	6 10	eqtr2d	$$⊢\left(x\in 𝒫A\wedge y=A\setminus x\right)\to x=A\setminus y$$
12	5 11	jca	$$⊢\left(x\in 𝒫A\wedge y=A\setminus x\right)\to \left(y\in 𝒫A\wedge x=A\setminus y\right)$$