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