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 
|- ( A e. On -> A C_ ( aleph ` A ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( x = y -> x = y )
2 fveq2 
 |-  ( x = y -> ( aleph ` x ) = ( aleph ` y ) )
3 1 2 sseq12d 
 |-  ( x = y -> ( x C_ ( aleph ` x ) <-> y C_ ( aleph ` y ) ) )
4 id 
 |-  ( x = A -> x = A )
5 fveq2 
 |-  ( x = A -> ( aleph ` x ) = ( aleph ` A ) )
6 4 5 sseq12d 
 |-  ( x = A -> ( x C_ ( aleph ` x ) <-> A C_ ( aleph ` A ) ) )
7 alephord2i 
 |-  ( x e. On -> ( y e. x -> ( aleph ` y ) e. ( aleph ` x ) ) )
8 7 imp 
 |-  ( ( x e. On /\ y e. x ) -> ( aleph ` y ) e. ( aleph ` x ) )
9 onelon 
 |-  ( ( x e. On /\ y e. x ) -> y e. On )
10 alephon 
 |-  ( aleph ` x ) e. On
11 ontr2 
 |-  ( ( y e. On /\ ( aleph ` x ) e. On ) -> ( ( y C_ ( aleph ` y ) /\ ( aleph ` y ) e. ( aleph ` x ) ) -> y e. ( aleph ` x ) ) )
12 9 10 11 sylancl 
 |-  ( ( x e. On /\ y e. x ) -> ( ( y C_ ( aleph ` y ) /\ ( aleph ` y ) e. ( aleph ` x ) ) -> y e. ( aleph ` x ) ) )
13 8 12 mpan2d 
 |-  ( ( x e. On /\ y e. x ) -> ( y C_ ( aleph ` y ) -> y e. ( aleph ` x ) ) )
14 13 ralimdva 
 |-  ( x e. On -> ( A. y e. x y C_ ( aleph ` y ) -> A. y e. x y e. ( aleph ` x ) ) )
15 10 onirri 
 |-  -. ( aleph ` x ) e. ( aleph ` x )
16 eleq1 
 |-  ( y = ( aleph ` x ) -> ( y e. ( aleph ` x ) <-> ( aleph ` x ) e. ( aleph ` x ) ) )
17 16 rspccv 
 |-  ( A. y e. x y e. ( aleph ` x ) -> ( ( aleph ` x ) e. x -> ( aleph ` x ) e. ( aleph ` x ) ) )
18 15 17 mtoi 
 |-  ( A. y e. x y e. ( aleph ` x ) -> -. ( aleph ` x ) e. x )
19 ontri1 
 |-  ( ( x e. On /\ ( aleph ` x ) e. On ) -> ( x C_ ( aleph ` x ) <-> -. ( aleph ` x ) e. x ) )
20 10 19 mpan2 
 |-  ( x e. On -> ( x C_ ( aleph ` x ) <-> -. ( aleph ` x ) e. x ) )
21 18 20 syl5ibr 
 |-  ( x e. On -> ( A. y e. x y e. ( aleph ` x ) -> x C_ ( aleph ` x ) ) )
22 14 21 syld 
 |-  ( x e. On -> ( A. y e. x y C_ ( aleph ` y ) -> x C_ ( aleph ` x ) ) )
23 3 6 22 tfis3 
 |-  ( A e. On -> A C_ ( aleph ` A ) )