Theorem fin34

Description: Every III-finite set is IV-finite. (Contributed by Stefan O'Rear, 30-Oct-2014)

	Ref	Expression
Assertion	fin34	|- ( A e. Fin3 -> A e. Fin4 )

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		reldom	|- Rel ~<_
5	4	brrelex2i	|- ( _om ~<_ A -> A e. _V )
6		canth2g	|- ( A e. _V -> A ~< ~P A )
7	5 6	syl	|- ( _om ~<_ A -> A ~< ~P A )
8		domsdomtr	|- ( ( _om ~<_ A /\ A ~< ~P A ) -> _om ~< ~P A )
9	7 8	mpdan	|- ( _om ~<_ A -> _om ~< ~P A )
10		sdomdom	|- ( _om ~< ~P A -> _om ~<_ ~P A )
11	9 10	syl	|- ( _om ~<_ A -> _om ~<_ ~P A )
12	3 11	nsyl	|- ( ~P A e. Fin4 -> -. _om ~<_ A )
13	1 12	sylbi	|- ( A e. Fin3 -> -. _om ~<_ A )
14		isfin4-2	|- ( A e. Fin3 -> ( A e. Fin4 <-> -. _om ~<_ A ) )
15	13 14	mpbird	|- ( A e. Fin3 -> A e. Fin4 )