Theorem alephle

Description: The argument of the aleph function is less than or equal to its value. Exercise 2 of TakeutiZaring p. 91. (Later, in alephfp2 , we will that equality can sometimes hold.) (Contributed by NM, 9-Nov-2003) (Proof shortened by Mario Carneiro, 22-Feb-2013)

	Ref	Expression
Assertion	alephle	⊢ ( 𝐴 ∈ On → 𝐴 ⊆ ( ℵ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
2		fveq2	⊢ ( 𝑥 = 𝑦 → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ 𝑦 ) )
3	1 2	sseq12d	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ ( ℵ ‘ 𝑥 ) ↔ 𝑦 ⊆ ( ℵ ‘ 𝑦 ) ) )
4		id	⊢ ( 𝑥 = 𝐴 → 𝑥 = 𝐴 )
5		fveq2	⊢ ( 𝑥 = 𝐴 → ( ℵ ‘ 𝑥 ) = ( ℵ ‘ 𝐴 ) )
6	4 5	sseq12d	⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ ( ℵ ‘ 𝑥 ) ↔ 𝐴 ⊆ ( ℵ ‘ 𝐴 ) ) )
7		alephord2i	⊢ ( 𝑥 ∈ On → ( 𝑦 ∈ 𝑥 → ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑥 ) ) )
8	7	imp	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑥 ) )
9		onelon	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
10		alephon	⊢ ( ℵ ‘ 𝑥 ) ∈ On
11		ontr2	⊢ ( ( 𝑦 ∈ On ∧ ( ℵ ‘ 𝑥 ) ∈ On ) → ( ( 𝑦 ⊆ ( ℵ ‘ 𝑦 ) ∧ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑥 ) ) → 𝑦 ∈ ( ℵ ‘ 𝑥 ) ) )
12	9 10 11	sylancl	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑦 ⊆ ( ℵ ‘ 𝑦 ) ∧ ( ℵ ‘ 𝑦 ) ∈ ( ℵ ‘ 𝑥 ) ) → 𝑦 ∈ ( ℵ ‘ 𝑥 ) ) )
13	8 12	mpan2d	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → ( 𝑦 ⊆ ( ℵ ‘ 𝑦 ) → 𝑦 ∈ ( ℵ ‘ 𝑥 ) ) )
14	13	ralimdva	⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ ( ℵ ‘ 𝑦 ) → ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ( ℵ ‘ 𝑥 ) ) )
15	10	onirri	⊢ ¬ ( ℵ ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑥 )
16		eleq1	⊢ ( 𝑦 = ( ℵ ‘ 𝑥 ) → ( 𝑦 ∈ ( ℵ ‘ 𝑥 ) ↔ ( ℵ ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑥 ) ) )
17	16	rspccv	⊢ ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ( ℵ ‘ 𝑥 ) → ( ( ℵ ‘ 𝑥 ) ∈ 𝑥 → ( ℵ ‘ 𝑥 ) ∈ ( ℵ ‘ 𝑥 ) ) )
18	15 17	mtoi	⊢ ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ( ℵ ‘ 𝑥 ) → ¬ ( ℵ ‘ 𝑥 ) ∈ 𝑥 )
19		ontri1	⊢ ( ( 𝑥 ∈ On ∧ ( ℵ ‘ 𝑥 ) ∈ On ) → ( 𝑥 ⊆ ( ℵ ‘ 𝑥 ) ↔ ¬ ( ℵ ‘ 𝑥 ) ∈ 𝑥 ) )
20	10 19	mpan2	⊢ ( 𝑥 ∈ On → ( 𝑥 ⊆ ( ℵ ‘ 𝑥 ) ↔ ¬ ( ℵ ‘ 𝑥 ) ∈ 𝑥 ) )
21	18 20	imbitrrid	⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 𝑦 ∈ ( ℵ ‘ 𝑥 ) → 𝑥 ⊆ ( ℵ ‘ 𝑥 ) ) )
22	14 21	syld	⊢ ( 𝑥 ∈ On → ( ∀ 𝑦 ∈ 𝑥 𝑦 ⊆ ( ℵ ‘ 𝑦 ) → 𝑥 ⊆ ( ℵ ‘ 𝑥 ) ) )
23	3 6 22	tfis3	⊢ ( 𝐴 ∈ On → 𝐴 ⊆ ( ℵ ‘ 𝐴 ) )