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	$⊢ \neg A \in ⋃ R_{1} [On] \to rank (A) = \emptyset$

Proof

Step	Hyp	Ref	Expression
1		rankf	$⊢ rank : ⋃ R_{1} [On] ⟶ On$
2	1	fdmi	$⊢ dom rank = ⋃ R_{1} [On]$
3	2	eleq2i	$⊢ A \in dom rank \leftrightarrow A \in ⋃ R_{1} [On]$
4		ndmfv	$⊢ \neg A \in dom rank \to rank (A) = \emptyset$
5	3 4	sylnbir	$⊢ \neg A \in ⋃ R_{1} [On] \to rank (A) = \emptyset$