Theorem rankval2

Description: Value of an alternate definition of the rank function. Definition of BellMachover p. 478. (Contributed by NM, 8-Oct-2003)

	Ref	Expression
Assertion	rankval2	⊢ ( 𝐴 ∈ 𝐵 → ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) } )

Proof

Step	Hyp	Ref	Expression
1		rankvalg	⊢ ( 𝐴 ∈ 𝐵 → ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )
2		r1suc	⊢ ( 𝑥 ∈ On → ( 𝑅1 ‘ suc 𝑥 ) = 𝒫 ( 𝑅1 ‘ 𝑥 ) )
3	2	eleq2d	⊢ ( 𝑥 ∈ On → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ↔ 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) ) )
4		fvex	⊢ ( 𝑅1 ‘ 𝑥 ) ∈ V
5	4	elpw2	⊢ ( 𝐴 ∈ 𝒫 ( 𝑅1 ‘ 𝑥 ) ↔ 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) )
6	3 5	bitrdi	⊢ ( 𝑥 ∈ On → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ↔ 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) ) )
7	6	rabbiia	⊢ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } = { 𝑥 ∈ On ∣ 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) }
8	7	inteqi	⊢ ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } = ∩ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) }
9	1 8	eqtrdi	⊢ ( 𝐴 ∈ 𝐵 → ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ⊆ ( 𝑅1 ‘ 𝑥 ) } )