Step |
Hyp |
Ref |
Expression |
1 |
|
relwdom |
|- Rel ~<_* |
2 |
1
|
brrelex2i |
|- ( X ~<_* Y -> Y e. _V ) |
3 |
|
0domg |
|- ( Y e. _V -> (/) ~<_ Y ) |
4 |
2 3
|
syl |
|- ( X ~<_* Y -> (/) ~<_ Y ) |
5 |
|
breq1 |
|- ( X = (/) -> ( X ~<_ Y <-> (/) ~<_ Y ) ) |
6 |
4 5
|
syl5ibr |
|- ( X = (/) -> ( X ~<_* Y -> X ~<_ Y ) ) |
7 |
6
|
adantl |
|- ( ( X e. Fin /\ X = (/) ) -> ( X ~<_* Y -> X ~<_ Y ) ) |
8 |
|
brwdomn0 |
|- ( X =/= (/) -> ( X ~<_* Y <-> E. x x : Y -onto-> X ) ) |
9 |
8
|
adantl |
|- ( ( X e. Fin /\ X =/= (/) ) -> ( X ~<_* Y <-> E. x x : Y -onto-> X ) ) |
10 |
|
vex |
|- x e. _V |
11 |
|
fof |
|- ( x : Y -onto-> X -> x : Y --> X ) |
12 |
|
dmfex |
|- ( ( x e. _V /\ x : Y --> X ) -> Y e. _V ) |
13 |
10 11 12
|
sylancr |
|- ( x : Y -onto-> X -> Y e. _V ) |
14 |
13
|
adantl |
|- ( ( X e. Fin /\ x : Y -onto-> X ) -> Y e. _V ) |
15 |
|
simpl |
|- ( ( X e. Fin /\ x : Y -onto-> X ) -> X e. Fin ) |
16 |
|
simpr |
|- ( ( X e. Fin /\ x : Y -onto-> X ) -> x : Y -onto-> X ) |
17 |
|
fodomfi2 |
|- ( ( Y e. _V /\ X e. Fin /\ x : Y -onto-> X ) -> X ~<_ Y ) |
18 |
14 15 16 17
|
syl3anc |
|- ( ( X e. Fin /\ x : Y -onto-> X ) -> X ~<_ Y ) |
19 |
18
|
ex |
|- ( X e. Fin -> ( x : Y -onto-> X -> X ~<_ Y ) ) |
20 |
19
|
adantr |
|- ( ( X e. Fin /\ X =/= (/) ) -> ( x : Y -onto-> X -> X ~<_ Y ) ) |
21 |
20
|
exlimdv |
|- ( ( X e. Fin /\ X =/= (/) ) -> ( E. x x : Y -onto-> X -> X ~<_ Y ) ) |
22 |
9 21
|
sylbid |
|- ( ( X e. Fin /\ X =/= (/) ) -> ( X ~<_* Y -> X ~<_ Y ) ) |
23 |
7 22
|
pm2.61dane |
|- ( X e. Fin -> ( X ~<_* Y -> X ~<_ Y ) ) |
24 |
|
domwdom |
|- ( X ~<_ Y -> X ~<_* Y ) |
25 |
23 24
|
impbid1 |
|- ( X e. Fin -> ( X ~<_* Y <-> X ~<_ Y ) ) |