Metamath Proof Explorer

Theorem bndrank

Description: Any class whose elements have bounded rank is a set. Proposition 9.19 of TakeutiZaring p. 80. (Contributed by NM, 13-Oct-2003)

Ref Expression
Assertion bndrank 
|- ( E. x e. On A. y e. A ( rank ` y ) C_ x -> A e. _V )

Proof

Step Hyp Ref Expression
1 rankon 
 |-  ( rank ` y ) e. On
2 1 onordi 
 |-  Ord ( rank ` y )
3 eloni 
 |-  ( x e. On -> Ord x )
4 ordsucsssuc 
 |-  ( ( Ord ( rank ` y ) /\ Ord x ) -> ( ( rank ` y ) C_ x <-> suc ( rank ` y ) C_ suc x ) )
5 2 3 4 sylancr 
 |-  ( x e. On -> ( ( rank ` y ) C_ x <-> suc ( rank ` y ) C_ suc x ) )
6 1 onsuci 
 |-  suc ( rank ` y ) e. On
7 suceloni 
 |-  ( x e. On -> suc x e. On )
8 r1ord3 
 |-  ( ( suc ( rank ` y ) e. On /\ suc x e. On ) -> ( suc ( rank ` y ) C_ suc x -> ( R1 ` suc ( rank ` y ) ) C_ ( R1 ` suc x ) ) )
9 6 7 8 sylancr 
 |-  ( x e. On -> ( suc ( rank ` y ) C_ suc x -> ( R1 ` suc ( rank ` y ) ) C_ ( R1 ` suc x ) ) )
10 5 9 sylbid 
 |-  ( x e. On -> ( ( rank ` y ) C_ x -> ( R1 ` suc ( rank ` y ) ) C_ ( R1 ` suc x ) ) )
11 vex 
 |-  y e. _V
12 11 rankid 
 |-  y e. ( R1 ` suc ( rank ` y ) )
13 ssel 
 |-  ( ( R1 ` suc ( rank ` y ) ) C_ ( R1 ` suc x ) -> ( y e. ( R1 ` suc ( rank ` y ) ) -> y e. ( R1 ` suc x ) ) )
14 10 12 13 syl6mpi 
 |-  ( x e. On -> ( ( rank ` y ) C_ x -> y e. ( R1 ` suc x ) ) )
15 14 ralimdv 
 |-  ( x e. On -> ( A. y e. A ( rank ` y ) C_ x -> A. y e. A y e. ( R1 ` suc x ) ) )
16 dfss3 
 |-  ( A C_ ( R1 ` suc x ) <-> A. y e. A y e. ( R1 ` suc x ) )
17 fvex 
 |-  ( R1 ` suc x ) e. _V
18 17 ssex 
 |-  ( A C_ ( R1 ` suc x ) -> A e. _V )
19 16 18 sylbir 
 |-  ( A. y e. A y e. ( R1 ` suc x ) -> A e. _V )
20 15 19 syl6 
 |-  ( x e. On -> ( A. y e. A ( rank ` y ) C_ x -> A e. _V ) )
21 20 rexlimiv 
 |-  ( E. x e. On A. y e. A ( rank ` y ) C_ x -> A e. _V )