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 ( 𝐴 ∈ ( 𝒫 ( 𝐵 ∪ { 𝐶 } ) ∖ 𝒫 𝐵 ) → 𝐶𝐴 )