rankval2

Description: Value of an alternate definition of the rank function. Definition of BellMachover p. 478. (Contributed by NM, 8-Oct-2003)

		Ref	Expression
	Assertion	rankval2	$⊢ A \in B \to rank (A) = ⋂ \{x \in On \| A \subseteq R_{1} (x)\}$

Step	Hyp	Ref	Expression
1		rankvalg	$⊢ A \in B \to rank (A) = ⋂ \{x \in On \| A \in R_{1} (suc x)\}$
2		r1suc	$⊢ x \in On \to R_{1} (suc x) = 𝒫 R_{1} (x)$
3	2	eleq2d	$⊢ x \in On \to (A \in R_{1} (suc x) \leftrightarrow A \in 𝒫 R_{1} (x))$
4		fvex	$⊢ R_{1} (x) \in V$
5	4	elpw2	$⊢ A \in 𝒫 R_{1} (x) \leftrightarrow A \subseteq R_{1} (x)$
6	3 5	bitrdi	$⊢ x \in On \to (A \in R_{1} (suc x) \leftrightarrow A \subseteq R_{1} (x))$
7	6	rabbiia	$⊢ \{x \in On \| A \in R_{1} (suc x)\} = \{x \in On \| A \subseteq R_{1} (x)\}$
8	7	inteqi	$⊢ ⋂ \{x \in On \| A \in R_{1} (suc x)\} = ⋂ \{x \in On \| A \subseteq R_{1} (x)\}$
9	1 8	eqtrdi	$⊢ A \in B \to rank (A) = ⋂ \{x \in On \| A \subseteq R_{1} (x)\}$

Metamath Proof Explorer