rankvalb

Description: Value of the rank function. Definition 9.14 of TakeutiZaring p. 79 (proved as a theorem from our definition). This variant of rankval does not use Regularity, and so requires the assumption that A is in the range of R1 . (Contributed by NM, 11-Oct-2003) (Revised by Mario Carneiro, 10-Sep-2013)

		Ref	Expression
	Assertion	rankvalb	$⊢ A \in ⋃ R_{1} [On] \to rank (A) = ⋂ \{x \in On \| A \in R_{1} (suc x)\}$

Proof

Step	Hyp	Ref	Expression
1		df-rank	$⊢ rank = (y \in V ⟼ ⋂ \{x \in On \| y \in R_{1} (suc x)\})$
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		elex	$⊢ A \in ⋃ R_{1} [On] \to A \in V$
6		rankwflemb	$⊢ A \in ⋃ R_{1} [On] \leftrightarrow \exists x \in On A \in R_{1} (suc x)$
7		intexrab	$⊢ \exists x \in On A \in R_{1} (suc x) \leftrightarrow ⋂ \{x \in On \| A \in R_{1} (suc x)\} \in V$
8	6 7	sylbb	$⊢ A \in ⋃ R_{1} [On] \to ⋂ \{x \in On \| A \in R_{1} (suc x)\} \in V$
9	1 4 5 8	fvmptd3	$⊢ A \in ⋃ R_{1} [On] \to rank (A) = ⋂ \{x \in On \| A \in R_{1} (suc x)\}$

Metamath Proof Explorer

Theorem rankvalb

Proof