Metamath Proof Explorer

Theorem cantnfub2

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 suc U. ran A ) when ( Mn ) is less than _om . Lemma 5.2 of Schloeder p. 15. (Contributed by RP, 9-Feb-2025)

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

Proof

Step Hyp Ref Expression
1 cantnfub2.n 
 |-  ( ph -> N e. _om )
2 cantnfub2.a 
 |-  ( ph -> A : N -1-1-> On )
3 cantnfub2.m 
 |-  ( ph -> M : N --> _om )
4 cantnfub2.f 
 |-  F = ( x e. suc U. ran A |-> if ( x e. ran A , ( M ` ( `' A ` x ) ) , (/) ) )
5 f1fn 
 |-  ( A : N -1-1-> On -> A Fn N )
6 2 5 syl 
 |-  ( ph -> A Fn N )
7 nnfi 
 |-  ( N e. _om -> N e. Fin )
8 1 7 syl 
 |-  ( ph -> N e. Fin )
9 fnfi 
 |-  ( ( A Fn N /\ N e. Fin ) -> A e. Fin )
10 6 8 9 syl2anc 
 |-  ( ph -> A e. Fin )
11 rnfi 
 |-  ( A e. Fin -> ran A e. Fin )
12 10 11 syl 
 |-  ( ph -> ran A e. Fin )
13 f1f 
 |-  ( A : N -1-1-> On -> A : N --> On )
14 2 13 syl 
 |-  ( ph -> A : N --> On )
15 14 frnd 
 |-  ( ph -> ran A C_ On )
16 ssonuni 
 |-  ( ran A e. Fin -> ( ran A C_ On -> U. ran A e. On ) )
17 12 15 16 sylc 
 |-  ( ph -> U. ran A e. On )
18 onsuc 
 |-  ( U. ran A e. On -> suc U. ran A e. On )
19 17 18 syl 
 |-  ( ph -> suc U. ran A e. On )
20 onsucuni 
 |-  ( ran A C_ On -> ran A C_ suc U. ran A )
21 15 20 syl 
 |-  ( ph -> ran A C_ suc U. ran A )
22 f1ssr 
 |-  ( ( A : N -1-1-> On /\ ran A C_ suc U. ran A ) -> A : N -1-1-> suc U. ran A )
23 2 21 22 syl2anc 
 |-  ( ph -> A : N -1-1-> suc U. ran A )
24 19 1 23 3 4 cantnfub 
 |-  ( ph -> ( F e. dom ( _om CNF suc U. ran A ) /\ ( ( _om CNF suc U. ran A ) ` F ) e. ( _om ^o suc U. ran A ) ) )
25 3anass 
 |-  ( ( suc U. ran A e. On /\ F e. dom ( _om CNF suc U. ran A ) /\ ( ( _om CNF suc U. ran A ) ` F ) e. ( _om ^o suc U. ran A ) ) <-> ( suc U. ran A e. On /\ ( F e. dom ( _om CNF suc U. ran A ) /\ ( ( _om CNF suc U. ran A ) ` F ) e. ( _om ^o suc U. ran A ) ) ) )
26 19 24 25 sylanbrc 
 |-  ( ph -> ( suc U. ran A e. On /\ F e. dom ( _om CNF suc U. ran A ) /\ ( ( _om CNF suc U. ran A ) ` F ) e. ( _om ^o suc U. ran A ) ) )