Metamath Proof Explorer


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 syl5ibr ( 𝑥 ∈ On → ( ∀ 𝑦𝑥 𝑦 ∈ ( ℵ ‘ 𝑥 ) → 𝑥 ⊆ ( ℵ ‘ 𝑥 ) ) )
22 14 21 syld ( 𝑥 ∈ On → ( ∀ 𝑦𝑥 𝑦 ⊆ ( ℵ ‘ 𝑦 ) → 𝑥 ⊆ ( ℵ ‘ 𝑥 ) ) )
23 3 6 22 tfis3 ( 𝐴 ∈ On → 𝐴 ⊆ ( ℵ ‘ 𝐴 ) )