MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tcrank Unicode version

Theorem tcrank 7742
Description: This theorem expresses two different facts from the two subset implications in this equality. In the forward direction, it says that the transitive closure has members of every rank below  A. Stated another way, to construct a set at a given rank, you have to climb the entire hierarchy of ordinals below  ( rank `  A ), constructing at least one set at each level in order to move up the ranks. In the reverse direction, it says that every member of  ( TC `  A ) has a rank below the rank of  A, since intuitively it contains only the members of  A and the members of those and so on, but nothing "bigger" than  A. (Contributed by Mario Carneiro, 23-Jun-2013.)
Assertion
Ref Expression
tcrank  |-  ( A  e.  U. ( R1
" On )  -> 
( rank `  A )  =  ( rank " ( TC `  A ) ) )

Proof of Theorem tcrank
Dummy variables  x  y  z  w  u are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rankwflemb 7653 . . 3  |-  ( A  e.  U. ( R1
" On )  <->  E. y  e.  On  A  e.  ( R1 `  suc  y
) )
2 suceloni 4734 . . . . 5  |-  ( y  e.  On  ->  suc  y  e.  On )
3 fveq2 5669 . . . . . . . 8  |-  ( x  =  y  ->  ( R1 `  x )  =  ( R1 `  y
) )
43raleqdv 2854 . . . . . . 7  |-  ( x  =  y  ->  ( A. z  e.  ( R1 `  x ) (
rank `  z )  C_  ( rank " ( TC `  z ) )  <->  A. z  e.  ( R1 `  y ) (
rank `  z )  C_  ( rank " ( TC `  z ) ) ) )
5 fveq2 5669 . . . . . . . . 9  |-  ( z  =  u  ->  ( rank `  z )  =  ( rank `  u
) )
6 fveq2 5669 . . . . . . . . . 10  |-  ( z  =  u  ->  ( TC `  z )  =  ( TC `  u
) )
76imaeq2d 5144 . . . . . . . . 9  |-  ( z  =  u  ->  ( rank " ( TC `  z ) )  =  ( rank " ( TC `  u ) ) )
85, 7sseq12d 3321 . . . . . . . 8  |-  ( z  =  u  ->  (
( rank `  z )  C_  ( rank " ( TC `  z ) )  <-> 
( rank `  u )  C_  ( rank " ( TC `  u ) ) ) )
98cbvralv 2876 . . . . . . 7  |-  ( A. z  e.  ( R1 `  y ) ( rank `  z )  C_  ( rank " ( TC `  z ) )  <->  A. u  e.  ( R1 `  y
) ( rank `  u
)  C_  ( rank " ( TC `  u
) ) )
104, 9syl6bb 253 . . . . . 6  |-  ( x  =  y  ->  ( A. z  e.  ( R1 `  x ) (
rank `  z )  C_  ( rank " ( TC `  z ) )  <->  A. u  e.  ( R1 `  y ) (
rank `  u )  C_  ( rank " ( TC `  u ) ) ) )
11 fveq2 5669 . . . . . . 7  |-  ( x  =  suc  y  -> 
( R1 `  x
)  =  ( R1
`  suc  y )
)
1211raleqdv 2854 . . . . . 6  |-  ( x  =  suc  y  -> 
( A. z  e.  ( R1 `  x
) ( rank `  z
)  C_  ( rank " ( TC `  z
) )  <->  A. z  e.  ( R1 `  suc  y ) ( rank `  z )  C_  ( rank " ( TC `  z ) ) ) )
13 simpr 448 . . . . . . . . . . . 12  |-  ( ( ( x  e.  On  /\ 
A. y  e.  x  A. u  e.  ( R1 `  y ) (
rank `  u )  C_  ( rank " ( TC `  u ) ) )  /\  ( z  e.  ( R1 `  x )  /\  w  e.  ( rank `  z
) ) )  -> 
( z  e.  ( R1 `  x )  /\  w  e.  (
rank `  z )
) )
14 simprl 733 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  On  /\ 
A. y  e.  x  A. u  e.  ( R1 `  y ) (
rank `  u )  C_  ( rank " ( TC `  u ) ) )  /\  ( z  e.  ( R1 `  x )  /\  w  e.  ( rank `  z
) ) )  -> 
z  e.  ( R1
`  x ) )
15 simplr 732 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  On  /\ 
A. y  e.  x  A. u  e.  ( R1 `  y ) (
rank `  u )  C_  ( rank " ( TC `  u ) ) )  /\  ( z  e.  ( R1 `  x )  /\  w  e.  ( rank `  z
) ) )  ->  A. y  e.  x  A. u  e.  ( R1 `  y ) (
rank `  u )  C_  ( rank " ( TC `  u ) ) )
16 rankr1ai 7658 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( R1 `  x )  ->  ( rank `  z )  e.  x )
17 fveq2 5669 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( rank `  z
)  ->  ( R1 `  y )  =  ( R1 `  ( rank `  z ) ) )
1817raleqdv 2854 . . . . . . . . . . . . . . . . 17  |-  ( y  =  ( rank `  z
)  ->  ( A. u  e.  ( R1 `  y ) ( rank `  u )  C_  ( rank " ( TC `  u ) )  <->  A. u  e.  ( R1 `  ( rank `  z ) ) ( rank `  u
)  C_  ( rank " ( TC `  u
) ) ) )
1918rspcv 2992 . . . . . . . . . . . . . . . 16  |-  ( (
rank `  z )  e.  x  ->  ( A. y  e.  x  A. u  e.  ( R1 `  y ) ( rank `  u )  C_  ( rank " ( TC `  u ) )  ->  A. u  e.  ( R1 `  ( rank `  z
) ) ( rank `  u )  C_  ( rank " ( TC `  u ) ) ) )
2016, 19syl 16 . . . . . . . . . . . . . . 15  |-  ( z  e.  ( R1 `  x )  ->  ( A. y  e.  x  A. u  e.  ( R1 `  y ) (
rank `  u )  C_  ( rank " ( TC `  u ) )  ->  A. u  e.  ( R1 `  ( rank `  z ) ) (
rank `  u )  C_  ( rank " ( TC `  u ) ) ) )
21 r1elwf 7656 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( R1 `  x )  ->  z  e.  U. ( R1 " On ) )
22 r1rankidb 7664 . . . . . . . . . . . . . . . 16  |-  ( z  e.  U. ( R1
" On )  -> 
z  C_  ( R1 `  ( rank `  z
) ) )
23 ssralv 3351 . . . . . . . . . . . . . . . 16  |-  ( z 
C_  ( R1 `  ( rank `  z )
)  ->  ( A. u  e.  ( R1 `  ( rank `  z
) ) ( rank `  u )  C_  ( rank " ( TC `  u ) )  ->  A. u  e.  z 
( rank `  u )  C_  ( rank " ( TC `  u ) ) ) )
2421, 22, 233syl 19 . . . . . . . . . . . . . . 15  |-  ( z  e.  ( R1 `  x )  ->  ( A. u  e.  ( R1 `  ( rank `  z
) ) ( rank `  u )  C_  ( rank " ( TC `  u ) )  ->  A. u  e.  z 
( rank `  u )  C_  ( rank " ( TC `  u ) ) ) )
2520, 24syld 42 . . . . . . . . . . . . . 14  |-  ( z  e.  ( R1 `  x )  ->  ( A. y  e.  x  A. u  e.  ( R1 `  y ) (
rank `  u )  C_  ( rank " ( TC `  u ) )  ->  A. u  e.  z  ( rank `  u
)  C_  ( rank " ( TC `  u
) ) ) )
2614, 15, 25sylc 58 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  On  /\ 
A. y  e.  x  A. u  e.  ( R1 `  y ) (
rank `  u )  C_  ( rank " ( TC `  u ) ) )  /\  ( z  e.  ( R1 `  x )  /\  w  e.  ( rank `  z
) ) )  ->  A. u  e.  z 
( rank `  u )  C_  ( rank " ( TC `  u ) ) )
27 rankval3b 7686 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  U. ( R1
" On )  -> 
( rank `  z )  =  |^| { x  e.  On  |  A. u  e.  z  ( rank `  u )  e.  x } )
2827eleq2d 2455 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  U. ( R1
" On )  -> 
( w  e.  (
rank `  z )  <->  w  e.  |^| { x  e.  On  |  A. u  e.  z  ( rank `  u )  e.  x } ) )
2928biimpd 199 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  U. ( R1
" On )  -> 
( w  e.  (
rank `  z )  ->  w  e.  |^| { x  e.  On  |  A. u  e.  z  ( rank `  u )  e.  x } ) )
30 rankon 7655 . . . . . . . . . . . . . . . . . . . 20  |-  ( rank `  z )  e.  On
3130oneli 4630 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  ( rank `  z
)  ->  w  e.  On )
32 eleq2 2449 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  w  ->  (
( rank `  u )  e.  x  <->  ( rank `  u
)  e.  w ) )
3332ralbidv 2670 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  w  ->  ( A. u  e.  z 
( rank `  u )  e.  x  <->  A. u  e.  z  ( rank `  u
)  e.  w ) )
3433onnminsb 4725 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  On  ->  (
w  e.  |^| { x  e.  On  |  A. u  e.  z  ( rank `  u )  e.  x }  ->  -.  A. u  e.  z  ( rank `  u )  e.  w
) )
3531, 34syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  ( rank `  z
)  ->  ( w  e.  |^| { x  e.  On  |  A. u  e.  z  ( rank `  u )  e.  x }  ->  -.  A. u  e.  z  ( rank `  u )  e.  w
) )
3629, 35sylcom 27 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  U. ( R1
" On )  -> 
( w  e.  (
rank `  z )  ->  -.  A. u  e.  z  ( rank `  u
)  e.  w ) )
3721, 36syl 16 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( R1 `  x )  ->  (
w  e.  ( rank `  z )  ->  -.  A. u  e.  z  (
rank `  u )  e.  w ) )
3837imp 419 . . . . . . . . . . . . . . 15  |-  ( ( z  e.  ( R1
`  x )  /\  w  e.  ( rank `  z ) )  ->  -.  A. u  e.  z  ( rank `  u
)  e.  w )
39 rexnal 2661 . . . . . . . . . . . . . . 15  |-  ( E. u  e.  z  -.  ( rank `  u
)  e.  w  <->  -.  A. u  e.  z  ( rank `  u )  e.  w
)
4038, 39sylibr 204 . . . . . . . . . . . . . 14  |-  ( ( z  e.  ( R1
`  x )  /\  w  e.  ( rank `  z ) )  ->  E. u  e.  z  -.  ( rank `  u
)  e.  w )
4140adantl 453 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  On  /\ 
A. y  e.  x  A. u  e.  ( R1 `  y ) (
rank `  u )  C_  ( rank " ( TC `  u ) ) )  /\  ( z  e.  ( R1 `  x )  /\  w  e.  ( rank `  z
) ) )  ->  E. u  e.  z  -.  ( rank `  u
)  e.  w )
42 r19.29 2790 . . . . . . . . . . . . 13  |-  ( ( A. u  e.  z  ( rank `  u
)  C_  ( rank " ( TC `  u
) )  /\  E. u  e.  z  -.  ( rank `  u )  e.  w )  ->  E. u  e.  z  ( ( rank `  u )  C_  ( rank " ( TC
`  u ) )  /\  -.  ( rank `  u )  e.  w
) )
4326, 41, 42syl2anc 643 . . . . . . . . . . . 12  |-  ( ( ( x  e.  On  /\ 
A. y  e.  x  A. u  e.  ( R1 `  y ) (
rank `  u )  C_  ( rank " ( TC `  u ) ) )  /\  ( z  e.  ( R1 `  x )  /\  w  e.  ( rank `  z
) ) )  ->  E. u  e.  z 
( ( rank `  u
)  C_  ( rank " ( TC `  u
) )  /\  -.  ( rank `  u )  e.  w ) )
44 simp2 958 . . . . . . . . . . . . . . 15  |-  ( ( ( z  e.  ( R1 `  x )  /\  w  e.  (
rank `  z )
)  /\  u  e.  z  /\  ( ( rank `  u )  C_  ( rank " ( TC `  u ) )  /\  -.  ( rank `  u
)  e.  w ) )  ->  u  e.  z )
45 vex 2903 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
46 tcid 7612 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  _V  ->  z  C_  ( TC `  z
) )
4745, 46ax-mp 8 . . . . . . . . . . . . . . . 16  |-  z  C_  ( TC `  z )
4847sseli 3288 . . . . . . . . . . . . . . 15  |-  ( u  e.  z  ->  u  e.  ( TC `  z
) )
49 fveq2 5669 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  u  ->  ( rank `  x )  =  ( rank `  u
) )
5049eqeq1d 2396 . . . . . . . . . . . . . . . . 17  |-  ( x  =  u  ->  (
( rank `  x )  =  w  <->  ( rank `  u
)  =  w ) )
5150rspcev 2996 . . . . . . . . . . . . . . . 16  |-  ( ( u  e.  ( TC
`  z )  /\  ( rank `  u )  =  w )  ->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w )
5251ex 424 . . . . . . . . . . . . . . 15  |-  ( u  e.  ( TC `  z )  ->  (
( rank `  u )  =  w  ->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w ) )
5344, 48, 523syl 19 . . . . . . . . . . . . . 14  |-  ( ( ( z  e.  ( R1 `  x )  /\  w  e.  (
rank `  z )
)  /\  u  e.  z  /\  ( ( rank `  u )  C_  ( rank " ( TC `  u ) )  /\  -.  ( rank `  u
)  e.  w ) )  ->  ( ( rank `  u )  =  w  ->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w ) )
54 simp3l 985 . . . . . . . . . . . . . . . 16  |-  ( ( ( z  e.  ( R1 `  x )  /\  w  e.  (
rank `  z )
)  /\  u  e.  z  /\  ( ( rank `  u )  C_  ( rank " ( TC `  u ) )  /\  -.  ( rank `  u
)  e.  w ) )  ->  ( rank `  u )  C_  ( rank " ( TC `  u ) ) )
5554sseld 3291 . . . . . . . . . . . . . . 15  |-  ( ( ( z  e.  ( R1 `  x )  /\  w  e.  (
rank `  z )
)  /\  u  e.  z  /\  ( ( rank `  u )  C_  ( rank " ( TC `  u ) )  /\  -.  ( rank `  u
)  e.  w ) )  ->  ( w  e.  ( rank `  u
)  ->  w  e.  ( rank " ( TC
`  u ) ) ) )
56 simp1l 981 . . . . . . . . . . . . . . . 16  |-  ( ( ( z  e.  ( R1 `  x )  /\  w  e.  (
rank `  z )
)  /\  u  e.  z  /\  ( ( rank `  u )  C_  ( rank " ( TC `  u ) )  /\  -.  ( rank `  u
)  e.  w ) )  ->  z  e.  ( R1 `  x ) )
57 rankf 7654 . . . . . . . . . . . . . . . . . . 19  |-  rank : U. ( R1 " On ) --> On
58 ffn 5532 . . . . . . . . . . . . . . . . . . 19  |-  ( rank
: U. ( R1
" On ) --> On 
->  rank  Fn  U. ( R1 " On ) )
5957, 58ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  rank  Fn  U. ( R1 " On )
60 r1tr 7636 . . . . . . . . . . . . . . . . . . . 20  |-  Tr  ( R1 `  x )
61 trel 4251 . . . . . . . . . . . . . . . . . . . 20  |-  ( Tr  ( R1 `  x
)  ->  ( (
u  e.  z  /\  z  e.  ( R1 `  x ) )  ->  u  e.  ( R1 `  x ) ) )
6260, 61ax-mp 8 . . . . . . . . . . . . . . . . . . 19  |-  ( ( u  e.  z  /\  z  e.  ( R1 `  x ) )  ->  u  e.  ( R1 `  x ) )
63 r1elwf 7656 . . . . . . . . . . . . . . . . . . 19  |-  ( u  e.  ( R1 `  x )  ->  u  e.  U. ( R1 " On ) )
64 tcwf 7741 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  e.  U. ( R1
" On )  -> 
( TC `  u
)  e.  U. ( R1 " On ) )
65 fvex 5683 . . . . . . . . . . . . . . . . . . . . 21  |-  ( TC
`  u )  e. 
_V
6665r1elss 7666 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( TC `  u )  e.  U. ( R1
" On )  <->  ( TC `  u )  C_  U. ( R1 " On ) )
6764, 66sylib 189 . . . . . . . . . . . . . . . . . . 19  |-  ( u  e.  U. ( R1
" On )  -> 
( TC `  u
)  C_  U. ( R1 " On ) )
6862, 63, 673syl 19 . . . . . . . . . . . . . . . . . 18  |-  ( ( u  e.  z  /\  z  e.  ( R1 `  x ) )  -> 
( TC `  u
)  C_  U. ( R1 " On ) )
69 fvelimab 5722 . . . . . . . . . . . . . . . . . 18  |-  ( (
rank  Fn  U. ( R1 " On )  /\  ( TC `  u ) 
C_  U. ( R1 " On ) )  ->  (
w  e.  ( rank " ( TC `  u ) )  <->  E. x  e.  ( TC `  u
) ( rank `  x
)  =  w ) )
7059, 68, 69sylancr 645 . . . . . . . . . . . . . . . . 17  |-  ( ( u  e.  z  /\  z  e.  ( R1 `  x ) )  -> 
( w  e.  (
rank " ( TC `  u ) )  <->  E. x  e.  ( TC `  u
) ( rank `  x
)  =  w ) )
7145tcel 7618 . . . . . . . . . . . . . . . . . . 19  |-  ( u  e.  z  ->  ( TC `  u )  C_  ( TC `  z ) )
72 ssrexv 3352 . . . . . . . . . . . . . . . . . . 19  |-  ( ( TC `  u ) 
C_  ( TC `  z )  ->  ( E. x  e.  ( TC `  u ) (
rank `  x )  =  w  ->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w ) )
7371, 72syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  z  ->  ( E. x  e.  ( TC `  u ) (
rank `  x )  =  w  ->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w ) )
7473adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( u  e.  z  /\  z  e.  ( R1 `  x ) )  -> 
( E. x  e.  ( TC `  u
) ( rank `  x
)  =  w  ->  E. x  e.  ( TC `  z ) (
rank `  x )  =  w ) )
7570, 74sylbid 207 . . . . . . . . . . . . . . . 16  |-  ( ( u  e.  z  /\  z  e.  ( R1 `  x ) )  -> 
( w  e.  (
rank " ( TC `  u ) )  ->  E. x  e.  ( TC `  z ) (
rank `  x )  =  w ) )
7644, 56, 75syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( ( ( z  e.  ( R1 `  x )  /\  w  e.  (
rank `  z )
)  /\  u  e.  z  /\  ( ( rank `  u )  C_  ( rank " ( TC `  u ) )  /\  -.  ( rank `  u
)  e.  w ) )  ->  ( w  e.  ( rank " ( TC `  u ) )  ->  E. x  e.  ( TC `  z ) ( rank `  x
)  =  w ) )
7755, 76syld 42 . . . . . . . . . . . . . 14  |-  ( ( ( z  e.  ( R1 `  x )  /\  w  e.  (
rank `  z )
)  /\  u  e.  z  /\  ( ( rank `  u )  C_  ( rank " ( TC `  u ) )  /\  -.  ( rank `  u
)  e.  w ) )  ->  ( w  e.  ( rank `  u
)  ->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w ) )
78 rankon 7655 . . . . . . . . . . . . . . . . . . 19  |-  ( rank `  u )  e.  On
79 eloni 4533 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
rank `  u )  e.  On  ->  Ord  ( rank `  u ) )
80 eloni 4533 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  On  ->  Ord  w )
81 ordtri3or 4555 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Ord  ( rank `  u
)  /\  Ord  w )  ->  ( ( rank `  u )  e.  w  \/  ( rank `  u
)  =  w  \/  w  e.  ( rank `  u ) ) )
8279, 80, 81syl2an 464 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( rank `  u
)  e.  On  /\  w  e.  On )  ->  ( ( rank `  u
)  e.  w  \/  ( rank `  u
)  =  w  \/  w  e.  ( rank `  u ) ) )
8378, 31, 82sylancr 645 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  ( rank `  z
)  ->  ( ( rank `  u )  e.  w  \/  ( rank `  u )  =  w  \/  w  e.  (
rank `  u )
) )
84 3orass 939 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( rank `  u
)  e.  w  \/  ( rank `  u
)  =  w  \/  w  e.  ( rank `  u ) )  <->  ( ( rank `  u )  e.  w  \/  ( (
rank `  u )  =  w  \/  w  e.  ( rank `  u
) ) ) )
8583, 84sylib 189 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  ( rank `  z
)  ->  ( ( rank `  u )  e.  w  \/  ( (
rank `  u )  =  w  \/  w  e.  ( rank `  u
) ) ) )
8685orcanai 880 . . . . . . . . . . . . . . . 16  |-  ( ( w  e.  ( rank `  z )  /\  -.  ( rank `  u )  e.  w )  ->  (
( rank `  u )  =  w  \/  w  e.  ( rank `  u
) ) )
8786ad2ant2l 727 . . . . . . . . . . . . . . 15  |-  ( ( ( z  e.  ( R1 `  x )  /\  w  e.  (
rank `  z )
)  /\  ( ( rank `  u )  C_  ( rank " ( TC
`  u ) )  /\  -.  ( rank `  u )  e.  w
) )  ->  (
( rank `  u )  =  w  \/  w  e.  ( rank `  u
) ) )
88873adant2 976 . . . . . . . . . . . . . 14  |-  ( ( ( z  e.  ( R1 `  x )  /\  w  e.  (
rank `  z )
)  /\  u  e.  z  /\  ( ( rank `  u )  C_  ( rank " ( TC `  u ) )  /\  -.  ( rank `  u
)  e.  w ) )  ->  ( ( rank `  u )  =  w  \/  w  e.  ( rank `  u
) ) )
8953, 77, 88mpjaod 371 . . . . . . . . . . . . 13  |-  ( ( ( z  e.  ( R1 `  x )  /\  w  e.  (
rank `  z )
)  /\  u  e.  z  /\  ( ( rank `  u )  C_  ( rank " ( TC `  u ) )  /\  -.  ( rank `  u
)  e.  w ) )  ->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w )
9089rexlimdv3a 2776 . . . . . . . . . . . 12  |-  ( ( z  e.  ( R1
`  x )  /\  w  e.  ( rank `  z ) )  -> 
( E. u  e.  z  ( ( rank `  u )  C_  ( rank " ( TC `  u ) )  /\  -.  ( rank `  u
)  e.  w )  ->  E. x  e.  ( TC `  z ) ( rank `  x
)  =  w ) )
9113, 43, 90sylc 58 . . . . . . . . . . 11  |-  ( ( ( x  e.  On  /\ 
A. y  e.  x  A. u  e.  ( R1 `  y ) (
rank `  u )  C_  ( rank " ( TC `  u ) ) )  /\  ( z  e.  ( R1 `  x )  /\  w  e.  ( rank `  z
) ) )  ->  E. x  e.  ( TC `  z ) (
rank `  x )  =  w )
9291expr 599 . . . . . . . . . 10  |-  ( ( ( x  e.  On  /\ 
A. y  e.  x  A. u  e.  ( R1 `  y ) (
rank `  u )  C_  ( rank " ( TC `  u ) ) )  /\  z  e.  ( R1 `  x
) )  ->  (
w  e.  ( rank `  z )  ->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w ) )
93 tcwf 7741 . . . . . . . . . . . . 13  |-  ( z  e.  U. ( R1
" On )  -> 
( TC `  z
)  e.  U. ( R1 " On ) )
94 r1elssi 7665 . . . . . . . . . . . . . 14  |-  ( ( TC `  z )  e.  U. ( R1
" On )  -> 
( TC `  z
)  C_  U. ( R1 " On ) )
95 fvelimab 5722 . . . . . . . . . . . . . 14  |-  ( (
rank  Fn  U. ( R1 " On )  /\  ( TC `  z ) 
C_  U. ( R1 " On ) )  ->  (
w  e.  ( rank " ( TC `  z ) )  <->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w ) )
9694, 95sylan2 461 . . . . . . . . . . . . 13  |-  ( (
rank  Fn  U. ( R1 " On )  /\  ( TC `  z )  e.  U. ( R1
" On ) )  ->  ( w  e.  ( rank " ( TC `  z ) )  <->  E. x  e.  ( TC `  z ) (
rank `  x )  =  w ) )
9759, 93, 96sylancr 645 . . . . . . . . . . . 12  |-  ( z  e.  U. ( R1
" On )  -> 
( w  e.  (
rank " ( TC `  z ) )  <->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w ) )
9821, 97syl 16 . . . . . . . . . . 11  |-  ( z  e.  ( R1 `  x )  ->  (
w  e.  ( rank " ( TC `  z ) )  <->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w ) )
9998adantl 453 . . . . . . . . . 10  |-  ( ( ( x  e.  On  /\ 
A. y  e.  x  A. u  e.  ( R1 `  y ) (
rank `  u )  C_  ( rank " ( TC `  u ) ) )  /\  z  e.  ( R1 `  x
) )  ->  (
w  e.  ( rank " ( TC `  z ) )  <->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w ) )
10092, 99sylibrd 226 . . . . . . . . 9  |-  ( ( ( x  e.  On  /\ 
A. y  e.  x  A. u  e.  ( R1 `  y ) (
rank `  u )  C_  ( rank " ( TC `  u ) ) )  /\  z  e.  ( R1 `  x
) )  ->  (
w  e.  ( rank `  z )  ->  w  e.  ( rank " ( TC `  z ) ) ) )
101100ssrdv 3298 . . . . . . . 8  |-  ( ( ( x  e.  On  /\ 
A. y  e.  x  A. u  e.  ( R1 `  y ) (
rank `  u )  C_  ( rank " ( TC `  u ) ) )  /\  z  e.  ( R1 `  x
) )  ->  ( rank `  z )  C_  ( rank " ( TC
`  z ) ) )
102101ralrimiva 2733 . . . . . . 7  |-  ( ( x  e.  On  /\  A. y  e.  x  A. u  e.  ( R1 `  y ) ( rank `  u )  C_  ( rank " ( TC `  u ) ) )  ->  A. z  e.  ( R1 `  x ) ( rank `  z
)  C_  ( rank " ( TC `  z
) ) )
103102ex 424 . . . . . 6  |-  ( x  e.  On  ->  ( A. y  e.  x  A. u  e.  ( R1 `  y ) (
rank `  u )  C_  ( rank " ( TC `  u ) )  ->  A. z  e.  ( R1 `  x ) ( rank `  z
)  C_  ( rank " ( TC `  z
) ) ) )
10410, 12, 103tfis3 4778 . . . . 5  |-  ( suc  y  e.  On  ->  A. z  e.  ( R1
`  suc  y )
( rank `  z )  C_  ( rank " ( TC `  z ) ) )
105 fveq2 5669 . . . . . . 7  |-  ( z  =  A  ->  ( rank `  z )  =  ( rank `  A
) )
106 fveq2 5669 . . . . . . . 8  |-  ( z  =  A  ->  ( TC `  z )  =  ( TC `  A
) )
107106imaeq2d 5144 . . . . . . 7  |-  ( z  =  A  ->  ( rank " ( TC `  z ) )  =  ( rank " ( TC `  A ) ) )
108105, 107sseq12d 3321 . . . . . 6  |-  ( z  =  A  ->  (
( rank `  z )  C_  ( rank " ( TC `  z ) )  <-> 
( rank `  A )  C_  ( rank " ( TC `  A ) ) ) )
109108rspccv 2993 . . . . 5  |-  ( A. z  e.  ( R1 ` 
suc  y ) (
rank `  z )  C_  ( rank " ( TC `  z ) )  ->  ( A  e.  ( R1 `  suc  y )  ->  ( rank `  A )  C_  ( rank " ( TC
`  A ) ) ) )
1102, 104, 1093syl 19 . . . 4  |-  ( y  e.  On  ->  ( A  e.  ( R1 ` 
suc  y )  -> 
( rank `  A )  C_  ( rank " ( TC `  A ) ) ) )
111110rexlimiv 2768 . . 3  |-  ( E. y  e.  On  A  e.  ( R1 `  suc  y )  ->  ( rank `  A )  C_  ( rank " ( TC
`  A ) ) )
1121, 111sylbi 188 . 2  |-  ( A  e.  U. ( R1
" On )  -> 
( rank `  A )  C_  ( rank " ( TC `  A ) ) )
113 tcvalg 7611 . . . 4  |-  ( A  e.  U. ( R1
" On )  -> 
( TC `  A
)  =  |^| { x  |  ( A  C_  x  /\  Tr  x ) } )
114 r1rankidb 7664 . . . . 5  |-  ( A  e.  U. ( R1
" On )  ->  A  C_  ( R1 `  ( rank `  A )
) )
115 r1tr 7636 . . . . 5  |-  Tr  ( R1 `  ( rank `  A
) )
116 fvex 5683 . . . . . . 7  |-  ( R1
`  ( rank `  A
) )  e.  _V
117 sseq2 3314 . . . . . . . 8  |-  ( x  =  ( R1 `  ( rank `  A )
)  ->  ( A  C_  x  <->  A  C_  ( R1
`  ( rank `  A
) ) ) )
118 treq 4250 . . . . . . . 8  |-  ( x  =  ( R1 `  ( rank `  A )
)  ->  ( Tr  x 
<->  Tr  ( R1 `  ( rank `  A )
) ) )
119117, 118anbi12d 692 . . . . . . 7  |-  ( x  =  ( R1 `  ( rank `  A )
)  ->  ( ( A  C_  x  /\  Tr  x )  <->  ( A  C_  ( R1 `  ( rank `  A ) )  /\  Tr  ( R1
`  ( rank `  A
) ) ) ) )
120116, 119elab 3026 . . . . . 6  |-  ( ( R1 `  ( rank `  A ) )  e. 
{ x  |  ( A  C_  x  /\  Tr  x ) }  <->  ( A  C_  ( R1 `  ( rank `  A ) )  /\  Tr  ( R1
`  ( rank `  A
) ) ) )
121 intss1 4008 . . . . . 6  |-  ( ( R1 `  ( rank `  A ) )  e. 
{ x  |  ( A  C_  x  /\  Tr  x ) }  ->  |^|
{ x  |  ( A  C_  x  /\  Tr  x ) }  C_  ( R1 `  ( rank `  A ) ) )
122120, 121sylbir 205 . . . . 5  |-  ( ( A  C_  ( R1 `  ( rank `  A
) )  /\  Tr  ( R1 `  ( rank `  A ) ) )  ->  |^| { x  |  ( A  C_  x  /\  Tr  x ) } 
C_  ( R1 `  ( rank `  A )
) )
123114, 115, 122sylancl 644 . . . 4  |-  ( A  e.  U. ( R1
" On )  ->  |^| { x  |  ( A  C_  x  /\  Tr  x ) }  C_  ( R1 `  ( rank `  A ) ) )
124113, 123eqsstrd 3326 . . 3  |-  ( A  e.  U. ( R1
" On )  -> 
( TC `  A
)  C_  ( R1 `  ( rank `  A
) ) )
125 imass2 5181 . . . 4  |-  ( ( TC `  A ) 
C_  ( R1 `  ( rank `  A )
)  ->  ( rank " ( TC `  A
) )  C_  ( rank " ( R1 `  ( rank `  A )
) ) )
126 ffun 5534 . . . . . . . 8  |-  ( rank
: U. ( R1
" On ) --> On 
->  Fun  rank )
12757, 126ax-mp 8 . . . . . . 7  |-  Fun  rank
128 fvelima 5718 . . . . . . 7  |-  ( ( Fun  rank  /\  x  e.  ( rank " ( R1 `  ( rank `  A
) ) ) )  ->  E. y  e.  ( R1 `  ( rank `  A ) ) (
rank `  y )  =  x )
129127, 128mpan 652 . . . . . 6  |-  ( x  e.  ( rank " ( R1 `  ( rank `  A
) ) )  ->  E. y  e.  ( R1 `  ( rank `  A
) ) ( rank `  y )  =  x )
130 rankr1ai 7658 . . . . . . . 8  |-  ( y  e.  ( R1 `  ( rank `  A )
)  ->  ( rank `  y )  e.  (
rank `  A )
)
131 eleq1 2448 . . . . . . . 8  |-  ( (
rank `  y )  =  x  ->  ( (
rank `  y )  e.  ( rank `  A
)  <->  x  e.  ( rank `  A ) ) )
132130, 131syl5ibcom 212 . . . . . . 7  |-  ( y  e.  ( R1 `  ( rank `  A )
)  ->  ( ( rank `  y )  =  x  ->  x  e.  ( rank `  A )
) )
133132rexlimiv 2768 . . . . . 6  |-  ( E. y  e.  ( R1
`  ( rank `  A
) ) ( rank `  y )  =  x  ->  x  e.  (
rank `  A )
)
134129, 133syl 16 . . . . 5  |-  ( x  e.  ( rank " ( R1 `  ( rank `  A
) ) )  ->  x  e.  ( rank `  A ) )
135134ssriv 3296 . . . 4  |-  ( rank " ( R1 `  ( rank `  A )
) )  C_  ( rank `  A )
136125, 135syl6ss 3304 . . 3  |-  ( ( TC `  A ) 
C_  ( R1 `  ( rank `  A )
)  ->  ( rank " ( TC `  A
) )  C_  ( rank `  A ) )
137124, 136syl 16 . 2  |-  ( A  e.  U. ( R1
" On )  -> 
( rank " ( TC
`  A ) ) 
C_  ( rank `  A
) )
138112, 137eqssd 3309 1  |-  ( A  e.  U. ( R1
" On )  -> 
( rank `  A )  =  ( rank " ( TC `  A ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    \/ w3o 935    /\ w3a 936    = wceq 1649    e. wcel 1717   {cab 2374   A.wral 2650   E.wrex 2651   {crab 2654   _Vcvv 2900    C_ wss 3264   U.cuni 3958   |^|cint 3993   Tr wtr 4244   Ord word 4522   Oncon0 4523   suc csuc 4525   "cima 4822   Fun wfun 5389    Fn wfn 5390   -->wf 5391   ` cfv 5395   TCctc 7609   R1cr1 7622   rankcrnk 7623
This theorem is referenced by:  hsmexlem5  8244  grur1  8629
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2369  ax-rep 4262  ax-sep 4272  ax-nul 4280  ax-pow 4319  ax-pr 4345  ax-un 4642  ax-inf2 7530
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2243  df-mo 2244  df-clab 2375  df-cleq 2381  df-clel 2384  df-nfc 2513  df-ne 2553  df-ral 2655  df-rex 2656  df-reu 2657  df-rab 2659  df-v 2902  df-sbc 3106  df-csb 3196  df-dif 3267  df-un 3269  df-in 3271  df-ss 3278  df-pss 3280  df-nul 3573  df-if 3684  df-pw 3745  df-sn 3764  df-pr 3765  df-tp 3766  df-op 3767  df-uni 3959  df-int 3994  df-iun 4038  df-br 4155  df-opab 4209  df-mpt 4210  df-tr 4245  df-eprel 4436  df-id 4440  df-po 4445  df-so 4446  df-fr 4483  df-we 4485  df-ord 4526  df-on 4527  df-lim 4528  df-suc 4529  df-om 4787  df-xp 4825  df-rel 4826  df-cnv 4827  df-co 4828  df-dm 4829  df-rn 4830  df-res 4831  df-ima 4832  df-iota 5359  df-fun 5397  df-fn 5398  df-f 5399  df-f1 5400  df-fo 5401  df-f1o 5402  df-fv 5403  df-recs 6570  df-rdg 6605  df-tc 7610  df-r1 7624  df-rank 7625
  Copyright terms: Public domain W3C validator