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 
|- ( A e. U. ( R1 " On ) -> ( rank ` { A } ) = suc ( rank ` A ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( y = A -> ( rank ` y ) = ( rank ` A ) )
2 1 eleq1d 
 |-  ( y = A -> ( ( rank ` y ) e. x <-> ( rank ` A ) e. x ) )
3 2 ralsng 
 |-  ( A e. U. ( R1 " On ) -> ( A. y e. { A } ( rank ` y ) e. x <-> ( rank ` A ) e. x ) )
4 3 rabbidv 
 |-  ( A e. U. ( R1 " On ) -> { x e. On | A. y e. { A } ( rank ` y ) e. x } = { x e. On | ( rank ` A ) e. x } )
5 4 inteqd 
 |-  ( A e. U. ( R1 " On ) -> |^| { x e. On | A. y e. { A } ( rank ` y ) e. x } = |^| { x e. On | ( rank ` A ) e. x } )
6 snwf 
 |-  ( A e. U. ( R1 " On ) -> { A } e. U. ( R1 " On ) )
7 rankval3b 
 |-  ( { A } e. U. ( R1 " On ) -> ( rank ` { A } ) = |^| { x e. On | A. y e. { A } ( rank ` y ) e. x } )
8 6 7 syl 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` { A } ) = |^| { x e. On | A. y e. { A } ( rank ` y ) e. x } )
9 rankon 
 |-  ( rank ` A ) e. On
10 onsucmin 
 |-  ( ( rank ` A ) e. On -> suc ( rank ` A ) = |^| { x e. On | ( rank ` A ) e. x } )
11 9 10 mp1i 
 |-  ( A e. U. ( R1 " On ) -> suc ( rank ` A ) = |^| { x e. On | ( rank ` A ) e. x } )
12 5 8 11 3eqtr4d 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` { A } ) = suc ( rank ` A ) )