alephsing

Description: The cofinality of a limit aleph is the same as the cofinality of its argument, so if ( alephA ) < A , then ( alephA ) is singular. Conversely, if ( alephA ) is regular (i.e. weakly inaccessible), then ( alephA ) = A , so A has to be rather large (see alephfp ). Proposition 11.13 of TakeutiZaring p. 103. (Contributed by Mario Carneiro, 9-Mar-2013)

		Ref	Expression
	Assertion	alephsing	$⊢ Lim A \to cf (ℵ (A)) = cf (A)$

Proof

Step	Hyp	Ref	Expression
1		alephfnon	$⊢ ℵ Fn On$
2		fnfun	$⊢ ℵ Fn On \to Fun ℵ$
3	1 2	ax-mp	$⊢ Fun ℵ$
4		simpl	$⊢ (A \in V \land Lim A) \to A \in V$
5		resfunexg	$⊢ (Fun ℵ \land A \in V) \to {ℵ ↾}_{A} \in V$
6	3 4 5	sylancr	$⊢ (A \in V \land Lim A) \to {ℵ ↾}_{A} \in V$
7		limelon	$⊢ (A \in V \land Lim A) \to A \in On$
8		onss	$⊢ A \in On \to A \subseteq On$
9	7 8	syl	$⊢ (A \in V \land Lim A) \to A \subseteq On$
10		fnssres	$⊢ (ℵ Fn On \land A \subseteq On) \to ({ℵ ↾}_{A}) Fn A$
11	1 9 10	sylancr	$⊢ (A \in V \land Lim A) \to ({ℵ ↾}_{A}) Fn A$
12		fvres	$⊢ y \in A \to ({ℵ ↾}_{A}) (y) = ℵ (y)$
13	12	adantl	$⊢ (A \in On \land y \in A) \to ({ℵ ↾}_{A}) (y) = ℵ (y)$
14		alephord2i	$⊢ A \in On \to (y \in A \to ℵ (y) \in ℵ (A))$
15	14	imp	$⊢ (A \in On \land y \in A) \to ℵ (y) \in ℵ (A)$
16	13 15	eqeltrd	$⊢ (A \in On \land y \in A) \to ({ℵ ↾}_{A}) (y) \in ℵ (A)$
17	7 16	sylan	$⊢ ((A \in V \land Lim A) \land y \in A) \to ({ℵ ↾}_{A}) (y) \in ℵ (A)$
18	17	ralrimiva	$⊢ (A \in V \land Lim A) \to \forall y \in A ({ℵ ↾}_{A}) (y) \in ℵ (A)$
19		fnfvrnss	$⊢ (({ℵ ↾}_{A}) Fn A \land \forall y \in A ({ℵ ↾}_{A}) (y) \in ℵ (A)) \to ran ({ℵ ↾}_{A}) \subseteq ℵ (A)$
20	11 18 19	syl2anc	$⊢ (A \in V \land Lim A) \to ran ({ℵ ↾}_{A}) \subseteq ℵ (A)$
21		df-f	$⊢ ({ℵ ↾}_{A}) : A ⟶ ℵ (A) \leftrightarrow (({ℵ ↾}_{A}) Fn A \land ran ({ℵ ↾}_{A}) \subseteq ℵ (A))$
22	11 20 21	sylanbrc	$⊢ (A \in V \land Lim A) \to ({ℵ ↾}_{A}) : A ⟶ ℵ (A)$
23		alephsmo	$⊢ Smo ℵ$
24	1	fndmi	$⊢ dom ℵ = On$
25	7 24	eleqtrrdi	$⊢ (A \in V \land Lim A) \to A \in dom ℵ$
26		smores	$⊢ (Smo ℵ \land A \in dom ℵ) \to Smo ({ℵ ↾}_{A})$
27	23 25 26	sylancr	$⊢ (A \in V \land Lim A) \to Smo ({ℵ ↾}_{A})$
28		alephlim	$⊢ (A \in V \land Lim A) \to ℵ (A) = ⋃_{y \in A} ℵ (y)$
29	28	eleq2d	$⊢ (A \in V \land Lim A) \to (x \in ℵ (A) \leftrightarrow x \in ⋃_{y \in A} ℵ (y))$
30		eliun	$⊢ x \in ⋃_{y \in A} ℵ (y) \leftrightarrow \exists y \in A x \in ℵ (y)$
31		alephon	$⊢ ℵ (y) \in On$
32	31	onelssi	$⊢ x \in ℵ (y) \to x \subseteq ℵ (y)$
33	32	reximi	$⊢ \exists y \in A x \in ℵ (y) \to \exists y \in A x \subseteq ℵ (y)$
34	30 33	sylbi	$⊢ x \in ⋃_{y \in A} ℵ (y) \to \exists y \in A x \subseteq ℵ (y)$
35	29 34	syl6bi	$⊢ (A \in V \land Lim A) \to (x \in ℵ (A) \to \exists y \in A x \subseteq ℵ (y))$
36	35	ralrimiv	$⊢ (A \in V \land Lim A) \to \forall x \in ℵ (A) \exists y \in A x \subseteq ℵ (y)$
37		feq1	$⊢ f = {ℵ ↾}_{A} \to (f : A ⟶ ℵ (A) \leftrightarrow ({ℵ ↾}_{A}) : A ⟶ ℵ (A))$
38		smoeq	$⊢ f = {ℵ ↾}_{A} \to (Smo f \leftrightarrow Smo ({ℵ ↾}_{A}))$
39		fveq1	$⊢ f = {ℵ ↾}_{A} \to f (y) = ({ℵ ↾}_{A}) (y)$
40	39 12	sylan9eq	$⊢ (f = {ℵ ↾}_{A} \land y \in A) \to f (y) = ℵ (y)$
41	40	sseq2d	$⊢ (f = {ℵ ↾}_{A} \land y \in A) \to (x \subseteq f (y) \leftrightarrow x \subseteq ℵ (y))$
42	41	rexbidva	$⊢ f = {ℵ ↾}_{A} \to (\exists y \in A x \subseteq f (y) \leftrightarrow \exists y \in A x \subseteq ℵ (y))$
43	42	ralbidv	$⊢ f = {ℵ ↾}_{A} \to (\forall x \in ℵ (A) \exists y \in A x \subseteq f (y) \leftrightarrow \forall x \in ℵ (A) \exists y \in A x \subseteq ℵ (y))$
44	37 38 43	3anbi123d	$⊢ f = {ℵ ↾}_{A} \to ((f : A ⟶ ℵ (A) \land Smo f \land \forall x \in ℵ (A) \exists y \in A x \subseteq f (y)) \leftrightarrow (({ℵ ↾}_{A}) : A ⟶ ℵ (A) \land Smo ({ℵ ↾}_{A}) \land \forall x \in ℵ (A) \exists y \in A x \subseteq ℵ (y)))$
45	44	spcegv	$⊢ {ℵ ↾}_{A} \in V \to ((({ℵ ↾}_{A}) : A ⟶ ℵ (A) \land Smo ({ℵ ↾}_{A}) \land \forall x \in ℵ (A) \exists y \in A x \subseteq ℵ (y)) \to \exists f (f : A ⟶ ℵ (A) \land Smo f \land \forall x \in ℵ (A) \exists y \in A x \subseteq f (y)))$
46	45	imp	$⊢ ({ℵ ↾}_{A} \in V \land (({ℵ ↾}_{A}) : A ⟶ ℵ (A) \land Smo ({ℵ ↾}_{A}) \land \forall x \in ℵ (A) \exists y \in A x \subseteq ℵ (y))) \to \exists f (f : A ⟶ ℵ (A) \land Smo f \land \forall x \in ℵ (A) \exists y \in A x \subseteq f (y))$
47	6 22 27 36 46	syl13anc	$⊢ (A \in V \land Lim A) \to \exists f (f : A ⟶ ℵ (A) \land Smo f \land \forall x \in ℵ (A) \exists y \in A x \subseteq f (y))$
48		alephon	$⊢ ℵ (A) \in On$
49		cfcof	$⊢ (ℵ (A) \in On \land A \in On) \to (\exists f (f : A ⟶ ℵ (A) \land Smo f \land \forall x \in ℵ (A) \exists y \in A x \subseteq f (y)) \to cf (ℵ (A)) = cf (A))$
50	48 7 49	sylancr	$⊢ (A \in V \land Lim A) \to (\exists f (f : A ⟶ ℵ (A) \land Smo f \land \forall x \in ℵ (A) \exists y \in A x \subseteq f (y)) \to cf (ℵ (A)) = cf (A))$
51	47 50	mpd	$⊢ (A \in V \land Lim A) \to cf (ℵ (A)) = cf (A)$
52	51	expcom	$⊢ Lim A \to (A \in V \to cf (ℵ (A)) = cf (A))$
53		cf0	$⊢ cf (\emptyset) = \emptyset$
54		fvprc	$⊢ \neg A \in V \to ℵ (A) = \emptyset$
55	54	fveq2d	$⊢ \neg A \in V \to cf (ℵ (A)) = cf (\emptyset)$
56		fvprc	$⊢ \neg A \in V \to cf (A) = \emptyset$
57	53 55 56	3eqtr4a	$⊢ \neg A \in V \to cf (ℵ (A)) = cf (A)$
58	52 57	pm2.61d1	$⊢ Lim A \to cf (ℵ (A)) = cf (A)$

Metamath Proof Explorer

Theorem alephsing

Proof