Metamath Proof Explorer

Theorem rankuni2b

Description: The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of TakeutiZaring p. 79. (Contributed by Mario Carneiro, 8-Jun-2013)

Ref Expression
Assertion rankuni2b 
|- ( A e. U. ( R1 " On ) -> ( rank ` U. A ) = U_ x e. A ( rank ` x ) )

Proof

Step Hyp Ref Expression
1 uniwf 
 |-  ( A e. U. ( R1 " On ) <-> U. A e. U. ( R1 " On ) )
2 rankval3b 
 |-  ( U. A e. U. ( R1 " On ) -> ( rank ` U. A ) = |^| { z e. On | A. y e. U. A ( rank ` y ) e. z } )
3 1 2 sylbi 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` U. A ) = |^| { z e. On | A. y e. U. A ( rank ` y ) e. z } )
4 eleq2 
 |-  ( z = U_ x e. A ( rank ` x ) -> ( ( rank ` y ) e. z <-> ( rank ` y ) e. U_ x e. A ( rank ` x ) ) )
5 4 ralbidv 
 |-  ( z = U_ x e. A ( rank ` x ) -> ( A. y e. U. A ( rank ` y ) e. z <-> A. y e. U. A ( rank ` y ) e. U_ x e. A ( rank ` x ) ) )
6 iuneq1 
 |-  ( y = A -> U_ x e. y ( rank ` x ) = U_ x e. A ( rank ` x ) )
7 6 eleq1d 
 |-  ( y = A -> ( U_ x e. y ( rank ` x ) e. On <-> U_ x e. A ( rank ` x ) e. On ) )
8 vex 
 |-  y e. _V
9 rankon 
 |-  ( rank ` x ) e. On
10 9 rgenw 
 |-  A. x e. y ( rank ` x ) e. On
11 iunon 
 |-  ( ( y e. _V /\ A. x e. y ( rank ` x ) e. On ) -> U_ x e. y ( rank ` x ) e. On )
12 8 10 11 mp2an 
 |-  U_ x e. y ( rank ` x ) e. On
13 7 12 vtoclg 
 |-  ( A e. U. ( R1 " On ) -> U_ x e. A ( rank ` x ) e. On )
14 eluni2 
 |-  ( y e. U. A <-> E. x e. A y e. x )
15 nfv 
 |-  F/ x A e. U. ( R1 " On )
16 nfiu1 
 |-  F/_ x U_ x e. A ( rank ` x )
17 16 nfel2 
 |-  F/ x ( rank ` y ) e. U_ x e. A ( rank ` x )
18 r1elssi 
 |-  ( A e. U. ( R1 " On ) -> A C_ U. ( R1 " On ) )
19 18 sseld 
 |-  ( A e. U. ( R1 " On ) -> ( x e. A -> x e. U. ( R1 " On ) ) )
20 rankelb 
 |-  ( x e. U. ( R1 " On ) -> ( y e. x -> ( rank ` y ) e. ( rank ` x ) ) )
21 19 20 syl6 
 |-  ( A e. U. ( R1 " On ) -> ( x e. A -> ( y e. x -> ( rank ` y ) e. ( rank ` x ) ) ) )
22 ssiun2 
 |-  ( x e. A -> ( rank ` x ) C_ U_ x e. A ( rank ` x ) )
23 22 sseld 
 |-  ( x e. A -> ( ( rank ` y ) e. ( rank ` x ) -> ( rank ` y ) e. U_ x e. A ( rank ` x ) ) )
24 23 a1i 
 |-  ( A e. U. ( R1 " On ) -> ( x e. A -> ( ( rank ` y ) e. ( rank ` x ) -> ( rank ` y ) e. U_ x e. A ( rank ` x ) ) ) )
25 21 24 syldd 
 |-  ( A e. U. ( R1 " On ) -> ( x e. A -> ( y e. x -> ( rank ` y ) e. U_ x e. A ( rank ` x ) ) ) )
26 15 17 25 rexlimd 
 |-  ( A e. U. ( R1 " On ) -> ( E. x e. A y e. x -> ( rank ` y ) e. U_ x e. A ( rank ` x ) ) )
27 14 26 syl5bi 
 |-  ( A e. U. ( R1 " On ) -> ( y e. U. A -> ( rank ` y ) e. U_ x e. A ( rank ` x ) ) )
28 27 ralrimiv 
 |-  ( A e. U. ( R1 " On ) -> A. y e. U. A ( rank ` y ) e. U_ x e. A ( rank ` x ) )
29 5 13 28 elrabd 
 |-  ( A e. U. ( R1 " On ) -> U_ x e. A ( rank ` x ) e. { z e. On | A. y e. U. A ( rank ` y ) e. z } )
30 intss1 
 |-  ( U_ x e. A ( rank ` x ) e. { z e. On | A. y e. U. A ( rank ` y ) e. z } -> |^| { z e. On | A. y e. U. A ( rank ` y ) e. z } C_ U_ x e. A ( rank ` x ) )
31 29 30 syl 
 |-  ( A e. U. ( R1 " On ) -> |^| { z e. On | A. y e. U. A ( rank ` y ) e. z } C_ U_ x e. A ( rank ` x ) )
32 3 31 eqsstrd 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` U. A ) C_ U_ x e. A ( rank ` x ) )
33 1 biimpi 
 |-  ( A e. U. ( R1 " On ) -> U. A e. U. ( R1 " On ) )
34 elssuni 
 |-  ( x e. A -> x C_ U. A )
35 rankssb 
 |-  ( U. A e. U. ( R1 " On ) -> ( x C_ U. A -> ( rank ` x ) C_ ( rank ` U. A ) ) )
36 33 34 35 syl2im 
 |-  ( A e. U. ( R1 " On ) -> ( x e. A -> ( rank ` x ) C_ ( rank ` U. A ) ) )
37 36 ralrimiv 
 |-  ( A e. U. ( R1 " On ) -> A. x e. A ( rank ` x ) C_ ( rank ` U. A ) )
38 iunss 
 |-  ( U_ x e. A ( rank ` x ) C_ ( rank ` U. A ) <-> A. x e. A ( rank ` x ) C_ ( rank ` U. A ) )
39 37 38 sylibr 
 |-  ( A e. U. ( R1 " On ) -> U_ x e. A ( rank ` x ) C_ ( rank ` U. A ) )
40 32 39 eqssd 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` U. A ) = U_ x e. A ( rank ` x ) )