Theorem rankvaln

Description: Value of the rank function at a non-well-founded set. (The antecedent is always false under Foundation, by unir1 , unless A is a proper class.) (Contributed by Mario Carneiro, 22-Mar-2013) (Revised by Mario Carneiro, 10-Sep-2013)

	Ref	Expression
Assertion	rankvaln	|- ( -. A e. U. ( R1 " On ) -> ( rank ` A ) = (/) )

Proof

Step	Hyp	Ref	Expression
1		rankf	|- rank : U. ( R1 " On ) --> On
2	1	fdmi	|- dom rank = U. ( R1 " On )
3	2	eleq2i	|- ( A e. dom rank <-> A e. U. ( R1 " On ) )
4		ndmfv	|- ( -. A e. dom rank -> ( rank ` A ) = (/) )
5	3 4	sylnbir	|- ( -. A e. U. ( R1 " On ) -> ( rank ` A ) = (/) )