Theorem rankvalb

Description: Value of the rank function. Definition 9.14 of TakeutiZaring p. 79 (proved as a theorem from our definition). This variant of rankval does not use Regularity, and so requires the assumption that A is in the range of R1 . (Contributed by NM, 11-Oct-2003) (Revised by Mario Carneiro, 10-Sep-2013)

	Ref	Expression
Assertion	rankvalb	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )

Proof

Step	Hyp	Ref	Expression
1		df-rank	⊢ rank = ( 𝑦 ∈ V ↦ ∩ { 𝑥 ∈ On ∣ 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )
2		eleq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) ↔ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ) )
3	2	rabbidv	⊢ ( 𝑦 = 𝐴 → { 𝑥 ∈ On ∣ 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) } = { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )
4	3	inteqd	⊢ ( 𝑦 = 𝐴 → ∩ { 𝑥 ∈ On ∣ 𝑦 ∈ ( 𝑅1 ‘ suc 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )
5		elex	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ V )
6		rankwflemb	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
7		intexrab	⊢ ( ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ↔ ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ∈ V )
8	6 7	sylbb	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ∈ V )
9	1 4 5 8	fvmptd3	⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )