Metamath Proof Explorer

Theorem domalom

Description: A class which dominates every natural number is not finite. (Contributed by ML, 14-Dec-2020)

Ref Expression
Assertion domalom 
|- ( A. n e. _om n ~<_ A -> -. A e. Fin )

Proof

Step Hyp Ref Expression
1 nfra1 
 |-  F/ n A. n e. _om n ~<_ A
2 breq1 
 |-  ( y = n -> ( y ~< A <-> n ~< A ) )
3 2 imbi2d 
 |-  ( y = n -> ( ( A. n e. _om n ~<_ A -> y ~< A ) <-> ( A. n e. _om n ~<_ A -> n ~< A ) ) )
4 breq1 
 |-  ( y = (/) -> ( y ~< A <-> (/) ~< A ) )
5 breq1 
 |-  ( y = z -> ( y ~< A <-> z ~< A ) )
6 breq1 
 |-  ( y = suc z -> ( y ~< A <-> suc z ~< A ) )
7 1n0 
 |-  1o =/= (/)
8 1onn 
 |-  1o e. _om
9 0sdomg 
 |-  ( 1o e. _om -> ( (/) ~< 1o <-> 1o =/= (/) ) )
10 8 9 ax-mp 
 |-  ( (/) ~< 1o <-> 1o =/= (/) )
11 7 10 mpbir 
 |-  (/) ~< 1o
12 breq1 
 |-  ( n = 1o -> ( n ~<_ A <-> 1o ~<_ A ) )
13 12 rspccv 
 |-  ( A. n e. _om n ~<_ A -> ( 1o e. _om -> 1o ~<_ A ) )
14 8 13 mpi 
 |-  ( A. n e. _om n ~<_ A -> 1o ~<_ A )
15 sdomdomtr 
 |-  ( ( (/) ~< 1o /\ 1o ~<_ A ) -> (/) ~< A )
16 11 14 15 sylancr 
 |-  ( A. n e. _om n ~<_ A -> (/) ~< A )
17 peano2 
 |-  ( z e. _om -> suc z e. _om )
18 php4 
 |-  ( suc z e. _om -> suc z ~< suc suc z )
19 17 18 syl 
 |-  ( z e. _om -> suc z ~< suc suc z )
20 breq1 
 |-  ( n = suc suc z -> ( n ~<_ A <-> suc suc z ~<_ A ) )
21 20 rspccv 
 |-  ( A. n e. _om n ~<_ A -> ( suc suc z e. _om -> suc suc z ~<_ A ) )
22 peano2 
 |-  ( suc z e. _om -> suc suc z e. _om )
23 17 22 syl 
 |-  ( z e. _om -> suc suc z e. _om )
24 21 23 impel 
 |-  ( ( A. n e. _om n ~<_ A /\ z e. _om ) -> suc suc z ~<_ A )
25 sdomdomtr 
 |-  ( ( suc z ~< suc suc z /\ suc suc z ~<_ A ) -> suc z ~< A )
26 19 24 25 syl2an2 
 |-  ( ( A. n e. _om n ~<_ A /\ z e. _om ) -> suc z ~< A )
27 26 a1d 
 |-  ( ( A. n e. _om n ~<_ A /\ z e. _om ) -> ( z ~< A -> suc z ~< A ) )
28 27 expcom 
 |-  ( z e. _om -> ( A. n e. _om n ~<_ A -> ( z ~< A -> suc z ~< A ) ) )
29 4 5 6 16 28 finds2 
 |-  ( y e. _om -> ( A. n e. _om n ~<_ A -> y ~< A ) )
30 3 29 vtoclga 
 |-  ( n e. _om -> ( A. n e. _om n ~<_ A -> n ~< A ) )
31 30 com12 
 |-  ( A. n e. _om n ~<_ A -> ( n e. _om -> n ~< A ) )
32 1 31 ralrimi 
 |-  ( A. n e. _om n ~<_ A -> A. n e. _om n ~< A )
33 sdomnen 
 |-  ( n ~< A -> -. n ~~ A )
34 ensym 
 |-  ( A ~~ n -> n ~~ A )
35 33 34 nsyl 
 |-  ( n ~< A -> -. A ~~ n )
36 35 ralimi 
 |-  ( A. n e. _om n ~< A -> A. n e. _om -. A ~~ n )
37 32 36 syl 
 |-  ( A. n e. _om n ~<_ A -> A. n e. _om -. A ~~ n )
38 isfi 
 |-  ( A e. Fin <-> E. n e. _om A ~~ n )
39 38 notbii 
 |-  ( -. A e. Fin <-> -. E. n e. _om A ~~ n )
40 ralnex 
 |-  ( A. n e. _om -. A ~~ n <-> -. E. n e. _om A ~~ n )
41 39 40 bitr4i 
 |-  ( -. A e. Fin <-> A. n e. _om -. A ~~ n )
42 37 41 sylibr 
 |-  ( A. n e. _om n ~<_ A -> -. A e. Fin )