This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
11 10 simpri 
 |-  Lim dom R1
12 limord 
 |-  ( Lim dom R1 -> Ord dom R1 )
13 ordtr1 
 |-  ( Ord dom R1 -> ( ( x e. ( rank ` A ) /\ ( rank ` A ) e. dom R1 ) -> x e. dom R1 ) )
14 11 12 13 mp2b 
 |-  ( ( x e. ( rank ` A ) /\ ( rank ` A ) e. dom R1 ) -> x e. dom R1 )
15 9 14 mpan2 
 |-  ( x e. ( rank ` A ) -> x e. dom R1 )
16 15 ad2antlr 
 |-  ( ( ( A e. U. ( R1 " On ) /\ x e. ( rank ` A ) ) /\ y e. A ) -> x e. dom R1 )
17 rankr1ag 
 |-  ( ( y e. U. ( R1 " On ) /\ x e. dom R1 ) -> ( y e. ( R1 ` x ) <-> ( rank ` y ) e. x ) )
18 8 16 17 syl2anc 
 |-  ( ( ( A e. U. ( R1 " On ) /\ x e. ( rank ` A ) ) /\ y e. A ) -> ( y e. ( R1 ` x ) <-> ( rank ` y ) e. x ) )
19 18 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 ) )
20 19 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 ) )
21 20 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 ) )
22 dfss3 
 |-  ( A C_ ( R1 ` x ) <-> A. y e. A y e. ( R1 ` x ) )
23 21 22 sylibr 
 |-  ( ( ( A e. U. ( R1 " On ) /\ A. y e. A ( rank ` y ) e. x ) /\ x e. ( rank ` A ) ) -> A C_ ( R1 ` x ) )
24 simpll 
 |-  ( ( ( A e. U. ( R1 " On ) /\ A. y e. A ( rank ` y ) e. x ) /\ x e. ( rank ` A ) ) -> A e. U. ( R1 " On ) )
25 15 adantl 
 |-  ( ( ( A e. U. ( R1 " On ) /\ A. y e. A ( rank ` y ) e. x ) /\ x e. ( rank ` A ) ) -> x e. dom R1 )
26 rankr1bg 
 |-  ( ( A e. U. ( R1 " On ) /\ x e. dom R1 ) -> ( A C_ ( R1 ` x ) <-> ( rank ` A ) C_ x ) )
27 24 25 26 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 ) )
28 23 27 mpbid 
 |-  ( ( ( A e. U. ( R1 " On ) /\ A. y e. A ( rank ` y ) e. x ) /\ x e. ( rank ` A ) ) -> ( rank ` A ) C_ x )
29 28 ex 
 |-  ( ( A e. U. ( R1 " On ) /\ A. y e. A ( rank ` y ) e. x ) -> ( x e. ( rank ` A ) -> ( rank ` A ) C_ x ) )
30 29 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 ) )
31 5 30 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 ) )
32 31 pm2.18d 
 |-  ( ( A e. U. ( R1 " On ) /\ ( x e. On /\ A. y e. A ( rank ` y ) e. x ) ) -> ( rank ` A ) C_ x )
33 32 ex 
 |-  ( A e. U. ( R1 " On ) -> ( ( x e. On /\ A. y e. A ( rank ` y ) e. x ) -> ( rank ` A ) C_ x ) )
34 33 alrimiv 
 |-  ( A e. U. ( R1 " On ) -> A. x ( ( x e. On /\ A. y e. A ( rank ` y ) e. x ) -> ( rank ` A ) C_ x ) )
35 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 ) )
36 34 35 sylibr 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) C_ |^| { x | ( x e. On /\ A. y e. A ( rank ` y ) e. x ) } )
37 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 ) }
38 37 inteqi 
 |-  |^| { x e. On | A. y e. A ( rank ` y ) e. x } = |^| { x | ( x e. On /\ A. y e. A ( rank ` y ) e. x ) }
39 36 38 sseqtrrdi 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) C_ |^| { x e. On | A. y e. A ( rank ` y ) e. x } )
40 rankelb 
 |-  ( A e. U. ( R1 " On ) -> ( y e. A -> ( rank ` y ) e. ( rank ` A ) ) )
41 40 ralrimiv 
 |-  ( A e. U. ( R1 " On ) -> A. y e. A ( rank ` y ) e. ( rank ` A ) )
42 eleq2 
 |-  ( x = ( rank ` A ) -> ( ( rank ` y ) e. x <-> ( rank ` y ) e. ( rank ` A ) ) )
43 42 ralbidv 
 |-  ( x = ( rank ` A ) -> ( A. y e. A ( rank ` y ) e. x <-> A. y e. A ( rank ` y ) e. ( rank ` A ) ) )
44 43 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 ) ) )
45 1 41 44 mpsyl 
 |-  ( A e. U. ( R1 " On ) -> |^| { x e. On | A. y e. A ( rank ` y ) e. x } C_ ( rank ` A ) )
46 39 45 eqssd 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) = |^| { x e. On | A. y e. A ( rank ` y ) e. x } )