Metamath Proof Explorer

Theorem isfinite2

Description: Any set strictly dominated by the class of natural numbers is finite. Sufficiency part of Theorem 42 of Suppes p. 151. This theorem does not require the Axiom of Infinity. (Contributed by NM, 24-Apr-2004)

Ref Expression
Assertion isfinite2 
|- ( A ~< _om -> A e. Fin )

Proof

Step Hyp Ref Expression
1 relsdom 
 |-  Rel ~<
2 1 brrelex2i 
 |-  ( A ~< _om -> _om e. _V )
3 sdomdom 
 |-  ( A ~< _om -> A ~<_ _om )
4 domeng 
 |-  ( _om e. _V -> ( A ~<_ _om <-> E. y ( A ~~ y /\ y C_ _om ) ) )
5 3 4 syl5ib 
 |-  ( _om e. _V -> ( A ~< _om -> E. y ( A ~~ y /\ y C_ _om ) ) )
6 ensym 
 |-  ( A ~~ y -> y ~~ A )
7 6 ad2antrl 
 |-  ( ( A ~< _om /\ ( A ~~ y /\ y C_ _om ) ) -> y ~~ A )
8 simpl 
 |-  ( ( A ~< _om /\ ( A ~~ y /\ y C_ _om ) ) -> A ~< _om )
9 ensdomtr 
 |-  ( ( y ~~ A /\ A ~< _om ) -> y ~< _om )
10 7 8 9 syl2anc 
 |-  ( ( A ~< _om /\ ( A ~~ y /\ y C_ _om ) ) -> y ~< _om )
11 sdomnen 
 |-  ( y ~< _om -> -. y ~~ _om )
12 10 11 syl 
 |-  ( ( A ~< _om /\ ( A ~~ y /\ y C_ _om ) ) -> -. y ~~ _om )
13 simpr 
 |-  ( ( A ~~ y /\ y C_ _om ) -> y C_ _om )
14 unbnn 
 |-  ( ( _om e. _V /\ y C_ _om /\ A. z e. _om E. w e. y z e. w ) -> y ~~ _om )
15 14 3expia 
 |-  ( ( _om e. _V /\ y C_ _om ) -> ( A. z e. _om E. w e. y z e. w -> y ~~ _om ) )
16 2 13 15 syl2an 
 |-  ( ( A ~< _om /\ ( A ~~ y /\ y C_ _om ) ) -> ( A. z e. _om E. w e. y z e. w -> y ~~ _om ) )
17 12 16 mtod 
 |-  ( ( A ~< _om /\ ( A ~~ y /\ y C_ _om ) ) -> -. A. z e. _om E. w e. y z e. w )
18 rexnal 
 |-  ( E. z e. _om -. E. w e. y z e. w <-> -. A. z e. _om E. w e. y z e. w )
19 omsson 
 |-  _om C_ On
20 sstr 
 |-  ( ( y C_ _om /\ _om C_ On ) -> y C_ On )
21 19 20 mpan2 
 |-  ( y C_ _om -> y C_ On )
22 nnord 
 |-  ( z e. _om -> Ord z )
23 ssel2 
 |-  ( ( y C_ On /\ w e. y ) -> w e. On )
24 vex 
 |-  w e. _V
25 24 elon 
 |-  ( w e. On <-> Ord w )
26 23 25 sylib 
 |-  ( ( y C_ On /\ w e. y ) -> Ord w )
27 ordtri1 
 |-  ( ( Ord w /\ Ord z ) -> ( w C_ z <-> -. z e. w ) )
28 26 27 sylan 
 |-  ( ( ( y C_ On /\ w e. y ) /\ Ord z ) -> ( w C_ z <-> -. z e. w ) )
29 28 an32s 
 |-  ( ( ( y C_ On /\ Ord z ) /\ w e. y ) -> ( w C_ z <-> -. z e. w ) )
30 29 ralbidva 
 |-  ( ( y C_ On /\ Ord z ) -> ( A. w e. y w C_ z <-> A. w e. y -. z e. w ) )
31 unissb 
 |-  ( U. y C_ z <-> A. w e. y w C_ z )
32 ralnex 
 |-  ( A. w e. y -. z e. w <-> -. E. w e. y z e. w )
33 32 bicomi 
 |-  ( -. E. w e. y z e. w <-> A. w e. y -. z e. w )
34 30 31 33 3bitr4g 
 |-  ( ( y C_ On /\ Ord z ) -> ( U. y C_ z <-> -. E. w e. y z e. w ) )
35 ordunisssuc 
 |-  ( ( y C_ On /\ Ord z ) -> ( U. y C_ z <-> y C_ suc z ) )
36 34 35 bitr3d 
 |-  ( ( y C_ On /\ Ord z ) -> ( -. E. w e. y z e. w <-> y C_ suc z ) )
37 21 22 36 syl2an 
 |-  ( ( y C_ _om /\ z e. _om ) -> ( -. E. w e. y z e. w <-> y C_ suc z ) )
38 peano2b 
 |-  ( z e. _om <-> suc z e. _om )
39 ssnnfi 
 |-  ( ( suc z e. _om /\ y C_ suc z ) -> y e. Fin )
40 38 39 sylanb 
 |-  ( ( z e. _om /\ y C_ suc z ) -> y e. Fin )
41 40 ex 
 |-  ( z e. _om -> ( y C_ suc z -> y e. Fin ) )
42 41 adantl 
 |-  ( ( y C_ _om /\ z e. _om ) -> ( y C_ suc z -> y e. Fin ) )
43 37 42 sylbid 
 |-  ( ( y C_ _om /\ z e. _om ) -> ( -. E. w e. y z e. w -> y e. Fin ) )
44 43 rexlimdva 
 |-  ( y C_ _om -> ( E. z e. _om -. E. w e. y z e. w -> y e. Fin ) )
45 18 44 syl5bir 
 |-  ( y C_ _om -> ( -. A. z e. _om E. w e. y z e. w -> y e. Fin ) )
46 45 ad2antll 
 |-  ( ( A ~< _om /\ ( A ~~ y /\ y C_ _om ) ) -> ( -. A. z e. _om E. w e. y z e. w -> y e. Fin ) )
47 17 46 mpd 
 |-  ( ( A ~< _om /\ ( A ~~ y /\ y C_ _om ) ) -> y e. Fin )
48 simprl 
 |-  ( ( A ~< _om /\ ( A ~~ y /\ y C_ _om ) ) -> A ~~ y )
49 enfii 
 |-  ( ( y e. Fin /\ A ~~ y ) -> A e. Fin )
50 47 48 49 syl2anc 
 |-  ( ( A ~< _om /\ ( A ~~ y /\ y C_ _om ) ) -> A e. Fin )
51 50 ex 
 |-  ( A ~< _om -> ( ( A ~~ y /\ y C_ _om ) -> A e. Fin ) )
52 51 exlimdv 
 |-  ( A ~< _om -> ( E. y ( A ~~ y /\ y C_ _om ) -> A e. Fin ) )
53 5 52 sylcom 
 |-  ( _om e. _V -> ( A ~< _om -> A e. Fin ) )
54 2 53 mpcom 
 |-  ( A ~< _om -> A e. Fin )