Step |
Hyp |
Ref |
Expression |
1 |
|
1sdom2 |
|- 1o ~< 2o |
2 |
|
sdomdom |
|- ( 1o ~< 2o -> 1o ~<_ 2o ) |
3 |
1 2
|
ax-mp |
|- 1o ~<_ 2o |
4 |
|
relsdom |
|- Rel ~< |
5 |
4
|
brrelex2i |
|- ( 1o ~< A -> A e. _V ) |
6 |
|
djudom2 |
|- ( ( 1o ~<_ 2o /\ A e. _V ) -> ( A |_| 1o ) ~<_ ( A |_| 2o ) ) |
7 |
3 5 6
|
sylancr |
|- ( 1o ~< A -> ( A |_| 1o ) ~<_ ( A |_| 2o ) ) |
8 |
|
canthp1lem1 |
|- ( 1o ~< A -> ( A |_| 2o ) ~<_ ~P A ) |
9 |
|
domtr |
|- ( ( ( A |_| 1o ) ~<_ ( A |_| 2o ) /\ ( A |_| 2o ) ~<_ ~P A ) -> ( A |_| 1o ) ~<_ ~P A ) |
10 |
7 8 9
|
syl2anc |
|- ( 1o ~< A -> ( A |_| 1o ) ~<_ ~P A ) |
11 |
|
fal |
|- -. F. |
12 |
|
ensym |
|- ( ( A |_| 1o ) ~~ ~P A -> ~P A ~~ ( A |_| 1o ) ) |
13 |
|
bren |
|- ( ~P A ~~ ( A |_| 1o ) <-> E. f f : ~P A -1-1-onto-> ( A |_| 1o ) ) |
14 |
12 13
|
sylib |
|- ( ( A |_| 1o ) ~~ ~P A -> E. f f : ~P A -1-1-onto-> ( A |_| 1o ) ) |
15 |
|
f1of |
|- ( f : ~P A -1-1-onto-> ( A |_| 1o ) -> f : ~P A --> ( A |_| 1o ) ) |
16 |
|
pwidg |
|- ( A e. _V -> A e. ~P A ) |
17 |
5 16
|
syl |
|- ( 1o ~< A -> A e. ~P A ) |
18 |
|
ffvelrn |
|- ( ( f : ~P A --> ( A |_| 1o ) /\ A e. ~P A ) -> ( f ` A ) e. ( A |_| 1o ) ) |
19 |
15 17 18
|
syl2anr |
|- ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) -> ( f ` A ) e. ( A |_| 1o ) ) |
20 |
|
dju1dif |
|- ( ( A e. _V /\ ( f ` A ) e. ( A |_| 1o ) ) -> ( ( A |_| 1o ) \ { ( f ` A ) } ) ~~ A ) |
21 |
5 19 20
|
syl2an2r |
|- ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) -> ( ( A |_| 1o ) \ { ( f ` A ) } ) ~~ A ) |
22 |
|
bren |
|- ( ( ( A |_| 1o ) \ { ( f ` A ) } ) ~~ A <-> E. g g : ( ( A |_| 1o ) \ { ( f ` A ) } ) -1-1-onto-> A ) |
23 |
21 22
|
sylib |
|- ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) -> E. g g : ( ( A |_| 1o ) \ { ( f ` A ) } ) -1-1-onto-> A ) |
24 |
|
simpll |
|- ( ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) /\ g : ( ( A |_| 1o ) \ { ( f ` A ) } ) -1-1-onto-> A ) -> 1o ~< A ) |
25 |
|
simplr |
|- ( ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) /\ g : ( ( A |_| 1o ) \ { ( f ` A ) } ) -1-1-onto-> A ) -> f : ~P A -1-1-onto-> ( A |_| 1o ) ) |
26 |
|
simpr |
|- ( ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) /\ g : ( ( A |_| 1o ) \ { ( f ` A ) } ) -1-1-onto-> A ) -> g : ( ( A |_| 1o ) \ { ( f ` A ) } ) -1-1-onto-> A ) |
27 |
|
eqeq1 |
|- ( w = x -> ( w = A <-> x = A ) ) |
28 |
|
id |
|- ( w = x -> w = x ) |
29 |
27 28
|
ifbieq2d |
|- ( w = x -> if ( w = A , (/) , w ) = if ( x = A , (/) , x ) ) |
30 |
29
|
cbvmptv |
|- ( w e. ~P A |-> if ( w = A , (/) , w ) ) = ( x e. ~P A |-> if ( x = A , (/) , x ) ) |
31 |
30
|
coeq2i |
|- ( ( g o. f ) o. ( w e. ~P A |-> if ( w = A , (/) , w ) ) ) = ( ( g o. f ) o. ( x e. ~P A |-> if ( x = A , (/) , x ) ) ) |
32 |
|
eqid |
|- { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a ( ( ( g o. f ) o. ( w e. ~P A |-> if ( w = A , (/) , w ) ) ) ` ( `' s " { z } ) ) = z ) ) } = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a ( ( ( g o. f ) o. ( w e. ~P A |-> if ( w = A , (/) , w ) ) ) ` ( `' s " { z } ) ) = z ) ) } |
33 |
32
|
fpwwecbv |
|- { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a ( ( ( g o. f ) o. ( w e. ~P A |-> if ( w = A , (/) , w ) ) ) ` ( `' s " { z } ) ) = z ) ) } = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( ( ( g o. f ) o. ( w e. ~P A |-> if ( w = A , (/) , w ) ) ) ` ( `' r " { y } ) ) = y ) ) } |
34 |
|
eqid |
|- U. dom { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a ( ( ( g o. f ) o. ( w e. ~P A |-> if ( w = A , (/) , w ) ) ) ` ( `' s " { z } ) ) = z ) ) } = U. dom { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a ( ( ( g o. f ) o. ( w e. ~P A |-> if ( w = A , (/) , w ) ) ) ` ( `' s " { z } ) ) = z ) ) } |
35 |
24 25 26 31 33 34
|
canthp1lem2 |
|- -. ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) /\ g : ( ( A |_| 1o ) \ { ( f ` A ) } ) -1-1-onto-> A ) |
36 |
35
|
pm2.21i |
|- ( ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) /\ g : ( ( A |_| 1o ) \ { ( f ` A ) } ) -1-1-onto-> A ) -> F. ) |
37 |
23 36
|
exlimddv |
|- ( ( 1o ~< A /\ f : ~P A -1-1-onto-> ( A |_| 1o ) ) -> F. ) |
38 |
37
|
ex |
|- ( 1o ~< A -> ( f : ~P A -1-1-onto-> ( A |_| 1o ) -> F. ) ) |
39 |
38
|
exlimdv |
|- ( 1o ~< A -> ( E. f f : ~P A -1-1-onto-> ( A |_| 1o ) -> F. ) ) |
40 |
14 39
|
syl5 |
|- ( 1o ~< A -> ( ( A |_| 1o ) ~~ ~P A -> F. ) ) |
41 |
11 40
|
mtoi |
|- ( 1o ~< A -> -. ( A |_| 1o ) ~~ ~P A ) |
42 |
|
brsdom |
|- ( ( A |_| 1o ) ~< ~P A <-> ( ( A |_| 1o ) ~<_ ~P A /\ -. ( A |_| 1o ) ~~ ~P A ) ) |
43 |
10 41 42
|
sylanbrc |
|- ( 1o ~< A -> ( A |_| 1o ) ~< ~P A ) |