Theorem 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 𝐴 → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		alephfnon	⊢ ℵ Fn On
2		fnfun	⊢ ( ℵ Fn On → Fun ℵ )
3	1 2	ax-mp	⊢ Fun ℵ
4		simpl	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → 𝐴 ∈ V )
5		resfunexg	⊢ ( ( Fun ℵ ∧ 𝐴 ∈ V ) → ( ℵ ↾ 𝐴 ) ∈ V )
6	3 4 5	sylancr	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ↾ 𝐴 ) ∈ V )
7		limelon	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → 𝐴 ∈ On )
8		onss	⊢ ( 𝐴 ∈ On → 𝐴 ⊆ On )
9	7 8	syl	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → 𝐴 ⊆ On )
10		fnssres	⊢ ( ( ℵ Fn On ∧ 𝐴 ⊆ On ) → ( ℵ ↾ 𝐴 ) Fn 𝐴 )
11	1 9 10	sylancr	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ↾ 𝐴 ) Fn 𝐴 )
12		fvres	⊢ ( 𝑦 ∈ 𝐴 → ( ( ℵ ↾ 𝐴 ) ‘ 𝑦 ) = ( ℵ ‘ 𝑦 ) )
13	12	adantl	⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ 𝐴 ) → ( ( ℵ ↾ 𝐴 ) ‘ 𝑦 ) = ( ℵ ‘ 𝑦 ) )
14		alephord2i	⊢ ( 𝐴 ∈ On → ( 𝑦 ∈ 𝐴 → ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) ) )
15	14	imp	⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ 𝐴 ) → ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) )
16	13 15	eqeltrd	⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ∈ 𝐴 ) → ( ( ℵ ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) )
17	7 16	sylan	⊢ ( ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( ℵ ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) )
18	17	ralrimiva	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ∀ 𝑦 ∈ 𝐴 ( ( ℵ ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) )
19		fnfvrnss	⊢ ( ( ( ℵ ↾ 𝐴 ) Fn 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 ( ( ℵ ↾ 𝐴 ) ‘ 𝑦 ) ∈ ( ℵ ‘ 𝐴 ) ) → ran ( ℵ ↾ 𝐴 ) ⊆ ( ℵ ‘ 𝐴 ) )
20	11 18 19	syl2anc	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ran ( ℵ ↾ 𝐴 ) ⊆ ( ℵ ‘ 𝐴 ) )
21		df-f	⊢ ( ( ℵ ↾ 𝐴 ) : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ↔ ( ( ℵ ↾ 𝐴 ) Fn 𝐴 ∧ ran ( ℵ ↾ 𝐴 ) ⊆ ( ℵ ‘ 𝐴 ) ) )
22	11 20 21	sylanbrc	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ↾ 𝐴 ) : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) )
23		alephsmo	⊢ Smo ℵ
24		fndm	⊢ ( ℵ Fn On → dom ℵ = On )
25	1 24	ax-mp	⊢ dom ℵ = On
26	7 25	eleqtrrdi	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → 𝐴 ∈ dom ℵ )
27		smores	⊢ ( ( Smo ℵ ∧ 𝐴 ∈ dom ℵ ) → Smo ( ℵ ↾ 𝐴 ) )
28	23 26 27	sylancr	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → Smo ( ℵ ↾ 𝐴 ) )
29		alephlim	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ‘ 𝐴 ) = ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) )
30	29	eleq2d	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( 𝑥 ∈ ( ℵ ‘ 𝐴 ) ↔ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ) )
31		eliun	⊢ ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ ( ℵ ‘ 𝑦 ) )
32		alephon	⊢ ( ℵ ‘ 𝑦 ) ∈ On
33	32	onelssi	⊢ ( 𝑥 ∈ ( ℵ ‘ 𝑦 ) → 𝑥 ⊆ ( ℵ ‘ 𝑦 ) )
34	33	reximi	⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ ( ℵ ‘ 𝑦 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) )
35	31 34	sylbi	⊢ ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) )
36	30 35	syl6bi	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( 𝑥 ∈ ( ℵ ‘ 𝐴 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) )
37	36	ralrimiv	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) )
38		feq1	⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ↔ ( ℵ ↾ 𝐴 ) : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ) )
39		smoeq	⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( Smo 𝑓 ↔ Smo ( ℵ ↾ 𝐴 ) ) )
40		fveq1	⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( 𝑓 ‘ 𝑦 ) = ( ( ℵ ↾ 𝐴 ) ‘ 𝑦 ) )
41	40 12	sylan9eq	⊢ ( ( 𝑓 = ( ℵ ↾ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑦 ) = ( ℵ ‘ 𝑦 ) )
42	41	sseq2d	⊢ ( ( 𝑓 = ( ℵ ↾ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ↔ 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) )
43	42	rexbidva	⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) )
44	43	ralbidv	⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) )
45	38 39 44	3anbi123d	⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ↔ ( ( ℵ ↾ 𝐴 ) : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo ( ℵ ↾ 𝐴 ) ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) ) )
46	45	spcegv	⊢ ( ( ℵ ↾ 𝐴 ) ∈ V → ( ( ( ℵ ↾ 𝐴 ) : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo ( ℵ ↾ 𝐴 ) ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ) )
47	46	imp	⊢ ( ( ( ℵ ↾ 𝐴 ) ∈ V ∧ ( ( ℵ ↾ 𝐴 ) : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo ( ℵ ↾ 𝐴 ) ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) )
48	6 22 28 37 47	syl13anc	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) )
49		alephon	⊢ ( ℵ ‘ 𝐴 ) ∈ On
50		cfcof	⊢ ( ( ( ℵ ‘ 𝐴 ) ∈ On ∧ 𝐴 ∈ On ) → ( ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) ) )
51	49 7 50	sylancr	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) ) )
52	48 51	mpd	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) )
53	52	expcom	⊢ ( Lim 𝐴 → ( 𝐴 ∈ V → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) ) )
54		cf0	⊢ ( cf ‘ ∅ ) = ∅
55		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( ℵ ‘ 𝐴 ) = ∅ )
56	55	fveq2d	⊢ ( ¬ 𝐴 ∈ V → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ ∅ ) )
57		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( cf ‘ 𝐴 ) = ∅ )
58	54 56 57	3eqtr4a	⊢ ( ¬ 𝐴 ∈ V → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) )
59	53 58	pm2.61d1	⊢ ( Lim 𝐴 → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) )