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	$⊢ φ \to X \in On$
	cantnfub.n	$⊢ φ \to N \in ω$
	cantnfub.a	$⊢ φ \to A : N \underset{1-1}{⟶} X$
	cantnfub.m	$⊢ φ \to M : N ⟶ ω$
	cantnfub.f	$⊢ F = (x \in X ⟼ if (x \in ran A, M (A^{-1} (x)), \emptyset))$
Assertion	cantnfub	$⊢ φ \to (F \in dom (ω CNF X) \land (ω CNF X) (F) \in (ω ↑_{𝑜} X))$

Proof

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

Metamath Proof Explorer

Theorem cantnfub

Proof