cfval

Description: Value of the cofinality function. Definition B of Saharon Shelah, Cardinal Arithmetic (1994), p. xxx (Roman numeral 30). The cofinality of an ordinal number A is the cardinality (size) of the smallest unbounded subset y of the ordinal number. Unbounded means that for every member of A , there is a member of y that is at least as large. Cofinality is a measure of how "reachable from below" an ordinal is. (Contributed by NM, 1-Apr-2004) (Revised by Mario Carneiro, 15-Sep-2013)

		Ref	Expression
	Assertion	cfval	$⊢ A \in On \to cf (A) = ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\}$

Proof

Step	Hyp	Ref	Expression
1		cflem	$⊢ A \in On \to \exists x \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))$
2		intexab	$⊢ \exists x \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \leftrightarrow ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\} \in V$
3	1 2	sylib	$⊢ A \in On \to ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\} \in V$
4		sseq2	$⊢ v = A \to (y \subseteq v \leftrightarrow y \subseteq A)$
5		raleq	$⊢ v = A \to (\forall z \in v \exists w \in y z \subseteq w \leftrightarrow \forall z \in A \exists w \in y z \subseteq w)$
6	4 5	anbi12d	$⊢ v = A \to ((y \subseteq v \land \forall z \in v \exists w \in y z \subseteq w) \leftrightarrow (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))$
7	6	anbi2d	$⊢ v = A \to ((x = card (y) \land (y \subseteq v \land \forall z \in v \exists w \in y z \subseteq w)) \leftrightarrow (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)))$
8	7	exbidv	$⊢ v = A \to (\exists y (x = card (y) \land (y \subseteq v \land \forall z \in v \exists w \in y z \subseteq w)) \leftrightarrow \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)))$
9	8	abbidv	$⊢ v = A \to \{x \| \exists y (x = card (y) \land (y \subseteq v \land \forall z \in v \exists w \in y z \subseteq w))\} = \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\}$
10	9	inteqd	$⊢ v = A \to ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq v \land \forall z \in v \exists w \in y z \subseteq w))\} = ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\}$
11		df-cf	$⊢ cf = (v \in On ⟼ ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq v \land \forall z \in v \exists w \in y z \subseteq w))\})$
12	10 11	fvmptg	$⊢ (A \in On \land ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\} \in V) \to cf (A) = ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\}$
13	3 12	mpdan	$⊢ A \in On \to cf (A) = ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\}$

Metamath Proof Explorer

Theorem cfval

Proof