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

Metamath Proof Explorer

Theorem wepwso

Description: A well-ordering induces a strict ordering on the power set.EDITORIAL: when well-orderings are set like, this can be strengthened to remove A e. V . (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Hypothesis wepwso.t 
|- T = { <. x , y >. | E. z e. A ( ( z e. y /\ -. z e. x ) /\ A. w e. A ( w R z -> ( w e. x <-> w e. y ) ) ) }
Assertion wepwso 
|- ( ( A e. V /\ R We A ) -> T Or ~P A )

Proof

Step Hyp Ref Expression
1 wepwso.t 
 |-  T = { <. x , y >. | E. z e. A ( ( z e. y /\ -. z e. x ) /\ A. w e. A ( w R z -> ( w e. x <-> w e. y ) ) ) }
2 2onn 
 |-  2o e. _om
3 nnord 
 |-  ( 2o e. _om -> Ord 2o )
4 2 3 ax-mp 
 |-  Ord 2o
5 ordwe 
 |-  ( Ord 2o -> _E We 2o )
6 weso 
 |-  ( _E We 2o -> _E Or 2o )
7 4 5 6 mp2b 
 |-  _E Or 2o
8 eqid 
 |-  { <. x , y >. | E. z e. A ( ( x ` z ) _E ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) } = { <. x , y >. | E. z e. A ( ( x ` z ) _E ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) }
9 8 wemapso 
 |-  ( ( R We A /\ _E Or 2o ) -> { <. x , y >. | E. z e. A ( ( x ` z ) _E ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) } Or ( 2o ^m A ) )
10 7 9 mpan2 
 |-  ( R We A -> { <. x , y >. | E. z e. A ( ( x ` z ) _E ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) } Or ( 2o ^m A ) )
11 10 adantl 
 |-  ( ( A e. V /\ R We A ) -> { <. x , y >. | E. z e. A ( ( x ` z ) _E ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) } Or ( 2o ^m A ) )
12 elex 
 |-  ( A e. V -> A e. _V )
13 eqid 
 |-  ( a e. ( 2o ^m A ) |-> ( `' a " { 1o } ) ) = ( a e. ( 2o ^m A ) |-> ( `' a " { 1o } ) )
14 1 8 13 wepwsolem 
 |-  ( A e. _V -> ( a e. ( 2o ^m A ) |-> ( `' a " { 1o } ) ) Isom { <. x , y >. | E. z e. A ( ( x ` z ) _E ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) } , T ( ( 2o ^m A ) , ~P A ) )
15 isoso 
 |-  ( ( a e. ( 2o ^m A ) |-> ( `' a " { 1o } ) ) Isom { <. x , y >. | E. z e. A ( ( x ` z ) _E ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) } , T ( ( 2o ^m A ) , ~P A ) -> ( { <. x , y >. | E. z e. A ( ( x ` z ) _E ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) } Or ( 2o ^m A ) <-> T Or ~P A ) )
16 12 14 15 3syl 
 |-  ( A e. V -> ( { <. x , y >. | E. z e. A ( ( x ` z ) _E ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) } Or ( 2o ^m A ) <-> T Or ~P A ) )
17 16 adantr 
 |-  ( ( A e. V /\ R We A ) -> ( { <. x , y >. | E. z e. A ( ( x ` z ) _E ( y ` z ) /\ A. w e. A ( w R z -> ( x ` w ) = ( y ` w ) ) ) } Or ( 2o ^m A ) <-> T Or ~P A ) )
18 11 17 mpbid 
 |-  ( ( A e. V /\ R We A ) -> T Or ~P A )