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

Metamath Proof Explorer

Theorem sspwimp

Description: If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of TakeutiZaring p. 18. For the biconditional, see sspwb . The proof sspwimp , using conventional notation, was translated from virtual deduction form, sspwimpVD , using a translation program. (Contributed by Alan Sare, 23-Apr-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sspwimp 
|- ( A C_ B -> ~P A C_ ~P B )

Proof

Step Hyp Ref Expression
1 vex 
 |-  x e. _V
2 1 a1i 
 |-  ( T. -> x e. _V )
3 id 
 |-  ( A C_ B -> A C_ B )
4 id 
 |-  ( x e. ~P A -> x e. ~P A )
5 elpwi 
 |-  ( x e. ~P A -> x C_ A )
6 4 5 syl 
 |-  ( x e. ~P A -> x C_ A )
7 sstr 
 |-  ( ( x C_ A /\ A C_ B ) -> x C_ B )
8 7 ancoms 
 |-  ( ( A C_ B /\ x C_ A ) -> x C_ B )
9 3 6 8 syl2an 
 |-  ( ( A C_ B /\ x e. ~P A ) -> x C_ B )
10 2 9 elpwgded 
 |-  ( ( T. /\ ( A C_ B /\ x e. ~P A ) ) -> x e. ~P B )
11 2 9 10 uun0.1 
 |-  ( ( A C_ B /\ x e. ~P A ) -> x e. ~P B )
12 11 ex 
 |-  ( A C_ B -> ( x e. ~P A -> x e. ~P B ) )
13 12 alrimiv 
 |-  ( A C_ B -> A. x ( x e. ~P A -> x e. ~P B ) )
14 df-ss 
 |-  ( ~P A C_ ~P B <-> A. x ( x e. ~P A -> x e. ~P B ) )
15 14 biimpri 
 |-  ( A. x ( x e. ~P A -> x e. ~P B ) -> ~P A C_ ~P B )
16 13 15 syl 
 |-  ( A C_ B -> ~P A C_ ~P B )
17 16 iin1 
 |-  ( A C_ B -> ~P A C_ ~P B )