Metamath Proof Explorer

Theorem cantnfub

Description: Given a finite number of terms of the form ( (om ^o ( An ) ) .o ( Mn ) ) with distinct exponents, we may order them from largest to smallest and find the sum is less than ( om ^o X ) when ( An ) is less than X and ( Mn ) is less than _om . Lemma 5.2 of Schloeder p. 15. (Contributed by RP, 31-Jan-2025)

Ref Expression
Hypotheses cantnfub.0 
|- ( ph -> X e. On )
cantnfub.n 
|- ( ph -> N e. _om )
cantnfub.a 
|- ( ph -> A : N -1-1-> X )
cantnfub.m 
|- ( ph -> M : N --> _om )
cantnfub.f 
|- F = ( x e. X |-> if ( x e. ran A , ( M ` ( `' A ` x ) ) , (/) ) )
Assertion cantnfub 
|- ( ph -> ( F e. dom ( _om CNF X ) /\ ( ( _om CNF X ) ` F ) e. ( _om ^o X ) ) )

Proof

Step Hyp Ref Expression
1 cantnfub.0 
 |-  ( ph -> X e. On )
2 cantnfub.n 
 |-  ( ph -> N e. _om )
3 cantnfub.a 
 |-  ( ph -> A : N -1-1-> X )
4 cantnfub.m 
 |-  ( ph -> M : N --> _om )
5 cantnfub.f 
 |-  F = ( x e. X |-> if ( x e. ran A , ( M ` ( `' A ` x ) ) , (/) ) )
6 4 ad2antrr 
 |-  ( ( ( ph /\ x e. X ) /\ x e. ran A ) -> M : N --> _om )
7 3 ad2antrr 
 |-  ( ( ( ph /\ x e. X ) /\ x e. ran A ) -> A : N -1-1-> X )
8 f1f1orn 
 |-  ( A : N -1-1-> X -> A : N -1-1-onto-> ran A )
9 7 8 syl 
 |-  ( ( ( ph /\ x e. X ) /\ x e. ran A ) -> A : N -1-1-onto-> ran A )
10 f1ocnvdm 
 |-  ( ( A : N -1-1-onto-> ran A /\ x e. ran A ) -> ( `' A ` x ) e. N )
11 9 10 sylancom 
 |-  ( ( ( ph /\ x e. X ) /\ x e. ran A ) -> ( `' A ` x ) e. N )
12 6 11 ffvelcdmd 
 |-  ( ( ( ph /\ x e. X ) /\ x e. ran A ) -> ( M ` ( `' A ` x ) ) e. _om )
13 peano1 
 |-  (/) e. _om
14 13 a1i 
 |-  ( ( ( ph /\ x e. X ) /\ -. x e. ran A ) -> (/) e. _om )
15 12 14 ifclda 
 |-  ( ( ph /\ x e. X ) -> if ( x e. ran A , ( M ` ( `' A ` x ) ) , (/) ) e. _om )
16 15 5 fmptd 
 |-  ( ph -> F : X --> _om )
17 f1fn 
 |-  ( A : N -1-1-> X -> A Fn N )
18 3 17 syl 
 |-  ( ph -> A Fn N )
19 nnon 
 |-  ( N e. _om -> N e. On )
20 onfin 
 |-  ( N e. On -> ( N e. Fin <-> N e. _om ) )
21 2 19 20 3syl 
 |-  ( ph -> ( N e. Fin <-> N e. _om ) )
22 2 21 mpbird 
 |-  ( ph -> N e. Fin )
23 18 22 jca 
 |-  ( ph -> ( A Fn N /\ N e. Fin ) )
24 fnfi 
 |-  ( ( A Fn N /\ N e. Fin ) -> A e. Fin )
25 rnfi 
 |-  ( A e. Fin -> ran A e. Fin )
26 23 24 25 3syl 
 |-  ( ph -> ran A e. Fin )
27 eldifi 
 |-  ( y e. ( X \ ran A ) -> y e. X )
28 27 adantl 
 |-  ( ( ph /\ y e. ( X \ ran A ) ) -> y e. X )
29 eleq1w 
 |-  ( x = y -> ( x e. ran A <-> y e. ran A ) )
30 2fveq3 
 |-  ( x = y -> ( M ` ( `' A ` x ) ) = ( M ` ( `' A ` y ) ) )
31 29 30 ifbieq1d 
 |-  ( x = y -> if ( x e. ran A , ( M ` ( `' A ` x ) ) , (/) ) = if ( y e. ran A , ( M ` ( `' A ` y ) ) , (/) ) )
32 fvex 
 |-  ( M ` ( `' A ` y ) ) e. _V
33 0ex 
 |-  (/) e. _V
34 32 33 ifex 
 |-  if ( y e. ran A , ( M ` ( `' A ` y ) ) , (/) ) e. _V
35 31 5 34 fvmpt 
 |-  ( y e. X -> ( F ` y ) = if ( y e. ran A , ( M ` ( `' A ` y ) ) , (/) ) )
36 28 35 syl 
 |-  ( ( ph /\ y e. ( X \ ran A ) ) -> ( F ` y ) = if ( y e. ran A , ( M ` ( `' A ` y ) ) , (/) ) )
37 eldifn 
 |-  ( y e. ( X \ ran A ) -> -. y e. ran A )
38 37 adantl 
 |-  ( ( ph /\ y e. ( X \ ran A ) ) -> -. y e. ran A )
39 38 iffalsed 
 |-  ( ( ph /\ y e. ( X \ ran A ) ) -> if ( y e. ran A , ( M ` ( `' A ` y ) ) , (/) ) = (/) )
40 36 39 eqtrd 
 |-  ( ( ph /\ y e. ( X \ ran A ) ) -> ( F ` y ) = (/) )
41 16 40 suppss 
 |-  ( ph -> ( F supp (/) ) C_ ran A )
42 26 41 ssfid 
 |-  ( ph -> ( F supp (/) ) e. Fin )
43 16 ffund 
 |-  ( ph -> Fun F )
44 omelon 
 |-  _om e. On
45 44 a1i 
 |-  ( ph -> _om e. On )
46 45 1 elmapd 
 |-  ( ph -> ( F e. ( _om ^m X ) <-> F : X --> _om ) )
47 16 46 mpbird 
 |-  ( ph -> F e. ( _om ^m X ) )
48 13 a1i 
 |-  ( ph -> (/) e. _om )
49 funisfsupp 
 |-  ( ( Fun F /\ F e. ( _om ^m X ) /\ (/) e. _om ) -> ( F finSupp (/) <-> ( F supp (/) ) e. Fin ) )
50 43 47 48 49 syl3anc 
 |-  ( ph -> ( F finSupp (/) <-> ( F supp (/) ) e. Fin ) )
51 42 50 mpbird 
 |-  ( ph -> F finSupp (/) )
52 eqid 
 |-  dom ( _om CNF X ) = dom ( _om CNF X )
53 52 45 1 cantnfs 
 |-  ( ph -> ( F e. dom ( _om CNF X ) <-> ( F : X --> _om /\ F finSupp (/) ) ) )
54 16 51 53 mpbir2and 
 |-  ( ph -> F e. dom ( _om CNF X ) )
55 52 45 1 cantnff 
 |-  ( ph -> ( _om CNF X ) : dom ( _om CNF X ) --> ( _om ^o X ) )
56 55 54 ffvelcdmd 
 |-  ( ph -> ( ( _om CNF X ) ` F ) e. ( _om ^o X ) )
57 54 56 jca 
 |-  ( ph -> ( F e. dom ( _om CNF X ) /\ ( ( _om CNF X ) ` F ) e. ( _om ^o X ) ) )