This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rankr1

Description: A relationship between the rank function and the cumulative hierarchy of sets function R1 . Proposition 9.15(2) of TakeutiZaring p. 79. (Contributed by NM, 6-Oct-2003) (Proof shortened by Mario Carneiro, 17-Nov-2014)

		Ref	Expression
	Hypothesis	rankid.1	⊢ 𝐴 ∈ V
	Assertion	rankr1	⊢ ( 𝐵 = ( rank ‘ 𝐴 ) ↔ ( ¬ 𝐴 ∈ ( 𝑅₁ ‘ 𝐵 ) ∧ 𝐴 ∈ ( 𝑅₁ ‘ suc 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rankid.1	⊢ 𝐴 ∈ V
2		rankr1g	⊢ ( 𝐴 ∈ V → ( 𝐵 = ( rank ‘ 𝐴 ) ↔ ( ¬ 𝐴 ∈ ( 𝑅₁ ‘ 𝐵 ) ∧ 𝐴 ∈ ( 𝑅₁ ‘ suc 𝐵 ) ) ) )
3	1 2	ax-mp	⊢ ( 𝐵 = ( rank ‘ 𝐴 ) ↔ ( ¬ 𝐴 ∈ ( 𝑅₁ ‘ 𝐵 ) ∧ 𝐴 ∈ ( 𝑅₁ ‘ suc 𝐵 ) ) )