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

Proof

Step	Hyp	Ref	Expression
1		cantnfub.0	⊢ ( 𝜑 → 𝑋 ∈ On )
2		cantnfub.n	⊢ ( 𝜑 → 𝑁 ∈ ω )
3		cantnfub.a	⊢ ( 𝜑 → 𝐴 : 𝑁 –1-1→ 𝑋 )
4		cantnfub.m	⊢ ( 𝜑 → 𝑀 : 𝑁 ⟶ ω )
5		cantnfub.f	⊢ 𝐹 = ( 𝑥 ∈ 𝑋 ↦ if ( 𝑥 ∈ ran 𝐴 , ( 𝑀 ‘ ( ◡ 𝐴 ‘ 𝑥 ) ) , ∅ ) )
6	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑥 ∈ ran 𝐴 ) → 𝑀 : 𝑁 ⟶ ω )
7	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑥 ∈ ran 𝐴 ) → 𝐴 : 𝑁 –1-1→ 𝑋 )
8		f1f1orn	⊢ ( 𝐴 : 𝑁 –1-1→ 𝑋 → 𝐴 : 𝑁 –1-1-onto→ ran 𝐴 )
9	7 8	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑥 ∈ ran 𝐴 ) → 𝐴 : 𝑁 –1-1-onto→ ran 𝐴 )
10		f1ocnvdm	⊢ ( ( 𝐴 : 𝑁 –1-1-onto→ ran 𝐴 ∧ 𝑥 ∈ ran 𝐴 ) → ( ◡ 𝐴 ‘ 𝑥 ) ∈ 𝑁 )
11	9 10	sylancom	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑥 ∈ ran 𝐴 ) → ( ◡ 𝐴 ‘ 𝑥 ) ∈ 𝑁 )
12	6 11	ffvelcdmd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑥 ∈ ran 𝐴 ) → ( 𝑀 ‘ ( ◡ 𝐴 ‘ 𝑥 ) ) ∈ ω )
13		peano1	⊢ ∅ ∈ ω
14	13	a1i	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ ¬ 𝑥 ∈ ran 𝐴 ) → ∅ ∈ ω )
15	12 14	ifclda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → if ( 𝑥 ∈ ran 𝐴 , ( 𝑀 ‘ ( ◡ 𝐴 ‘ 𝑥 ) ) , ∅ ) ∈ ω )
16	15 5	fmptd	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ω )
17		f1fn	⊢ ( 𝐴 : 𝑁 –1-1→ 𝑋 → 𝐴 Fn 𝑁 )
18	3 17	syl	⊢ ( 𝜑 → 𝐴 Fn 𝑁 )
19		nnon	⊢ ( 𝑁 ∈ ω → 𝑁 ∈ On )
20		onfin	⊢ ( 𝑁 ∈ On → ( 𝑁 ∈ Fin ↔ 𝑁 ∈ ω ) )
21	2 19 20	3syl	⊢ ( 𝜑 → ( 𝑁 ∈ Fin ↔ 𝑁 ∈ ω ) )
22	2 21	mpbird	⊢ ( 𝜑 → 𝑁 ∈ Fin )
23	18 22	jca	⊢ ( 𝜑 → ( 𝐴 Fn 𝑁 ∧ 𝑁 ∈ Fin ) )
24		fnfi	⊢ ( ( 𝐴 Fn 𝑁 ∧ 𝑁 ∈ Fin ) → 𝐴 ∈ Fin )
25		rnfi	⊢ ( 𝐴 ∈ Fin → ran 𝐴 ∈ Fin )
26	23 24 25	3syl	⊢ ( 𝜑 → ran 𝐴 ∈ Fin )
27		eldifi	⊢ ( 𝑦 ∈ ( 𝑋 ∖ ran 𝐴 ) → 𝑦 ∈ 𝑋 )
28	27	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ ran 𝐴 ) ) → 𝑦 ∈ 𝑋 )
29		eleq1w	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ ran 𝐴 ↔ 𝑦 ∈ ran 𝐴 ) )
30		2fveq3	⊢ ( 𝑥 = 𝑦 → ( 𝑀 ‘ ( ◡ 𝐴 ‘ 𝑥 ) ) = ( 𝑀 ‘ ( ◡ 𝐴 ‘ 𝑦 ) ) )
31	29 30	ifbieq1d	⊢ ( 𝑥 = 𝑦 → if ( 𝑥 ∈ ran 𝐴 , ( 𝑀 ‘ ( ◡ 𝐴 ‘ 𝑥 ) ) , ∅ ) = if ( 𝑦 ∈ ran 𝐴 , ( 𝑀 ‘ ( ◡ 𝐴 ‘ 𝑦 ) ) , ∅ ) )
32		fvex	⊢ ( 𝑀 ‘ ( ◡ 𝐴 ‘ 𝑦 ) ) ∈ V
33		0ex	⊢ ∅ ∈ V
34	32 33	ifex	⊢ if ( 𝑦 ∈ ran 𝐴 , ( 𝑀 ‘ ( ◡ 𝐴 ‘ 𝑦 ) ) , ∅ ) ∈ V
35	31 5 34	fvmpt	⊢ ( 𝑦 ∈ 𝑋 → ( 𝐹 ‘ 𝑦 ) = if ( 𝑦 ∈ ran 𝐴 , ( 𝑀 ‘ ( ◡ 𝐴 ‘ 𝑦 ) ) , ∅ ) )
36	28 35	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ ran 𝐴 ) ) → ( 𝐹 ‘ 𝑦 ) = if ( 𝑦 ∈ ran 𝐴 , ( 𝑀 ‘ ( ◡ 𝐴 ‘ 𝑦 ) ) , ∅ ) )
37		eldifn	⊢ ( 𝑦 ∈ ( 𝑋 ∖ ran 𝐴 ) → ¬ 𝑦 ∈ ran 𝐴 )
38	37	adantl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ ran 𝐴 ) ) → ¬ 𝑦 ∈ ran 𝐴 )
39	38	iffalsed	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ ran 𝐴 ) ) → if ( 𝑦 ∈ ran 𝐴 , ( 𝑀 ‘ ( ◡ 𝐴 ‘ 𝑦 ) ) , ∅ ) = ∅ )
40	36 39	eqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 ∖ ran 𝐴 ) ) → ( 𝐹 ‘ 𝑦 ) = ∅ )
41	16 40	suppss	⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ⊆ ran 𝐴 )
42	26 41	ssfid	⊢ ( 𝜑 → ( 𝐹 supp ∅ ) ∈ Fin )
43	16	ffund	⊢ ( 𝜑 → Fun 𝐹 )
44		omelon	⊢ ω ∈ On
45	44	a1i	⊢ ( 𝜑 → ω ∈ On )
46	45 1	elmapd	⊢ ( 𝜑 → ( 𝐹 ∈ ( ω ↑m 𝑋 ) ↔ 𝐹 : 𝑋 ⟶ ω ) )
47	16 46	mpbird	⊢ ( 𝜑 → 𝐹 ∈ ( ω ↑m 𝑋 ) )
48	13	a1i	⊢ ( 𝜑 → ∅ ∈ ω )
49		funisfsupp	⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ ( ω ↑m 𝑋 ) ∧ ∅ ∈ ω ) → ( 𝐹 finSupp ∅ ↔ ( 𝐹 supp ∅ ) ∈ Fin ) )
50	43 47 48 49	syl3anc	⊢ ( 𝜑 → ( 𝐹 finSupp ∅ ↔ ( 𝐹 supp ∅ ) ∈ Fin ) )
51	42 50	mpbird	⊢ ( 𝜑 → 𝐹 finSupp ∅ )
52		eqid	⊢ dom ( ω CNF 𝑋 ) = dom ( ω CNF 𝑋 )
53	52 45 1	cantnfs	⊢ ( 𝜑 → ( 𝐹 ∈ dom ( ω CNF 𝑋 ) ↔ ( 𝐹 : 𝑋 ⟶ ω ∧ 𝐹 finSupp ∅ ) ) )
54	16 51 53	mpbir2and	⊢ ( 𝜑 → 𝐹 ∈ dom ( ω CNF 𝑋 ) )
55	52 45 1	cantnff	⊢ ( 𝜑 → ( ω CNF 𝑋 ) : dom ( ω CNF 𝑋 ) ⟶ ( ω ↑o 𝑋 ) )
56	55 54	ffvelcdmd	⊢ ( 𝜑 → ( ( ω CNF 𝑋 ) ‘ 𝐹 ) ∈ ( ω ↑o 𝑋 ) )
57	54 56	jca	⊢ ( 𝜑 → ( 𝐹 ∈ dom ( ω CNF 𝑋 ) ∧ ( ( ω CNF 𝑋 ) ‘ 𝐹 ) ∈ ( ω ↑o 𝑋 ) ) )