Theorem rankr1a

Description: A relationship between rank and R1 , clearly equivalent to ssrankr1 and friends through trichotomy, but in Raph's opinion considerably more intuitive. See rankr1b for the subset version. (Contributed by Raph Levien, 29-May-2004)

	Ref	Expression
Hypothesis	rankid.1	$$⊢A\in \mathrm{V}$$
Assertion	rankr1a	$$⊢B\in \mathrm{On}\to \left(A\in R_1\left(B\right)\leftrightarrow \mathrm{rank}\left(A\right)\in B\right)$$

Proof

Step	Hyp	Ref	Expression
1		rankid.1	$$⊢A\in \mathrm{V}$$
2	1	ssrankr1	$$⊢B\in \mathrm{On}\to \left(B\subseteq \mathrm{rank}\left(A\right)\leftrightarrow \neg A\in R_1\left(B\right)\right)$$
3		rankon	$$⊢\mathrm{rank}\left(A\right)\in \mathrm{On}$$
4		ontri1	$$⊢\left(B\in \mathrm{On}\wedge \mathrm{rank}\left(A\right)\in \mathrm{On}\right)\to \left(B\subseteq \mathrm{rank}\left(A\right)\leftrightarrow \neg \mathrm{rank}\left(A\right)\in B\right)$$
5	3 4	mpan2	$$⊢B\in \mathrm{On}\to \left(B\subseteq \mathrm{rank}\left(A\right)\leftrightarrow \neg \mathrm{rank}\left(A\right)\in B\right)$$
6	2 5	bitr3d	$$⊢B\in \mathrm{On}\to \left(\neg A\in R_1\left(B\right)\leftrightarrow \neg \mathrm{rank}\left(A\right)\in B\right)$$
7	6	con4bid	$$⊢B\in \mathrm{On}\to \left(A\in R_1\left(B\right)\leftrightarrow \mathrm{rank}\left(A\right)\in B\right)$$