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

Metamath Proof Explorer

Theorem unbndrank

Description: The elements of a proper class have unbounded rank. Exercise 2 of TakeutiZaring p. 80. (Contributed by NM, 13-Oct-2003)

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

Proof

Step Hyp Ref Expression
1 rankon 
 |-  ( rank ` y ) e. On
2 ontri1 
 |-  ( ( ( rank ` y ) e. On /\ x e. On ) -> ( ( rank ` y ) C_ x <-> -. x e. ( rank ` y ) ) )
3 1 2 mpan 
 |-  ( x e. On -> ( ( rank ` y ) C_ x <-> -. x e. ( rank ` y ) ) )
4 3 ralbidv 
 |-  ( x e. On -> ( A. y e. A ( rank ` y ) C_ x <-> A. y e. A -. x e. ( rank ` y ) ) )
5 ralnex 
 |-  ( A. y e. A -. x e. ( rank ` y ) <-> -. E. y e. A x e. ( rank ` y ) )
6 4 5 bitrdi 
 |-  ( x e. On -> ( A. y e. A ( rank ` y ) C_ x <-> -. E. y e. A x e. ( rank ` y ) ) )
7 6 rexbiia 
 |-  ( E. x e. On A. y e. A ( rank ` y ) C_ x <-> E. x e. On -. E. y e. A x e. ( rank ` y ) )
8 rexnal 
 |-  ( E. x e. On -. E. y e. A x e. ( rank ` y ) <-> -. A. x e. On E. y e. A x e. ( rank ` y ) )
9 7 8 bitri 
 |-  ( E. x e. On A. y e. A ( rank ` y ) C_ x <-> -. A. x e. On E. y e. A x e. ( rank ` y ) )
10 bndrank 
 |-  ( E. x e. On A. y e. A ( rank ` y ) C_ x -> A e. _V )
11 9 10 sylbir 
 |-  ( -. A. x e. On E. y e. A x e. ( rank ` y ) -> A e. _V )
12 11 con1i 
 |-  ( -. A e. _V -> A. x e. On E. y e. A x e. ( rank ` y ) )