Theorem rankidn

Description: A relationship between the rank function and the cumulative hierarchy of sets function R1 . (Contributed by Mario Carneiro, 17-Nov-2014)

	Ref	Expression
Assertion	rankidn	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ¬ 𝐴 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( rank ‘ 𝐴 ) = ( rank ‘ 𝐴 )
2		rankr1c	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( ( rank ‘ 𝐴 ) = ( rank ‘ 𝐴 ) ↔ ( ¬ 𝐴 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ∧ 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ) ) )
3	1 2	mpbii	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( ¬ 𝐴 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ∧ 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) ) )
4	3	simpld	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ¬ 𝐴 ∈ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )