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 e. _V
Assertion	rankr1a	|- ( B e. On -> ( A e. ( R1 ` B ) <-> ( rank ` A ) e. B ) )

Proof

Step	Hyp	Ref	Expression
1		rankid.1	|- A e. _V
2	1	ssrankr1	|- ( B e. On -> ( B C_ ( rank ` A ) <-> -. A e. ( R1 ` B ) ) )
3		rankon	|- ( rank ` A ) e. On
4		ontri1	|- ( ( B e. On /\ ( rank ` A ) e. On ) -> ( B C_ ( rank ` A ) <-> -. ( rank ` A ) e. B ) )
5	3 4	mpan2	|- ( B e. On -> ( B C_ ( rank ` A ) <-> -. ( rank ` A ) e. B ) )
6	2 5	bitr3d	|- ( B e. On -> ( -. A e. ( R1 ` B ) <-> -. ( rank ` A ) e. B ) )
7	6	con4bid	|- ( B e. On -> ( A e. ( R1 ` B ) <-> ( rank ` A ) e. B ) )