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

Metamath Proof Explorer

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 ) = (/) )