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

Metamath Proof Explorer

Theorem ranksnb

Description: The rank of a singleton. Theorem 15.17(v) of Monk1 p. 112. (Contributed by Mario Carneiro, 10-Jun-2013)

Ref Expression
Assertion ranksnb ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ { 𝐴 } ) = suc ( rank ‘ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 fveq2 ⊢ ( 𝑦 = 𝐴 → ( rank ‘ 𝑦 ) = ( rank ‘ 𝐴 ) )
2 1 eleq1d ⊢ ( 𝑦 = 𝐴 → ( ( rank ‘ 𝑦 ) ∈ 𝑥 ↔ ( rank ‘ 𝐴 ) ∈ 𝑥 ) )
3 2 ralsng ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( ∀ 𝑦 ∈ { 𝐴 } ( rank ‘ 𝑦 ) ∈ 𝑥 ↔ ( rank ‘ 𝐴 ) ∈ 𝑥 ) )
4 3 rabbidv ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ { 𝐴 } ( rank ‘ 𝑦 ) ∈ 𝑥 } = { 𝑥 ∈ On ∣ ( rank ‘ 𝐴 ) ∈ 𝑥 } )
5 4 inteqd ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ { 𝐴 } ( rank ‘ 𝑦 ) ∈ 𝑥 } = ∩ { 𝑥 ∈ On ∣ ( rank ‘ 𝐴 ) ∈ 𝑥 } )
6 snwf ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) )
7 rankval3b ⊢ ( { 𝐴 } ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ { 𝐴 } ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ { 𝐴 } ( rank ‘ 𝑦 ) ∈ 𝑥 } )
8 6 7 syl ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ { 𝐴 } ) = ∩ { 𝑥 ∈ On ∣ ∀ 𝑦 ∈ { 𝐴 } ( rank ‘ 𝑦 ) ∈ 𝑥 } )
9 rankon ⊢ ( rank ‘ 𝐴 ) ∈ On
10 onsucmin ⊢ ( ( rank ‘ 𝐴 ) ∈ On → suc ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ ( rank ‘ 𝐴 ) ∈ 𝑥 } )
11 9 10 mp1i ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → suc ( rank ‘ 𝐴 ) = ∩ { 𝑥 ∈ On ∣ ( rank ‘ 𝐴 ) ∈ 𝑥 } )
12 5 8 11 3eqtr4d ⊢ ( 𝐴 ∈ ∪ ( 𝑅1 “ On ) → ( rank ‘ { 𝐴 } ) = suc ( rank ‘ 𝐴 ) )