cflm

Description: Value of the cofinality function at a limit ordinal. Part of Definition of cofinality of Enderton p. 257. (Contributed by NM, 26-Apr-2004)

		Ref	Expression
	Assertion	cflm	$⊢ (A \in B \land Lim A) \to cf (A) = ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\}$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in B \to A \in V$
2		limsuc	$⊢ Lim A \to (v \in A \leftrightarrow suc v \in A)$
3	2	biimpd	$⊢ Lim A \to (v \in A \to suc v \in A)$
4		sseq1	$⊢ z = suc v \to (z \subseteq w \leftrightarrow suc v \subseteq w)$
5	4	rexbidv	$⊢ z = suc v \to (\exists w \in y z \subseteq w \leftrightarrow \exists w \in y suc v \subseteq w)$
6	5	rspcv	$⊢ suc v \in A \to (\forall z \in A \exists w \in y z \subseteq w \to \exists w \in y suc v \subseteq w)$
7		sucssel	$⊢ v \in V \to (suc v \subseteq w \to v \in w)$
8	7	elv	$⊢ suc v \subseteq w \to v \in w$
9	8	reximi	$⊢ \exists w \in y suc v \subseteq w \to \exists w \in y v \in w$
10		eluni2	$⊢ v \in ⋃ y \leftrightarrow \exists w \in y v \in w$
11	9 10	sylibr	$⊢ \exists w \in y suc v \subseteq w \to v \in ⋃ y$
12	6 11	syl6com	$⊢ \forall z \in A \exists w \in y z \subseteq w \to (suc v \in A \to v \in ⋃ y)$
13	3 12	syl9	$⊢ Lim A \to (\forall z \in A \exists w \in y z \subseteq w \to (v \in A \to v \in ⋃ y))$
14	13	ralrimdv	$⊢ Lim A \to (\forall z \in A \exists w \in y z \subseteq w \to \forall v \in A v \in ⋃ y)$
15		dfss3	$⊢ A \subseteq ⋃ y \leftrightarrow \forall v \in A v \in ⋃ y$
16	14 15	imbitrrdi	$⊢ Lim A \to (\forall z \in A \exists w \in y z \subseteq w \to A \subseteq ⋃ y)$
17	16	adantr	$⊢ (Lim A \land y \subseteq A) \to (\forall z \in A \exists w \in y z \subseteq w \to A \subseteq ⋃ y)$
18		uniss	$⊢ y \subseteq A \to ⋃ y \subseteq ⋃ A$
19		limuni	$⊢ Lim A \to A = ⋃ A$
20	19	sseq2d	$⊢ Lim A \to (⋃ y \subseteq A \leftrightarrow ⋃ y \subseteq ⋃ A)$
21	18 20	imbitrrid	$⊢ Lim A \to (y \subseteq A \to ⋃ y \subseteq A)$
22	21	imp	$⊢ (Lim A \land y \subseteq A) \to ⋃ y \subseteq A$
23	17 22	jctird	$⊢ (Lim A \land y \subseteq A) \to (\forall z \in A \exists w \in y z \subseteq w \to (A \subseteq ⋃ y \land ⋃ y \subseteq A))$
24		eqss	$⊢ A = ⋃ y \leftrightarrow (A \subseteq ⋃ y \land ⋃ y \subseteq A)$
25	23 24	imbitrrdi	$⊢ (Lim A \land y \subseteq A) \to (\forall z \in A \exists w \in y z \subseteq w \to A = ⋃ y)$
26	25	imdistanda	$⊢ Lim A \to ((y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w) \to (y \subseteq A \land A = ⋃ y))$
27	26	anim2d	$⊢ Lim A \to ((x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \to (x = card (y) \land (y \subseteq A \land A = ⋃ y)))$
28	27	eximdv	$⊢ Lim A \to (\exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w)) \to \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y)))$
29	28	ss2abdv	$⊢ Lim A \to \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\} \subseteq \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\}$
30		intss	$⊢ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\} \subseteq \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \to ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \subseteq ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\}$
31	29 30	syl	$⊢ Lim A \to ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \subseteq ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\}$
32	31	adantl	$⊢ (A \in V \land Lim A) \to ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \subseteq ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists w \in y z \subseteq w))\}$
33		limelon	$⊢ (A \in V \land Lim A) \to A \in On$
34		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))\}$
35	33 34	syl	$⊢ (A \in V \land Lim A) \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))\}$
36	32 35	sseqtrrd	$⊢ (A \in V \land Lim A) \to ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \subseteq cf (A)$
37		cfub	$⊢ cf (A) \subseteq ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y))\}$
38		eqimss	$⊢ A = ⋃ y \to A \subseteq ⋃ y$
39	38	anim2i	$⊢ (y \subseteq A \land A = ⋃ y) \to (y \subseteq A \land A \subseteq ⋃ y)$
40	39	anim2i	$⊢ (x = card (y) \land (y \subseteq A \land A = ⋃ y)) \to (x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y))$
41	40	eximi	$⊢ \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y)) \to \exists y (x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y))$
42	41	ss2abi	$⊢ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \subseteq \{x \| \exists y (x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y))\}$
43		intss	$⊢ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \subseteq \{x \| \exists y (x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y))\} \to ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y))\} \subseteq ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\}$
44	42 43	ax-mp	$⊢ ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A \subseteq ⋃ y))\} \subseteq ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\}$
45	37 44	sstri	$⊢ cf (A) \subseteq ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\}$
46	36 45	jctil	$⊢ (A \in V \land Lim A) \to (cf (A) \subseteq ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \land ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \subseteq cf (A))$
47		eqss	$⊢ cf (A) = ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \leftrightarrow (cf (A) \subseteq ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \land ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\} \subseteq cf (A))$
48	46 47	sylibr	$⊢ (A \in V \land Lim A) \to cf (A) = ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\}$
49	1 48	sylan	$⊢ (A \in B \land Lim A) \to cf (A) = ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land A = ⋃ y))\}$

Metamath Proof Explorer

Theorem cflm

Proof