This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ 𝑦 = ( 𝐴 ∖ 𝑥 ) ) → ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑥 = ( 𝐴 ∖ 𝑦 ) ) )