Theorem compsscnvlem

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

	Ref	Expression
Assertion	compsscnvlem	|- ( ( x e. ~P A /\ y = ( A \ x ) ) -> ( y e. ~P A /\ x = ( A \ y ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( x e. ~P A /\ y = ( A \ x ) ) -> y = ( A \ x ) )
2		difss	|- ( A \ x ) C_ A
3	1 2	eqsstrdi	|- ( ( x e. ~P A /\ y = ( A \ x ) ) -> y C_ A )
4		velpw	|- ( y e. ~P A <-> y C_ A )
5	3 4	sylibr	|- ( ( x e. ~P A /\ y = ( A \ x ) ) -> y e. ~P A )
6	1	difeq2d	|- ( ( x e. ~P A /\ y = ( A \ x ) ) -> ( A \ y ) = ( A \ ( A \ x ) ) )
7		elpwi	|- ( x e. ~P A -> x C_ A )
8	7	adantr	|- ( ( x e. ~P A /\ y = ( A \ x ) ) -> x C_ A )
9		dfss4	|- ( x C_ A <-> ( A \ ( A \ x ) ) = x )
10	8 9	sylib	|- ( ( x e. ~P A /\ y = ( A \ x ) ) -> ( A \ ( A \ x ) ) = x )
11	6 10	eqtr2d	|- ( ( x e. ~P A /\ y = ( A \ x ) ) -> x = ( A \ y ) )
12	5 11	jca	|- ( ( x e. ~P A /\ y = ( A \ x ) ) -> ( y e. ~P A /\ x = ( A \ y ) ) )