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	1	fndmi	⊢ dom ℵ = On
25	7 24	eleqtrrdi	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → 𝐴 ∈ dom ℵ )
26		smores	⊢ ( ( Smo ℵ ∧ 𝐴 ∈ dom ℵ ) → Smo ( ℵ ↾ 𝐴 ) )
27	23 25 26	sylancr	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → Smo ( ℵ ↾ 𝐴 ) )
28		alephlim	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ℵ ‘ 𝐴 ) = ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) )
29	28	eleq2d	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( 𝑥 ∈ ( ℵ ‘ 𝐴 ) ↔ 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ) )
30		eliun	⊢ ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ∈ ( ℵ ‘ 𝑦 ) )
31		alephon	⊢ ( ℵ ‘ 𝑦 ) ∈ On
32	31	onelssi	⊢ ( 𝑥 ∈ ( ℵ ‘ 𝑦 ) → 𝑥 ⊆ ( ℵ ‘ 𝑦 ) )
33	32	reximi	⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 ∈ ( ℵ ‘ 𝑦 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) )
34	30 33	sylbi	⊢ ( 𝑥 ∈ ∪ 𝑦 ∈ 𝐴 ( ℵ ‘ 𝑦 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) )
35	29 34	biimtrdi	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( 𝑥 ∈ ( ℵ ‘ 𝐴 ) → ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) )
36	35	ralrimiv	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) )
37		feq1	⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ↔ ( ℵ ↾ 𝐴 ) : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ) )
38		smoeq	⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( Smo 𝑓 ↔ Smo ( ℵ ↾ 𝐴 ) ) )
39		fveq1	⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( 𝑓 ‘ 𝑦 ) = ( ( ℵ ↾ 𝐴 ) ‘ 𝑦 ) )
40	39 12	sylan9eq	⊢ ( ( 𝑓 = ( ℵ ↾ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑦 ) = ( ℵ ‘ 𝑦 ) )
41	40	sseq2d	⊢ ( ( 𝑓 = ( ℵ ↾ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ↔ 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) )
42	41	rexbidva	⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ↔ ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) )
43	42	ralbidv	⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ↔ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) )
44	37 38 43	3anbi123d	⊢ ( 𝑓 = ( ℵ ↾ 𝐴 ) → ( ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ↔ ( ( ℵ ↾ 𝐴 ) : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo ( ℵ ↾ 𝐴 ) ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) ) )
45	44	spcegv	⊢ ( ( ℵ ↾ 𝐴 ) ∈ V → ( ( ( ℵ ↾ 𝐴 ) : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo ( ℵ ↾ 𝐴 ) ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) ) )
46	45	imp	⊢ ( ( ( ℵ ↾ 𝐴 ) ∈ V ∧ ( ( ℵ ↾ 𝐴 ) : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo ( ℵ ↾ 𝐴 ) ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( ℵ ‘ 𝑦 ) ) ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) )
47	6 22 27 36 46	syl13anc	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) )
48		alephon	⊢ ( ℵ ‘ 𝐴 ) ∈ On
49		cfcof	⊢ ( ( ( ℵ ‘ 𝐴 ) ∈ On ∧ 𝐴 ∈ On ) → ( ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) ) )
50	48 7 49	sylancr	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( ∃ 𝑓 ( 𝑓 : 𝐴 ⟶ ( ℵ ‘ 𝐴 ) ∧ Smo 𝑓 ∧ ∀ 𝑥 ∈ ( ℵ ‘ 𝐴 ) ∃ 𝑦 ∈ 𝐴 𝑥 ⊆ ( 𝑓 ‘ 𝑦 ) ) → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) ) )
51	47 50	mpd	⊢ ( ( 𝐴 ∈ V ∧ Lim 𝐴 ) → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) )
52	51	expcom	⊢ ( Lim 𝐴 → ( 𝐴 ∈ V → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) ) )
53		cf0	⊢ ( cf ‘ ∅ ) = ∅
54		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( ℵ ‘ 𝐴 ) = ∅ )
55	54	fveq2d	⊢ ( ¬ 𝐴 ∈ V → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ ∅ ) )
56		fvprc	⊢ ( ¬ 𝐴 ∈ V → ( cf ‘ 𝐴 ) = ∅ )
57	53 55 56	3eqtr4a	⊢ ( ¬ 𝐴 ∈ V → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) )
58	52 57	pm2.61d1	⊢ ( Lim 𝐴 → ( cf ‘ ( ℵ ‘ 𝐴 ) ) = ( cf ‘ 𝐴 ) )