Theorem compsscnvlem

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

	Ref	Expression
Assertion	compsscnvlem	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = ( 𝐴 ∖ 𝑥 ) ) → ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = ( 𝐴 ∖ 𝑦 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpr	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = ( 𝐴 ∖ 𝑥 ) ) → 𝑦 = ( 𝐴 ∖ 𝑥 ) )
2		difss	⊢ ( 𝐴 ∖ 𝑥 ) ⊆ 𝐴
3	1 2	eqsstrdi	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = ( 𝐴 ∖ 𝑥 ) ) → 𝑦 ⊆ 𝐴 )
4		velpw	⊢ ( 𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴 )
5	3 4	sylibr	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = ( 𝐴 ∖ 𝑥 ) ) → 𝑦 ∈ 𝒫 𝐴 )
6	1	difeq2d	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = ( 𝐴 ∖ 𝑥 ) ) → ( 𝐴 ∖ 𝑦 ) = ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) )
7		elpwi	⊢ ( 𝑥 ∈ 𝒫 𝐴 → 𝑥 ⊆ 𝐴 )
8	7	adantr	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = ( 𝐴 ∖ 𝑥 ) ) → 𝑥 ⊆ 𝐴 )
9		dfss4	⊢ ( 𝑥 ⊆ 𝐴 ↔ ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) = 𝑥 )
10	8 9	sylib	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = ( 𝐴 ∖ 𝑥 ) ) → ( 𝐴 ∖ ( 𝐴 ∖ 𝑥 ) ) = 𝑥 )
11	6 10	eqtr2d	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = ( 𝐴 ∖ 𝑥 ) ) → 𝑥 = ( 𝐴 ∖ 𝑦 ) )
12	5 11	jca	⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = ( 𝐴 ∖ 𝑥 ) ) → ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = ( 𝐴 ∖ 𝑦 ) ) )