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

Metamath Proof Explorer

Theorem fpwwe2lem1

Description: Lemma for fpwwe2 . (Contributed by Mario Carneiro, 15-May-2015)

Ref Expression
Hypothesis fpwwe2.1 
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }
Assertion fpwwe2lem1 
|- W C_ ( ~P A X. ~P ( A X. A ) )

Proof

Step Hyp Ref Expression
1 fpwwe2.1 
 |-  W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }
2 simpll 
 |-  ( ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) -> x C_ A )
3 velpw 
 |-  ( x e. ~P A <-> x C_ A )
4 2 3 sylibr 
 |-  ( ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) -> x e. ~P A )
5 simplr 
 |-  ( ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) -> r C_ ( x X. x ) )
6 xpss12 
 |-  ( ( x C_ A /\ x C_ A ) -> ( x X. x ) C_ ( A X. A ) )
7 2 2 6 syl2anc 
 |-  ( ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) -> ( x X. x ) C_ ( A X. A ) )
8 5 7 sstrd 
 |-  ( ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) -> r C_ ( A X. A ) )
9 velpw 
 |-  ( r e. ~P ( A X. A ) <-> r C_ ( A X. A ) )
10 8 9 sylibr 
 |-  ( ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) -> r e. ~P ( A X. A ) )
11 4 10 jca 
 |-  ( ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) -> ( x e. ~P A /\ r e. ~P ( A X. A ) ) )
12 11 ssopab2i 
 |-  { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) } C_ { <. x , r >. | ( x e. ~P A /\ r e. ~P ( A X. A ) ) }
13 df-xp 
 |-  ( ~P A X. ~P ( A X. A ) ) = { <. x , r >. | ( x e. ~P A /\ r e. ~P ( A X. A ) ) }
14 12 1 13 3sstr4i 
 |-  W C_ ( ~P A X. ~P ( A X. A ) )