rankvalg

Description: Value of the rank function. Definition 9.14 of TakeutiZaring p. 79 (proved as a theorem from our definition). This variant of rankval expresses the class existence requirement as an antecedent instead of a hypothesis. (Contributed by NM, 5-Oct-2003)

		Ref	Expression
	Assertion	rankvalg	$⊢ A \in V \to rank (A) = ⋂ \{x \in On \| A \in R_{1} (suc x)\}$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$⊢ y = A \to rank (y) = rank (A)$
2		eleq1	$⊢ y = A \to (y \in R_{1} (suc x) \leftrightarrow A \in R_{1} (suc x))$
3	2	rabbidv	$⊢ y = A \to \{x \in On \| y \in R_{1} (suc x)\} = \{x \in On \| A \in R_{1} (suc x)\}$
4	3	inteqd	$⊢ y = A \to ⋂ \{x \in On \| y \in R_{1} (suc x)\} = ⋂ \{x \in On \| A \in R_{1} (suc x)\}$
5	1 4	eqeq12d	$⊢ y = A \to (rank (y) = ⋂ \{x \in On \| y \in R_{1} (suc x)\} \leftrightarrow rank (A) = ⋂ \{x \in On \| A \in R_{1} (suc x)\})$
6		vex	$⊢ y \in V$
7	6	rankval	$⊢ rank (y) = ⋂ \{x \in On \| y \in R_{1} (suc x)\}$
8	5 7	vtoclg	$⊢ A \in V \to rank (A) = ⋂ \{x \in On \| A \in R_{1} (suc x)\}$

Metamath Proof Explorer

Theorem rankvalg

Proof