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 
|- ( A e. ( ~P ( B u. { C } ) \ ~P B ) -> C e. A )

Proof

Step Hyp Ref Expression
1 eldif 
 |-  ( A e. ( ~P ( B u. { C } ) \ ~P B ) <-> ( A e. ~P ( B u. { C } ) /\ -. A e. ~P B ) )
2 elpwg 
 |-  ( A e. ~P ( B u. { C } ) -> ( A e. ~P B <-> A C_ B ) )
3 dfss3 
 |-  ( A C_ B <-> A. x e. A x e. B )
4 2 3 bitrdi 
 |-  ( A e. ~P ( B u. { C } ) -> ( A e. ~P B <-> A. x e. A x e. B ) )
5 4 notbid 
 |-  ( A e. ~P ( B u. { C } ) -> ( -. A e. ~P B <-> -. A. x e. A x e. B ) )
6 5 biimpa 
 |-  ( ( A e. ~P ( B u. { C } ) /\ -. A e. ~P B ) -> -. A. x e. A x e. B )
7 rexnal 
 |-  ( E. x e. A -. x e. B <-> -. A. x e. A x e. B )
8 6 7 sylibr 
 |-  ( ( A e. ~P ( B u. { C } ) /\ -. A e. ~P B ) -> E. x e. A -. x e. B )
9 elpwi 
 |-  ( A e. ~P ( B u. { C } ) -> A C_ ( B u. { C } ) )
10 ssel 
 |-  ( A C_ ( B u. { C } ) -> ( x e. A -> x e. ( B u. { C } ) ) )
11 elun 
 |-  ( x e. ( B u. { C } ) <-> ( x e. B \/ x e. { C } ) )
12 elsni 
 |-  ( x e. { C } -> x = C )
13 12 orim2i 
 |-  ( ( x e. B \/ x e. { C } ) -> ( x e. B \/ x = C ) )
14 13 ord 
 |-  ( ( x e. B \/ x e. { C } ) -> ( -. x e. B -> x = C ) )
15 11 14 sylbi 
 |-  ( x e. ( B u. { C } ) -> ( -. x e. B -> x = C ) )
16 15 imim2i 
 |-  ( ( x e. A -> x e. ( B u. { C } ) ) -> ( x e. A -> ( -. x e. B -> x = C ) ) )
17 16 impd 
 |-  ( ( x e. A -> x e. ( B u. { C } ) ) -> ( ( x e. A /\ -. x e. B ) -> x = C ) )
18 9 10 17 3syl 
 |-  ( A e. ~P ( B u. { C } ) -> ( ( x e. A /\ -. x e. B ) -> x = C ) )
19 eleq1 
 |-  ( x = C -> ( x e. A <-> C e. A ) )
20 19 biimpd 
 |-  ( x = C -> ( x e. A -> C e. A ) )
21 18 20 syl6 
 |-  ( A e. ~P ( B u. { C } ) -> ( ( x e. A /\ -. x e. B ) -> ( x e. A -> C e. A ) ) )
22 21 expd 
 |-  ( A e. ~P ( B u. { C } ) -> ( x e. A -> ( -. x e. B -> ( x e. A -> C e. A ) ) ) )
23 22 com4r 
 |-  ( x e. A -> ( A e. ~P ( B u. { C } ) -> ( x e. A -> ( -. x e. B -> C e. A ) ) ) )
24 23 pm2.43b 
 |-  ( A e. ~P ( B u. { C } ) -> ( x e. A -> ( -. x e. B -> C e. A ) ) )
25 24 rexlimdv 
 |-  ( A e. ~P ( B u. { C } ) -> ( E. x e. A -. x e. B -> C e. A ) )
26 25 imp 
 |-  ( ( A e. ~P ( B u. { C } ) /\ E. x e. A -. x e. B ) -> C e. A )
27 8 26 syldan 
 |-  ( ( A e. ~P ( B u. { C } ) /\ -. A e. ~P B ) -> C e. A )
28 1 27 sylbi 
 |-  ( A e. ( ~P ( B u. { C } ) \ ~P B ) -> C e. A )