cflim3

Description: Another expression for the cofinality function. (Contributed by Mario Carneiro, 28-Feb-2013)

		Ref	Expression
	Hypothesis	cflim3.1	$⊢ A \in V$
	Assertion	cflim3	$⊢ Lim A \to cf (A) = ⋂_{x \in \{x \in 𝒫 A \| ⋃ x = A\}} card (x)$

Proof

Step	Hyp	Ref	Expression
1		cflim3.1	$⊢ A \in V$
2		limord	$⊢ Lim A \to Ord A$
3	1	elon	$⊢ A \in On \leftrightarrow Ord A$
4	2 3	sylibr	$⊢ Lim A \to A \in On$
5		cfval	$⊢ A \in On \to cf (A) = ⋂ \{y \| \exists x (y = card (x) \land (x \subseteq A \land \forall z \in A \exists w \in x z \subseteq w))\}$
6	4 5	syl	$⊢ Lim A \to cf (A) = ⋂ \{y \| \exists x (y = card (x) \land (x \subseteq A \land \forall z \in A \exists w \in x z \subseteq w))\}$
7		fvex	$⊢ card (x) \in V$
8	7	dfiin2	$⊢ ⋂_{x \in \{x \in 𝒫 A \| ⋃ x = A\}} card (x) = ⋂ \{y \| \exists x \in \{x \in 𝒫 A \| ⋃ x = A\} y = card (x)\}$
9		df-rex	$⊢ \exists x \in \{x \in 𝒫 A \| ⋃ x = A\} y = card (x) \leftrightarrow \exists x (x \in \{x \in 𝒫 A \| ⋃ x = A\} \land y = card (x))$
10		ancom	$⊢ (x \in \{x \in 𝒫 A \| ⋃ x = A\} \land y = card (x)) \leftrightarrow (y = card (x) \land x \in \{x \in 𝒫 A \| ⋃ x = A\})$
11		rabid	$⊢ x \in \{x \in 𝒫 A \| ⋃ x = A\} \leftrightarrow (x \in 𝒫 A \land ⋃ x = A)$
12		velpw	$⊢ x \in 𝒫 A \leftrightarrow x \subseteq A$
13	12	anbi1i	$⊢ (x \in 𝒫 A \land ⋃ x = A) \leftrightarrow (x \subseteq A \land ⋃ x = A)$
14		coflim	$⊢ (Lim A \land x \subseteq A) \to (⋃ x = A \leftrightarrow \forall z \in A \exists w \in x z \subseteq w)$
15	14	pm5.32da	$⊢ Lim A \to ((x \subseteq A \land ⋃ x = A) \leftrightarrow (x \subseteq A \land \forall z \in A \exists w \in x z \subseteq w))$
16	13 15	bitrid	$⊢ Lim A \to ((x \in 𝒫 A \land ⋃ x = A) \leftrightarrow (x \subseteq A \land \forall z \in A \exists w \in x z \subseteq w))$
17	11 16	bitrid	$⊢ Lim A \to (x \in \{x \in 𝒫 A \| ⋃ x = A\} \leftrightarrow (x \subseteq A \land \forall z \in A \exists w \in x z \subseteq w))$
18	17	anbi2d	$⊢ Lim A \to ((y = card (x) \land x \in \{x \in 𝒫 A \| ⋃ x = A\}) \leftrightarrow (y = card (x) \land (x \subseteq A \land \forall z \in A \exists w \in x z \subseteq w)))$
19	10 18	bitrid	$⊢ Lim A \to ((x \in \{x \in 𝒫 A \| ⋃ x = A\} \land y = card (x)) \leftrightarrow (y = card (x) \land (x \subseteq A \land \forall z \in A \exists w \in x z \subseteq w)))$
20	19	exbidv	$⊢ Lim A \to (\exists x (x \in \{x \in 𝒫 A \| ⋃ x = A\} \land y = card (x)) \leftrightarrow \exists x (y = card (x) \land (x \subseteq A \land \forall z \in A \exists w \in x z \subseteq w)))$
21	9 20	bitrid	$⊢ Lim A \to (\exists x \in \{x \in 𝒫 A \| ⋃ x = A\} y = card (x) \leftrightarrow \exists x (y = card (x) \land (x \subseteq A \land \forall z \in A \exists w \in x z \subseteq w)))$
22	21	abbidv	$⊢ Lim A \to \{y \| \exists x \in \{x \in 𝒫 A \| ⋃ x = A\} y = card (x)\} = \{y \| \exists x (y = card (x) \land (x \subseteq A \land \forall z \in A \exists w \in x z \subseteq w))\}$
23	22	inteqd	$⊢ Lim A \to ⋂ \{y \| \exists x \in \{x \in 𝒫 A \| ⋃ x = A\} y = card (x)\} = ⋂ \{y \| \exists x (y = card (x) \land (x \subseteq A \land \forall z \in A \exists w \in x z \subseteq w))\}$
24	8 23	eqtr2id	$⊢ Lim A \to ⋂ \{y \| \exists x (y = card (x) \land (x \subseteq A \land \forall z \in A \exists w \in x z \subseteq w))\} = ⋂_{x \in \{x \in 𝒫 A \| ⋃ x = A\}} card (x)$
25	6 24	eqtrd	$⊢ Lim A \to cf (A) = ⋂_{x \in \{x \in 𝒫 A \| ⋃ x = A\}} card (x)$

Metamath Proof Explorer

Theorem cflim3

Proof