Metamath Proof Explorer

Theorem rankval4

Description: The rank of a set is the supremum of the successors of the ranks of its members. Exercise 9.1 of Jech p. 72. Also a special case of Theorem 7V(b) of Enderton p. 204. (Contributed by NM, 12-Oct-2003)

Ref Expression
Hypothesis rankr1b.1 
|- A e. _V
Assertion rankval4 
|- ( rank ` A ) = U_ x e. A suc ( rank ` x )

Proof

Step Hyp Ref Expression
1 rankr1b.1 
 |-  A e. _V
2 nfcv 
 |-  F/_ x A
3 nfcv 
 |-  F/_ x R1
4 nfiu1 
 |-  F/_ x U_ x e. A suc ( rank ` x )
5 3 4 nffv 
 |-  F/_ x ( R1 ` U_ x e. A suc ( rank ` x ) )
6 2 5 dfssf 
 |-  ( A C_ ( R1 ` U_ x e. A suc ( rank ` x ) ) <-> A. x ( x e. A -> x e. ( R1 ` U_ x e. A suc ( rank ` x ) ) ) )
7 vex 
 |-  x e. _V
8 7 rankid 
 |-  x e. ( R1 ` suc ( rank ` x ) )
9 ssiun2 
 |-  ( x e. A -> suc ( rank ` x ) C_ U_ x e. A suc ( rank ` x ) )
10 rankon 
 |-  ( rank ` x ) e. On
11 10 onsuci 
 |-  suc ( rank ` x ) e. On
12 11 rgenw 
 |-  A. x e. A suc ( rank ` x ) e. On
13 iunon 
 |-  ( ( A e. _V /\ A. x e. A suc ( rank ` x ) e. On ) -> U_ x e. A suc ( rank ` x ) e. On )
14 1 12 13 mp2an 
 |-  U_ x e. A suc ( rank ` x ) e. On
15 r1ord3 
 |-  ( ( suc ( rank ` x ) e. On /\ U_ x e. A suc ( rank ` x ) e. On ) -> ( suc ( rank ` x ) C_ U_ x e. A suc ( rank ` x ) -> ( R1 ` suc ( rank ` x ) ) C_ ( R1 ` U_ x e. A suc ( rank ` x ) ) ) )
16 11 14 15 mp2an 
 |-  ( suc ( rank ` x ) C_ U_ x e. A suc ( rank ` x ) -> ( R1 ` suc ( rank ` x ) ) C_ ( R1 ` U_ x e. A suc ( rank ` x ) ) )
17 9 16 syl 
 |-  ( x e. A -> ( R1 ` suc ( rank ` x ) ) C_ ( R1 ` U_ x e. A suc ( rank ` x ) ) )
18 17 sseld 
 |-  ( x e. A -> ( x e. ( R1 ` suc ( rank ` x ) ) -> x e. ( R1 ` U_ x e. A suc ( rank ` x ) ) ) )
19 8 18 mpi 
 |-  ( x e. A -> x e. ( R1 ` U_ x e. A suc ( rank ` x ) ) )
20 6 19 mpgbir 
 |-  A C_ ( R1 ` U_ x e. A suc ( rank ` x ) )
21 fvex 
 |-  ( R1 ` U_ x e. A suc ( rank ` x ) ) e. _V
22 21 rankss 
 |-  ( A C_ ( R1 ` U_ x e. A suc ( rank ` x ) ) -> ( rank ` A ) C_ ( rank ` ( R1 ` U_ x e. A suc ( rank ` x ) ) ) )
23 20 22 ax-mp 
 |-  ( rank ` A ) C_ ( rank ` ( R1 ` U_ x e. A suc ( rank ` x ) ) )
24 r1ord3 
 |-  ( ( U_ x e. A suc ( rank ` x ) e. On /\ y e. On ) -> ( U_ x e. A suc ( rank ` x ) C_ y -> ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) ) )
25 14 24 mpan 
 |-  ( y e. On -> ( U_ x e. A suc ( rank ` x ) C_ y -> ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) ) )
26 25 ss2rabi 
 |-  { y e. On | U_ x e. A suc ( rank ` x ) C_ y } C_ { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) }
27 intss 
 |-  ( { y e. On | U_ x e. A suc ( rank ` x ) C_ y } C_ { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) } -> |^| { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) } C_ |^| { y e. On | U_ x e. A suc ( rank ` x ) C_ y } )
28 26 27 ax-mp 
 |-  |^| { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) } C_ |^| { y e. On | U_ x e. A suc ( rank ` x ) C_ y }
29 rankval2 
 |-  ( ( R1 ` U_ x e. A suc ( rank ` x ) ) e. _V -> ( rank ` ( R1 ` U_ x e. A suc ( rank ` x ) ) ) = |^| { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) } )
30 21 29 ax-mp 
 |-  ( rank ` ( R1 ` U_ x e. A suc ( rank ` x ) ) ) = |^| { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) }
31 intmin 
 |-  ( U_ x e. A suc ( rank ` x ) e. On -> |^| { y e. On | U_ x e. A suc ( rank ` x ) C_ y } = U_ x e. A suc ( rank ` x ) )
32 14 31 ax-mp 
 |-  |^| { y e. On | U_ x e. A suc ( rank ` x ) C_ y } = U_ x e. A suc ( rank ` x )
33 32 eqcomi 
 |-  U_ x e. A suc ( rank ` x ) = |^| { y e. On | U_ x e. A suc ( rank ` x ) C_ y }
34 28 30 33 3sstr4i 
 |-  ( rank ` ( R1 ` U_ x e. A suc ( rank ` x ) ) ) C_ U_ x e. A suc ( rank ` x )
35 23 34 sstri 
 |-  ( rank ` A ) C_ U_ x e. A suc ( rank ` x )
36 iunss 
 |-  ( U_ x e. A suc ( rank ` x ) C_ ( rank ` A ) <-> A. x e. A suc ( rank ` x ) C_ ( rank ` A ) )
37 1 rankel 
 |-  ( x e. A -> ( rank ` x ) e. ( rank ` A ) )
38 rankon 
 |-  ( rank ` A ) e. On
39 10 38 onsucssi 
 |-  ( ( rank ` x ) e. ( rank ` A ) <-> suc ( rank ` x ) C_ ( rank ` A ) )
40 37 39 sylib 
 |-  ( x e. A -> suc ( rank ` x ) C_ ( rank ` A ) )
41 36 40 mprgbir 
 |-  U_ x e. A suc ( rank ` x ) C_ ( rank ` A )
42 35 41 eqssi 
 |-  ( rank ` A ) = U_ x e. A suc ( rank ` x )