Metamath Proof Explorer


Theorem isfin32i

Description: One half of isfin3-2 . (Contributed by Mario Carneiro, 3-Jun-2015)

Ref Expression
Assertion isfin32i
|- ( A e. Fin3 -> -. _om ~<_* A )

Proof

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 )