Step |
Hyp |
Ref |
Expression |
1 |
|
isfin3 |
|- ( A e. Fin3 <-> ~P A e. Fin4 ) |
2 |
|
isfin4-2 |
|- ( ~P A e. Fin4 -> ( ~P A e. Fin4 <-> -. _om ~<_ ~P A ) ) |
3 |
2
|
ibi |
|- ( ~P A e. Fin4 -> -. _om ~<_ ~P A ) |
4 |
|
relwdom |
|- Rel ~<_* |
5 |
4
|
brrelex1i |
|- ( _om ~<_* A -> _om e. _V ) |
6 |
|
canth2g |
|- ( _om e. _V -> _om ~< ~P _om ) |
7 |
|
sdomdom |
|- ( _om ~< ~P _om -> _om ~<_ ~P _om ) |
8 |
5 6 7
|
3syl |
|- ( _om ~<_* A -> _om ~<_ ~P _om ) |
9 |
|
wdompwdom |
|- ( _om ~<_* A -> ~P _om ~<_ ~P A ) |
10 |
|
domtr |
|- ( ( _om ~<_ ~P _om /\ ~P _om ~<_ ~P A ) -> _om ~<_ ~P A ) |
11 |
8 9 10
|
syl2anc |
|- ( _om ~<_* A -> _om ~<_ ~P A ) |
12 |
3 11
|
nsyl |
|- ( ~P A e. Fin4 -> -. _om ~<_* A ) |
13 |
1 12
|
sylbi |
|- ( A e. Fin3 -> -. _om ~<_* A ) |