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

Metamath Proof Explorer

Theorem rankidb

Description: Identity law for the rank function. (Contributed by NM, 3-Oct-2003) (Revised by Mario Carneiro, 22-Mar-2013)

Ref Expression
Assertion rankidb ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 rankwflemb ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) ↔ ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) )
2 nfcv ⊢ Ⅎ 𝑥 𝑅1
3 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) }
4 3 nfint ⊢ Ⅎ 𝑥 ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) }
5 4 nfsuc ⊢ Ⅎ 𝑥 suc ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) }
6 2 5 nffv ⊢ Ⅎ 𝑥 ( 𝑅1 ‘ suc ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )
7 6 nfel2 ⊢ Ⅎ 𝑥 𝐴 ∈ ( 𝑅1 ‘ suc ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )
8 suceq ⊢ ( 𝑥 = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } → suc 𝑥 = suc ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )
9 8 fveq2d ⊢ ( 𝑥 = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } → ( 𝑅1 ‘ suc 𝑥 ) = ( 𝑅1 ‘ suc ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ) )
10 9 eleq2d ⊢ ( 𝑥 = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } → ( 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) ↔ 𝐴 ∈ ( 𝑅1 ‘ suc ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ) ) )
11 7 10 onminsb ⊢ ( ∃ 𝑥 ∈ On 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) → 𝐴 ∈ ( 𝑅1 ‘ suc ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ) )
12 1 11 sylbi ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ( 𝑅1 ‘ suc ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ) )
13 rankvalb ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )
14 suceq ⊢ ( ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } → suc ( rank ‘ 𝐴 ) = suc ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )
15 13 14 syl ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → suc ( rank ‘ 𝐴 ) = suc ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } )
16 15 fveq2d ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) = ( 𝑅1 ‘ suc ∩ { 𝑥 ∈ On ∣ 𝐴 ∈ ( 𝑅1 ‘ suc 𝑥 ) } ) )
17 12 16 eleqtrrd ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → 𝐴 ∈ ( 𝑅1 ‘ suc ( rank ‘ 𝐴 ) ) )