This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )