This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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