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

Metamath Proof Explorer

Theorem eldifpw

Description: Membership in a power class difference. (Contributed by NM, 25-Mar-2007)

Ref Expression
Hypothesis eldifpw.1 ⊢ 𝐶 ∈ V
Assertion eldifpw ( ( 𝐴 ∈ 𝒫 𝐵 ∧ ¬ 𝐶 ⊆ 𝐵 ) → ( 𝐴 ∪ 𝐶 ) ∈ ( 𝒫 ( 𝐵 ∪ 𝐶 ) ∖ 𝒫 𝐵 ) )

Proof

Step Hyp Ref Expression
1 eldifpw.1 ⊢ 𝐶 ∈ V
2 elpwi ⊢ ( 𝐴 ∈ 𝒫 𝐵 → 𝐴 ⊆ 𝐵 )
3 unss1 ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∪ 𝐶 ) ⊆ ( 𝐵 ∪ 𝐶 ) )
4 unexg ⊢ ( ( 𝐴 ∈ 𝒫 𝐵 ∧ 𝐶 ∈ V ) → ( 𝐴 ∪ 𝐶 ) ∈ V )
5 1 4 mpan2 ⊢ ( 𝐴 ∈ 𝒫 𝐵 → ( 𝐴 ∪ 𝐶 ) ∈ V )
6 elpwg ⊢ ( ( 𝐴 ∪ 𝐶 ) ∈ V → ( ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 ( 𝐵 ∪ 𝐶 ) ↔ ( 𝐴 ∪ 𝐶 ) ⊆ ( 𝐵 ∪ 𝐶 ) ) )
7 5 6 syl ⊢ ( 𝐴 ∈ 𝒫 𝐵 → ( ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 ( 𝐵 ∪ 𝐶 ) ↔ ( 𝐴 ∪ 𝐶 ) ⊆ ( 𝐵 ∪ 𝐶 ) ) )
8 3 7 imbitrrid ⊢ ( 𝐴 ∈ 𝒫 𝐵 → ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 ( 𝐵 ∪ 𝐶 ) ) )
9 2 8 mpd ⊢ ( 𝐴 ∈ 𝒫 𝐵 → ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 ( 𝐵 ∪ 𝐶 ) )
10 elpwi ⊢ ( ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 𝐵 → ( 𝐴 ∪ 𝐶 ) ⊆ 𝐵 )
11 10 unssbd ⊢ ( ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 𝐵 → 𝐶 ⊆ 𝐵 )
12 11 con3i ⊢ ( ¬ 𝐶 ⊆ 𝐵 → ¬ ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 𝐵 )
13 9 12 anim12i ⊢ ( ( 𝐴 ∈ 𝒫 𝐵 ∧ ¬ 𝐶 ⊆ 𝐵 ) → ( ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 ( 𝐵 ∪ 𝐶 ) ∧ ¬ ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 𝐵 ) )
14 eldif ⊢ ( ( 𝐴 ∪ 𝐶 ) ∈ ( 𝒫 ( 𝐵 ∪ 𝐶 ) ∖ 𝒫 𝐵 ) ↔ ( ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 ( 𝐵 ∪ 𝐶 ) ∧ ¬ ( 𝐴 ∪ 𝐶 ) ∈ 𝒫 𝐵 ) )
15 13 14 sylibr ⊢ ( ( 𝐴 ∈ 𝒫 𝐵 ∧ ¬ 𝐶 ⊆ 𝐵 ) → ( 𝐴 ∪ 𝐶 ) ∈ ( 𝒫 ( 𝐵 ∪ 𝐶 ) ∖ 𝒫 𝐵 ) )