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 )