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 ⊢ ( 𝜑 → 𝑁 ∈ ω )
cantnfub2.a ⊢ ( 𝜑 → 𝐴 : 𝑁 –1-1→ On )
cantnfub2.m ⊢ ( 𝜑 → 𝑀 : 𝑁 ⟶ ω )
cantnfub2.f ⊢ 𝐹 = ( 𝑥 ∈ suc ∪ ran 𝐴 ↦ if ( 𝑥 ∈ ran 𝐴 , ( 𝑀 ‘ ( ◡ 𝐴 ‘ 𝑥 ) ) , ∅ ) )
Assertion cantnfub2 ( 𝜑 → ( suc ∪ ran 𝐴 ∈ On ∧ 𝐹 ∈ dom ( ω CNF suc ∪ ran 𝐴 ) ∧ ( ( ω CNF suc ∪ ran 𝐴 ) ‘ 𝐹 ) ∈ ( ω ↑o suc ∪ ran 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 cantnfub2.n ⊢ ( 𝜑 → 𝑁 ∈ ω )
2 cantnfub2.a ⊢ ( 𝜑 → 𝐴 : 𝑁 –1-1→ On )
3 cantnfub2.m ⊢ ( 𝜑 → 𝑀 : 𝑁 ⟶ ω )
4 cantnfub2.f ⊢ 𝐹 = ( 𝑥 ∈ suc ∪ ran 𝐴 ↦ if ( 𝑥 ∈ ran 𝐴 , ( 𝑀 ‘ ( ◡ 𝐴 ‘ 𝑥 ) ) , ∅ ) )
5 f1fn ⊢ ( 𝐴 : 𝑁 –1-1→ On → 𝐴 Fn 𝑁 )
6 2 5 syl ⊢ ( 𝜑 → 𝐴 Fn 𝑁 )
7 nnfi ⊢ ( 𝑁 ∈ ω → 𝑁 ∈ Fin )
8 1 7 syl ⊢ ( 𝜑 → 𝑁 ∈ Fin )
9 fnfi ⊢ ( ( 𝐴 Fn 𝑁 ∧ 𝑁 ∈ Fin ) → 𝐴 ∈ Fin )
10 6 8 9 syl2anc ⊢ ( 𝜑 → 𝐴 ∈ Fin )
11 rnfi ⊢ ( 𝐴 ∈ Fin → ran 𝐴 ∈ Fin )
12 10 11 syl ⊢ ( 𝜑 → ran 𝐴 ∈ Fin )
13 f1f ⊢ ( 𝐴 : 𝑁 –1-1→ On → 𝐴 : 𝑁 ⟶ On )
14 2 13 syl ⊢ ( 𝜑 → 𝐴 : 𝑁 ⟶ On )
15 14 frnd ⊢ ( 𝜑 → ran 𝐴 ⊆ On )
16 ssonuni ⊢ ( ran 𝐴 ∈ Fin → ( ran 𝐴 ⊆ On → ∪ ran 𝐴 ∈ On ) )
17 12 15 16 sylc ⊢ ( 𝜑 → ∪ ran 𝐴 ∈ On )
18 onsuc ⊢ ( ∪ ran 𝐴 ∈ On → suc ∪ ran 𝐴 ∈ On )
19 17 18 syl ⊢ ( 𝜑 → suc ∪ ran 𝐴 ∈ On )
20 onsucuni ⊢ ( ran 𝐴 ⊆ On → ran 𝐴 ⊆ suc ∪ ran 𝐴 )
21 15 20 syl ⊢ ( 𝜑 → ran 𝐴 ⊆ suc ∪ ran 𝐴 )
22 f1ssr ⊢ ( ( 𝐴 : 𝑁 –1-1→ On ∧ ran 𝐴 ⊆ suc ∪ ran 𝐴 ) → 𝐴 : 𝑁 –1-1→ suc ∪ ran 𝐴 )
23 2 21 22 syl2anc ⊢ ( 𝜑 → 𝐴 : 𝑁 –1-1→ suc ∪ ran 𝐴 )
24 19 1 23 3 4 cantnfub ⊢ ( 𝜑 → ( 𝐹 ∈ dom ( ω CNF suc ∪ ran 𝐴 ) ∧ ( ( ω CNF suc ∪ ran 𝐴 ) ‘ 𝐹 ) ∈ ( ω ↑o suc ∪ ran 𝐴 ) ) )
25 3anass ⊢ ( ( suc ∪ ran 𝐴 ∈ On ∧ 𝐹 ∈ dom ( ω CNF suc ∪ ran 𝐴 ) ∧ ( ( ω CNF suc ∪ ran 𝐴 ) ‘ 𝐹 ) ∈ ( ω ↑o suc ∪ ran 𝐴 ) ) ↔ ( suc ∪ ran 𝐴 ∈ On ∧ ( 𝐹 ∈ dom ( ω CNF suc ∪ ran 𝐴 ) ∧ ( ( ω CNF suc ∪ ran 𝐴 ) ‘ 𝐹 ) ∈ ( ω ↑o suc ∪ ran 𝐴 ) ) ) )
26 19 24 25 sylanbrc ⊢ ( 𝜑 → ( suc ∪ ran 𝐴 ∈ On ∧ 𝐹 ∈ dom ( ω CNF suc ∪ ran 𝐴 ) ∧ ( ( ω CNF suc ∪ ran 𝐴 ) ‘ 𝐹 ) ∈ ( ω ↑o suc ∪ ran 𝐴 ) ) )