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

Metamath Proof Explorer

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 ‘ 𝑥 ) } )