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

Proof

Step	Hyp	Ref	Expression
1		cantnfub2.n	$⊢ φ \to N \in ω$
2		cantnfub2.a	$⊢ φ \to A : N \underset{1-1}{⟶} On$
3		cantnfub2.m	$⊢ φ \to M : N ⟶ ω$
4		cantnfub2.f	$⊢ F = (x \in suc ⋃ ran A ⟼ if (x \in ran A, M (A^{-1} (x)), \emptyset))$
5		f1fn	$⊢ A : N \underset{1-1}{⟶} On \to A Fn N$
6	2 5	syl	$⊢ φ \to A Fn N$
7		nnfi	$⊢ N \in ω \to N \in Fin$
8	1 7	syl	$⊢ φ \to N \in Fin$
9		fnfi	$⊢ (A Fn N \land N \in Fin) \to A \in Fin$
10	6 8 9	syl2anc	$⊢ φ \to A \in Fin$
11		rnfi	$⊢ A \in Fin \to ran A \in Fin$
12	10 11	syl	$⊢ φ \to ran A \in Fin$
13		f1f	$⊢ A : N \underset{1-1}{⟶} On \to A : N ⟶ On$
14	2 13	syl	$⊢ φ \to A : N ⟶ On$
15	14	frnd	$⊢ φ \to ran A \subseteq On$
16		ssonuni	$⊢ ran A \in Fin \to (ran A \subseteq On \to ⋃ ran A \in On)$
17	12 15 16	sylc	$⊢ φ \to ⋃ ran A \in On$
18		onsuc	$⊢ ⋃ ran A \in On \to suc ⋃ ran A \in On$
19	17 18	syl	$⊢ φ \to suc ⋃ ran A \in On$
20		onsucuni	$⊢ ran A \subseteq On \to ran A \subseteq suc ⋃ ran A$
21	15 20	syl	$⊢ φ \to ran A \subseteq suc ⋃ ran A$
22		f1ssr	$⊢ (A : N \underset{1-1}{⟶} On \land ran A \subseteq suc ⋃ ran A) \to A : N \underset{1-1}{⟶} suc ⋃ ran A$
23	2 21 22	syl2anc	$⊢ φ \to A : N \underset{1-1}{⟶} suc ⋃ ran A$
24	19 1 23 3 4	cantnfub	$⊢ φ \to (F \in dom (ω CNF suc ⋃ ran A) \land (ω CNF suc ⋃ ran A) (F) \in (ω ↑_{𝑜} suc ⋃ ran A))$
25		3anass	$⊢ (suc ⋃ ran A \in On \land F \in dom (ω CNF suc ⋃ ran A) \land (ω CNF suc ⋃ ran A) (F) \in (ω ↑_{𝑜} suc ⋃ ran A)) \leftrightarrow (suc ⋃ ran A \in On \land (F \in dom (ω CNF suc ⋃ ran A) \land (ω CNF suc ⋃ ran A) (F) \in (ω ↑_{𝑜} suc ⋃ ran A)))$
26	19 24 25	sylanbrc	$⊢ φ \to (suc ⋃ ran A \in On \land F \in dom (ω CNF suc ⋃ ran A) \land (ω CNF suc ⋃ ran A) (F) \in (ω ↑_{𝑜} suc ⋃ ran A))$

Metamath Proof Explorer

Theorem cantnfub2

Proof