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 dfss2f
 |-  ( 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 )