Metamath Proof Explorer

Theorem rankval3b

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, 17-Nov-2014)

Ref Expression
Assertion rankval3b 
|- ( A e. U. ( R1 " On ) -> ( rank ` A ) = |^| { x e. On | A. y e. A ( rank ` y ) e. x } )

Proof

Step Hyp Ref Expression
1 rankon 
 |-  ( rank ` A ) e. On
2 simprl 
 |-  ( ( A e. U. ( R1 " On ) /\ ( x e. On /\ A. y e. A ( rank ` y ) e. x ) ) -> x e. On )
3 ontri1 
 |-  ( ( ( rank ` A ) e. On /\ x e. On ) -> ( ( rank ` A ) C_ x <-> -. x e. ( rank ` A ) ) )
4 1 2 3 sylancr 
 |-  ( ( A e. U. ( R1 " On ) /\ ( x e. On /\ A. y e. A ( rank ` y ) e. x ) ) -> ( ( rank ` A ) C_ x <-> -. x e. ( rank ` A ) ) )
5 4 con2bid 
 |-  ( ( A e. U. ( R1 " On ) /\ ( x e. On /\ A. y e. A ( rank ` y ) e. x ) ) -> ( x e. ( rank ` A ) <-> -. ( rank ` A ) C_ x ) )
6 r1elssi 
 |-  ( A e. U. ( R1 " On ) -> A C_ U. ( R1 " On ) )
7 6 adantr 
 |-  ( ( A e. U. ( R1 " On ) /\ x e. ( rank ` A ) ) -> A C_ U. ( R1 " On ) )
8 7 sselda 
 |-  ( ( ( A e. U. ( R1 " On ) /\ x e. ( rank ` A ) ) /\ y e. A ) -> y e. U. ( R1 " On ) )
9 rankdmr1 
 |-  ( rank ` A ) e. dom R1
10 r1dmlim 
 |-  Lim dom R1
11 limord 
 |-  ( Lim dom R1 -> Ord dom R1 )
12 ordtr1 
 |-  ( Ord dom R1 -> ( ( x e. ( rank ` A ) /\ ( rank ` A ) e. dom R1 ) -> x e. dom R1 ) )
13 10 11 12 mp2b 
 |-  ( ( x e. ( rank ` A ) /\ ( rank ` A ) e. dom R1 ) -> x e. dom R1 )
14 9 13 mpan2 
 |-  ( x e. ( rank ` A ) -> x e. dom R1 )
15 14 ad2antlr 
 |-  ( ( ( A e. U. ( R1 " On ) /\ x e. ( rank ` A ) ) /\ y e. A ) -> x e. dom R1 )
16 rankr1ag 
 |-  ( ( y e. U. ( R1 " On ) /\ x e. dom R1 ) -> ( y e. ( R1 ` x ) <-> ( rank ` y ) e. x ) )
17 8 15 16 syl2anc 
 |-  ( ( ( A e. U. ( R1 " On ) /\ x e. ( rank ` A ) ) /\ y e. A ) -> ( y e. ( R1 ` x ) <-> ( rank ` y ) e. x ) )
18 17 ralbidva 
 |-  ( ( A e. U. ( R1 " On ) /\ x e. ( rank ` A ) ) -> ( A. y e. A y e. ( R1 ` x ) <-> A. y e. A ( rank ` y ) e. x ) )
19 18 biimpar 
 |-  ( ( ( A e. U. ( R1 " On ) /\ x e. ( rank ` A ) ) /\ A. y e. A ( rank ` y ) e. x ) -> A. y e. A y e. ( R1 ` x ) )
20 19 an32s 
 |-  ( ( ( A e. U. ( R1 " On ) /\ A. y e. A ( rank ` y ) e. x ) /\ x e. ( rank ` A ) ) -> A. y e. A y e. ( R1 ` x ) )
21 dfss3 
 |-  ( A C_ ( R1 ` x ) <-> A. y e. A y e. ( R1 ` x ) )
22 20 21 sylibr 
 |-  ( ( ( A e. U. ( R1 " On ) /\ A. y e. A ( rank ` y ) e. x ) /\ x e. ( rank ` A ) ) -> A C_ ( R1 ` x ) )
23 simpll 
 |-  ( ( ( A e. U. ( R1 " On ) /\ A. y e. A ( rank ` y ) e. x ) /\ x e. ( rank ` A ) ) -> A e. U. ( R1 " On ) )
24 14 adantl 
 |-  ( ( ( A e. U. ( R1 " On ) /\ A. y e. A ( rank ` y ) e. x ) /\ x e. ( rank ` A ) ) -> x e. dom R1 )
25 rankr1bg 
 |-  ( ( A e. U. ( R1 " On ) /\ x e. dom R1 ) -> ( A C_ ( R1 ` x ) <-> ( rank ` A ) C_ x ) )
26 23 24 25 syl2anc 
 |-  ( ( ( A e. U. ( R1 " On ) /\ A. y e. A ( rank ` y ) e. x ) /\ x e. ( rank ` A ) ) -> ( A C_ ( R1 ` x ) <-> ( rank ` A ) C_ x ) )
27 22 26 mpbid 
 |-  ( ( ( A e. U. ( R1 " On ) /\ A. y e. A ( rank ` y ) e. x ) /\ x e. ( rank ` A ) ) -> ( rank ` A ) C_ x )
28 27 ex 
 |-  ( ( A e. U. ( R1 " On ) /\ A. y e. A ( rank ` y ) e. x ) -> ( x e. ( rank ` A ) -> ( rank ` A ) C_ x ) )
29 28 adantrl 
 |-  ( ( A e. U. ( R1 " On ) /\ ( x e. On /\ A. y e. A ( rank ` y ) e. x ) ) -> ( x e. ( rank ` A ) -> ( rank ` A ) C_ x ) )
30 5 29 sylbird 
 |-  ( ( A e. U. ( R1 " On ) /\ ( x e. On /\ A. y e. A ( rank ` y ) e. x ) ) -> ( -. ( rank ` A ) C_ x -> ( rank ` A ) C_ x ) )
31 30 pm2.18d 
 |-  ( ( A e. U. ( R1 " On ) /\ ( x e. On /\ A. y e. A ( rank ` y ) e. x ) ) -> ( rank ` A ) C_ x )
32 31 ex 
 |-  ( A e. U. ( R1 " On ) -> ( ( x e. On /\ A. y e. A ( rank ` y ) e. x ) -> ( rank ` A ) C_ x ) )
33 32 alrimiv 
 |-  ( A e. U. ( R1 " On ) -> A. x ( ( x e. On /\ A. y e. A ( rank ` y ) e. x ) -> ( rank ` A ) C_ x ) )
34 ssintab 
 |-  ( ( rank ` A ) C_ |^| { x | ( x e. On /\ A. y e. A ( rank ` y ) e. x ) } <-> A. x ( ( x e. On /\ A. y e. A ( rank ` y ) e. x ) -> ( rank ` A ) C_ x ) )
35 33 34 sylibr 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) C_ |^| { x | ( x e. On /\ A. y e. A ( rank ` y ) e. x ) } )
36 df-rab 
 |-  { x e. On | A. y e. A ( rank ` y ) e. x } = { x | ( x e. On /\ A. y e. A ( rank ` y ) e. x ) }
37 36 inteqi 
 |-  |^| { x e. On | A. y e. A ( rank ` y ) e. x } = |^| { x | ( x e. On /\ A. y e. A ( rank ` y ) e. x ) }
38 35 37 sseqtrrdi 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) C_ |^| { x e. On | A. y e. A ( rank ` y ) e. x } )
39 rankelb 
 |-  ( A e. U. ( R1 " On ) -> ( y e. A -> ( rank ` y ) e. ( rank ` A ) ) )
40 39 ralrimiv 
 |-  ( A e. U. ( R1 " On ) -> A. y e. A ( rank ` y ) e. ( rank ` A ) )
41 eleq2 
 |-  ( x = ( rank ` A ) -> ( ( rank ` y ) e. x <-> ( rank ` y ) e. ( rank ` A ) ) )
42 41 ralbidv 
 |-  ( x = ( rank ` A ) -> ( A. y e. A ( rank ` y ) e. x <-> A. y e. A ( rank ` y ) e. ( rank ` A ) ) )
43 42 onintss 
 |-  ( ( rank ` A ) e. On -> ( A. y e. A ( rank ` y ) e. ( rank ` A ) -> |^| { x e. On | A. y e. A ( rank ` y ) e. x } C_ ( rank ` A ) ) )
44 1 40 43 mpsyl 
 |-  ( A e. U. ( R1 " On ) -> |^| { x e. On | A. y e. A ( rank ` y ) e. x } C_ ( rank ` A ) )
45 38 44 eqssd 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) = |^| { x e. On | A. y e. A ( rank ` y ) e. x } )