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 ) |