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

Metamath Proof Explorer

Theorem elpwunsn

Description: Membership in an extension of a power class. (Contributed by NM, 26-Mar-2007)

Ref Expression
Assertion elpwunsn ( 𝐴 ∈ ( 𝒫 ( 𝐵 ∪ { 𝐶 } ) ∖ 𝒫 𝐵 ) → 𝐶 ∈ 𝐴 )

Proof

Step Hyp Ref Expression
1 eldif ⊢ ( 𝐴 ∈ ( 𝒫 ( 𝐵 ∪ { 𝐶 } ) ∖ 𝒫 𝐵 ) ↔ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) ∧ ¬ 𝐴 ∈ 𝒫 𝐵 ) )
2 elpwg ⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( 𝐴 ∈ 𝒫 𝐵 ↔ 𝐴 ⊆ 𝐵 ) )
3 dfss3 ⊢ ( 𝐴 ⊆ 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 )
4 2 3 bitrdi ⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( 𝐴 ∈ 𝒫 𝐵 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ) )
5 4 notbid ⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( ¬ 𝐴 ∈ 𝒫 𝐵 ↔ ¬ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 ) )
6 5 biimpa ⊢ ( ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) ∧ ¬ 𝐴 ∈ 𝒫 𝐵 ) → ¬ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 )
7 rexnal ⊢ ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ↔ ¬ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝐵 )
8 6 7 sylibr ⊢ ( ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) ∧ ¬ 𝐴 ∈ 𝒫 𝐵 ) → ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 )
9 elpwi ⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 } ) )
10 ssel ⊢ ( 𝐴 ⊆ ( 𝐵 ∪ { 𝐶 } ) → ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐵 ∪ { 𝐶 } ) ) )
11 elun ⊢ ( 𝑥 ∈ ( 𝐵 ∪ { 𝐶 } ) ↔ ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ { 𝐶 } ) )
12 elsni ⊢ ( 𝑥 ∈ { 𝐶 } → 𝑥 = 𝐶 )
13 12 orim2i ⊢ ( ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ { 𝐶 } ) → ( 𝑥 ∈ 𝐵 ∨ 𝑥 = 𝐶 ) )
14 13 ord ⊢ ( ( 𝑥 ∈ 𝐵 ∨ 𝑥 ∈ { 𝐶 } ) → ( ¬ 𝑥 ∈ 𝐵 → 𝑥 = 𝐶 ) )
15 11 14 sylbi ⊢ ( 𝑥 ∈ ( 𝐵 ∪ { 𝐶 } ) → ( ¬ 𝑥 ∈ 𝐵 → 𝑥 = 𝐶 ) )
16 15 imim2i ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐵 ∪ { 𝐶 } ) ) → ( 𝑥 ∈ 𝐴 → ( ¬ 𝑥 ∈ 𝐵 → 𝑥 = 𝐶 ) ) )
17 16 impd ⊢ ( ( 𝑥 ∈ 𝐴 → 𝑥 ∈ ( 𝐵 ∪ { 𝐶 } ) ) → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) → 𝑥 = 𝐶 ) )
18 9 10 17 3syl ⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) → 𝑥 = 𝐶 ) )
19 eleq1 ⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴 ) )
20 19 biimpd ⊢ ( 𝑥 = 𝐶 → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐴 ) )
21 18 20 syl6 ⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐴 ) ) )
22 21 expd ⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( 𝑥 ∈ 𝐴 → ( ¬ 𝑥 ∈ 𝐵 → ( 𝑥 ∈ 𝐴 → 𝐶 ∈ 𝐴 ) ) ) )
23 22 com4r ⊢ ( 𝑥 ∈ 𝐴 → ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( 𝑥 ∈ 𝐴 → ( ¬ 𝑥 ∈ 𝐵 → 𝐶 ∈ 𝐴 ) ) ) )
24 23 pm2.43b ⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( 𝑥 ∈ 𝐴 → ( ¬ 𝑥 ∈ 𝐵 → 𝐶 ∈ 𝐴 ) ) )
25 24 rexlimdv ⊢ ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) → ( ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 → 𝐶 ∈ 𝐴 ) )
26 25 imp ⊢ ( ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) ∧ ∃ 𝑥 ∈ 𝐴 ¬ 𝑥 ∈ 𝐵 ) → 𝐶 ∈ 𝐴 )
27 8 26 syldan ⊢ ( ( 𝐴 ∈ 𝒫 ( 𝐵 ∪ { 𝐶 } ) ∧ ¬ 𝐴 ∈ 𝒫 𝐵 ) → 𝐶 ∈ 𝐴 )
28 1 27 sylbi ⊢ ( 𝐴 ∈ ( 𝒫 ( 𝐵 ∪ { 𝐶 } ) ∖ 𝒫 𝐵 ) → 𝐶 ∈ 𝐴 )