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	⊢ 𝐴 ∈ V
Assertion	rankr1a	⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		rankid.1	⊢ 𝐴 ∈ V
2	1	ssrankr1	⊢ ( 𝐵 ∈ On → ( 𝐵 ⊆ ( rank ‘ 𝐴 ) ↔ ¬ 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ) )
3		rankon	⊢ ( rank ‘ 𝐴 ) ∈ On
4		ontri1	⊢ ( ( 𝐵 ∈ On ∧ ( rank ‘ 𝐴 ) ∈ On ) → ( 𝐵 ⊆ ( rank ‘ 𝐴 ) ↔ ¬ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
5	3 4	mpan2	⊢ ( 𝐵 ∈ On → ( 𝐵 ⊆ ( rank ‘ 𝐴 ) ↔ ¬ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
6	2 5	bitr3d	⊢ ( 𝐵 ∈ On → ( ¬ 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ¬ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )
7	6	con4bid	⊢ ( 𝐵 ∈ On → ( 𝐴 ∈ ( 𝑅1 ‘ 𝐵 ) ↔ ( rank ‘ 𝐴 ) ∈ 𝐵 ) )