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 ) )