ssrankr1

Description: A relationship between an ordinal number less than or equal to a rank, and the cumulative hierarchy of sets R1 . Proposition 9.15(3) of TakeutiZaring p. 79. (Contributed by NM, 8-Oct-2003) (Revised by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Hypothesis	rankid.1	$⊢ A \in V$
	Assertion	ssrankr1	$⊢ B \in On \to (B \subseteq rank (A) \leftrightarrow \neg A \in R_{1} (B))$

Proof

Step	Hyp	Ref	Expression
1		rankid.1	$⊢ A \in V$
2		unir1	$⊢ ⋃ R_{1} [On] = V$
3	1 2	eleqtrri	$⊢ A \in ⋃ R_{1} [On]$
4		r1fnon	$⊢ R_{1} Fn On$
5		fndm	$⊢ R_{1} Fn On \to dom R_{1} = On$
6	4 5	ax-mp	$⊢ dom R_{1} = On$
7	6	eleq2i	$⊢ B \in dom R_{1} \leftrightarrow B \in On$
8	7	biimpri	$⊢ B \in On \to B \in dom R_{1}$
9		rankr1clem	$⊢ (A \in ⋃ R_{1} [On] \land B \in dom R_{1}) \to (\neg A \in R_{1} (B) \leftrightarrow B \subseteq rank (A))$
10	3 8 9	sylancr	$⊢ B \in On \to (\neg A \in R_{1} (B) \leftrightarrow B \subseteq rank (A))$
11	10	bicomd	$⊢ B \in On \to (B \subseteq rank (A) \leftrightarrow \neg A \in R_{1} (B))$

Metamath Proof Explorer

Theorem ssrankr1

Proof