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