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

Theorem tcrank 7570
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 7481 . . 3  |-  ( A  e.  U. ( R1
" On )  <->  E. y  e.  On  A  e.  ( R1 `  suc  y
) )
2 suceloni 4620 . . . . 5  |-  ( y  e.  On  ->  suc  y  e.  On )
3 fveq2 5541 . . . . . . . 8  |-  ( x  =  y  ->  ( R1 `  x )  =  ( R1 `  y
) )
43raleqdv 2755 . . . . . . 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 5541 . . . . . . . . 9  |-  ( z  =  u  ->  ( rank `  z )  =  ( rank `  u
) )
6 fveq2 5541 . . . . . . . . . 10  |-  ( z  =  u  ->  ( TC `  z )  =  ( TC `  u
) )
76imaeq2d 5028 . . . . . . . . 9  |-  ( z  =  u  ->  ( rank " ( TC `  z ) )  =  ( rank " ( TC `  u ) ) )
85, 7sseq12d 3220 . . . . . . . 8  |-  ( z  =  u  ->  (
( rank `  z )  C_  ( rank " ( TC `  z ) )  <-> 
( rank `  u )  C_  ( rank " ( TC `  u ) ) ) )
98cbvralv 2777 . . . . . . 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 252 . . . . . 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 5541 . . . . . . 7  |-  ( x  =  suc  y  -> 
( R1 `  x
)  =  ( R1
`  suc  y )
)
1211raleqdv 2755 . . . . . 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 447 . . . . . . . . . . . 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 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
) ) )  -> 
z  e.  ( R1
`  x ) )
15 simplr 731 . . . . . . . . . . . . . 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 7486 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( R1 `  x )  ->  ( rank `  z )  e.  x )
17 fveq2 5541 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( rank `  z
)  ->  ( R1 `  y )  =  ( R1 `  ( rank `  z ) ) )
1817raleqdv 2755 . . . . . . . . . . . . . . . . 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 2893 . . . . . . . . . . . . . . . 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 15 . . . . . . . . . . . . . . 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 7484 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( R1 `  x )  ->  z  e.  U. ( R1 " On ) )
22 r1rankidb 7492 . . . . . . . . . . . . . . . 16  |-  ( z  e.  U. ( R1
" On )  -> 
z  C_  ( R1 `  ( rank `  z
) ) )
23 ssralv 3250 . . . . . . . . . . . . . . . 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 18 . . . . . . . . . . . . . . 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 40 . . . . . . . . . . . . . 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 56 . . . . . . . . . . . . 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 7514 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  U. ( R1
" On )  -> 
( rank `  z )  =  |^| { x  e.  On  |  A. u  e.  z  ( rank `  u )  e.  x } )
2827eleq2d 2363 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  U. ( R1
" On )  -> 
( w  e.  (
rank `  z )  <->  w  e.  |^| { x  e.  On  |  A. u  e.  z  ( rank `  u )  e.  x } ) )
2928biimpd 198 . . . . . . . . . . . . . . . . . 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 7483 . . . . . . . . . . . . . . . . . . . 20  |-  ( rank `  z )  e.  On
3130oneli 4516 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  ( rank `  z
)  ->  w  e.  On )
32 eleq2 2357 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  w  ->  (
( rank `  u )  e.  x  <->  ( rank `  u
)  e.  w ) )
3332ralbidv 2576 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  w  ->  ( A. u  e.  z 
( rank `  u )  e.  x  <->  A. u  e.  z  ( rank `  u
)  e.  w ) )
3433onnminsb 4611 . . . . . . . . . . . . . . . . . . 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 15 . . . . . . . . . . . . . . . . . 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 25 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  U. ( R1
" On )  -> 
( w  e.  (
rank `  z )  ->  -.  A. u  e.  z  ( rank `  u
)  e.  w ) )
3721, 36syl 15 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( R1 `  x )  ->  (
w  e.  ( rank `  z )  ->  -.  A. u  e.  z  (
rank `  u )  e.  w ) )
3837imp 418 . . . . . . . . . . . . . . 15  |-  ( ( z  e.  ( R1
`  x )  /\  w  e.  ( rank `  z ) )  ->  -.  A. u  e.  z  ( rank `  u
)  e.  w )
39 rexnal 2567 . . . . . . . . . . . . . . 15  |-  ( E. u  e.  z  -.  ( rank `  u
)  e.  w  <->  -.  A. u  e.  z  ( rank `  u )  e.  w
)
4038, 39sylibr 203 . . . . . . . . . . . . . 14  |-  ( ( z  e.  ( R1
`  x )  /\  w  e.  ( rank `  z ) )  ->  E. u  e.  z  -.  ( rank `  u
)  e.  w )
4140adantl 452 . . . . . . . . . . . . 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 2696 . . . . . . . . . . . . 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 642 . . . . . . . . . . . 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 956 . . . . . . . . . . . . . . 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 2804 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
46 tcid 7440 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  _V  ->  z  C_  ( TC `  z
) )
4745, 46ax-mp 8 . . . . . . . . . . . . . . . 16  |-  z  C_  ( TC `  z )
4847sseli 3189 . . . . . . . . . . . . . . 15  |-  ( u  e.  z  ->  u  e.  ( TC `  z
) )
49 fveq2 5541 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  u  ->  ( rank `  x )  =  ( rank `  u
) )
5049eqeq1d 2304 . . . . . . . . . . . . . . . . 17  |-  ( x  =  u  ->  (
( rank `  x )  =  w  <->  ( rank `  u
)  =  w ) )
5150rspcev 2897 . . . . . . . . . . . . . . . 16  |-  ( ( u  e.  ( TC
`  z )  /\  ( rank `  u )  =  w )  ->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w )
5251ex 423 . . . . . . . . . . . . . . 15  |-  ( u  e.  ( TC `  z )  ->  (
( rank `  u )  =  w  ->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w ) )
5344, 48, 523syl 18 . . . . . . . . . . . . . 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 983 . . . . . . . . . . . . . . . 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 3192 . . . . . . . . . . . . . . 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 979 . . . . . . . . . . . . . . . 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 7482 . . . . . . . . . . . . . . . . . . 19  |-  rank : U. ( R1 " On ) --> On
58 ffn 5405 . . . . . . . . . . . . . . . . . . 19  |-  ( rank
: U. ( R1
" On ) --> On 
->  rank  Fn  U. ( R1 " On ) )
5957, 58ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  rank  Fn  U. ( R1 " On )
60 r1tr 7464 . . . . . . . . . . . . . . . . . . . 20  |-  Tr  ( R1 `  x )
61 trel 4136 . . . . . . . . . . . . . . . . . . . 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 7484 . . . . . . . . . . . . . . . . . . 19  |-  ( u  e.  ( R1 `  x )  ->  u  e.  U. ( R1 " On ) )
64 tcwf 7569 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  e.  U. ( R1
" On )  -> 
( TC `  u
)  e.  U. ( R1 " On ) )
65 fvex 5555 . . . . . . . . . . . . . . . . . . . . 21  |-  ( TC
`  u )  e. 
_V
6665r1elss 7494 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( TC `  u )  e.  U. ( R1
" On )  <->  ( TC `  u )  C_  U. ( R1 " On ) )
6764, 66sylib 188 . . . . . . . . . . . . . . . . . . 19  |-  ( u  e.  U. ( R1
" On )  -> 
( TC `  u
)  C_  U. ( R1 " On ) )
6862, 63, 673syl 18 . . . . . . . . . . . . . . . . . 18  |-  ( ( u  e.  z  /\  z  e.  ( R1 `  x ) )  -> 
( TC `  u
)  C_  U. ( R1 " On ) )
69 fvelimab 5594 . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . 17  |-  ( ( u  e.  z  /\  z  e.  ( R1 `  x ) )  -> 
( w  e.  (
rank " ( TC `  u ) )  <->  E. x  e.  ( TC `  u
) ( rank `  x
)  =  w ) )
7145tcel 7446 . . . . . . . . . . . . . . . . . . 19  |-  ( u  e.  z  ->  ( TC `  u )  C_  ( TC `  z ) )
72 ssrexv 3251 . . . . . . . . . . . . . . . . . . 19  |-  ( ( TC `  u ) 
C_  ( TC `  z )  ->  ( E. x  e.  ( TC `  u ) (
rank `  x )  =  w  ->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w ) )
7371, 72syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( u  e.  z  ->  ( E. x  e.  ( TC `  u ) (
rank `  x )  =  w  ->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w ) )
7473adantr 451 . . . . . . . . . . . . . . . . 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 206 . . . . . . . . . . . . . . . 16  |-  ( ( u  e.  z  /\  z  e.  ( R1 `  x ) )  -> 
( w  e.  (
rank " ( TC `  u ) )  ->  E. x  e.  ( TC `  z ) (
rank `  x )  =  w ) )
7644, 56, 75syl2anc 642 . . . . . . . . . . . . . . 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 40 . . . . . . . . . . . . . 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 7483 . . . . . . . . . . . . . . . . . . 19  |-  ( rank `  u )  e.  On
79 eloni 4418 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
rank `  u )  e.  On  ->  Ord  ( rank `  u ) )
80 eloni 4418 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  On  ->  Ord  w )
81 ordtri3or 4440 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( Ord  ( rank `  u
)  /\  Ord  w )  ->  ( ( rank `  u )  e.  w  \/  ( rank `  u
)  =  w  \/  w  e.  ( rank `  u ) ) )
8279, 80, 81syl2an 463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( rank `  u
)  e.  On  /\  w  e.  On )  ->  ( ( rank `  u
)  e.  w  \/  ( rank `  u
)  =  w  \/  w  e.  ( rank `  u ) ) )
8378, 31, 82sylancr 644 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  ( rank `  z
)  ->  ( ( rank `  u )  e.  w  \/  ( rank `  u )  =  w  \/  w  e.  (
rank `  u )
) )
84 3orass 937 . . . . . . . . . . . . . . . . . 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 188 . . . . . . . . . . . . . . . . 17  |-  ( w  e.  ( rank `  z
)  ->  ( ( rank `  u )  e.  w  \/  ( (
rank `  u )  =  w  \/  w  e.  ( rank `  u
) ) ) )
8685orcanai 879 . . . . . . . . . . . . . . . 16  |-  ( ( w  e.  ( rank `  z )  /\  -.  ( rank `  u )  e.  w )  ->  (
( rank `  u )  =  w  \/  w  e.  ( rank `  u
) ) )
8786ad2ant2l 726 . . . . . . . . . . . . . . 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 974 . . . . . . . . . . . . . 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 370 . . . . . . . . . . . . 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 2682 . . . . . . . . . . . 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 56 . . . . . . . . . . 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 598 . . . . . . . . . 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 7569 . . . . . . . . . . . . 13  |-  ( z  e.  U. ( R1
" On )  -> 
( TC `  z
)  e.  U. ( R1 " On ) )
94 r1elssi 7493 . . . . . . . . . . . . . 14  |-  ( ( TC `  z )  e.  U. ( R1
" On )  -> 
( TC `  z
)  C_  U. ( R1 " On ) )
95 fvelimab 5594 . . . . . . . . . . . . . 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 460 . . . . . . . . . . . . 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 644 . . . . . . . . . . . 12  |-  ( z  e.  U. ( R1
" On )  -> 
( w  e.  (
rank " ( TC `  z ) )  <->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w ) )
9821, 97syl 15 . . . . . . . . . . 11  |-  ( z  e.  ( R1 `  x )  ->  (
w  e.  ( rank " ( TC `  z ) )  <->  E. x  e.  ( TC `  z
) ( rank `  x
)  =  w ) )
9998adantl 452 . . . . . . . . . 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 225 . . . . . . . . 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 3198 . . . . . . . 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 2639 . . . . . . 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 423 . . . . . 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 4664 . . . . 5  |-  ( suc  y  e.  On  ->  A. z  e.  ( R1
`  suc  y )
( rank `  z )  C_  ( rank " ( TC `  z ) ) )
105 fveq2 5541 . . . . . . 7  |-  ( z  =  A  ->  ( rank `  z )  =  ( rank `  A
) )
106 fveq2 5541 . . . . . . . 8  |-  ( z  =  A  ->  ( TC `  z )  =  ( TC `  A
) )
107106imaeq2d 5028 . . . . . . 7  |-  ( z  =  A  ->  ( rank " ( TC `  z ) )  =  ( rank " ( TC `  A ) ) )
108105, 107sseq12d 3220 . . . . . 6  |-  ( z  =  A  ->  (
( rank `  z )  C_  ( rank " ( TC `  z ) )  <-> 
( rank `  A )  C_  ( rank " ( TC `  A ) ) ) )
109108rspccv 2894 . . . . 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 18 . . . 4  |-  ( y  e.  On  ->  ( A  e.  ( R1 ` 
suc  y )  -> 
( rank `  A )  C_  ( rank " ( TC `  A ) ) ) )
111110rexlimiv 2674 . . 3  |-  ( E. y  e.  On  A  e.  ( R1 `  suc  y )  ->  ( rank `  A )  C_  ( rank " ( TC
`  A ) ) )
1121, 111sylbi 187 . 2  |-  ( A  e.  U. ( R1
" On )  -> 
( rank `  A )  C_  ( rank " ( TC `  A ) ) )
113 tcvalg 7439 . . . 4  |-  ( A  e.  U. ( R1
" On )  -> 
( TC `  A
)  =  |^| { x  |  ( A  C_  x  /\  Tr  x ) } )
114 r1rankidb 7492 . . . . 5  |-  ( A  e.  U. ( R1
" On )  ->  A  C_  ( R1 `  ( rank `  A )
) )
115 r1tr 7464 . . . . 5  |-  Tr  ( R1 `  ( rank `  A
) )
116 fvex 5555 . . . . . . 7  |-  ( R1
`  ( rank `  A
) )  e.  _V
117 sseq2 3213 . . . . . . . 8  |-  ( x  =  ( R1 `  ( rank `  A )
)  ->  ( A  C_  x  <->  A  C_  ( R1
`  ( rank `  A
) ) ) )
118 treq 4135 . . . . . . . 8  |-  ( x  =  ( R1 `  ( rank `  A )
)  ->  ( Tr  x 
<->  Tr  ( R1 `  ( rank `  A )
) ) )
119117, 118anbi12d 691 . . . . . . 7  |-  ( x  =  ( R1 `  ( rank `  A )
)  ->  ( ( A  C_  x  /\  Tr  x )  <->  ( A  C_  ( R1 `  ( rank `  A ) )  /\  Tr  ( R1
`  ( rank `  A
) ) ) ) )
120116, 119elab 2927 . . . . . 6  |-  ( ( R1 `  ( rank `  A ) )  e. 
{ x  |  ( A  C_  x  /\  Tr  x ) }  <->  ( A  C_  ( R1 `  ( rank `  A ) )  /\  Tr  ( R1
`  ( rank `  A
) ) ) )
121 intss1 3893 . . . . . 6  |-  ( ( R1 `  ( rank `  A ) )  e. 
{ x  |  ( A  C_  x  /\  Tr  x ) }  ->  |^|
{ x  |  ( A  C_  x  /\  Tr  x ) }  C_  ( R1 `  ( rank `  A ) ) )
122120, 121sylbir 204 . . . . 5  |-  ( ( A  C_  ( R1 `  ( rank `  A
) )  /\  Tr  ( R1 `  ( rank `  A ) ) )  ->  |^| { x  |  ( A  C_  x  /\  Tr  x ) } 
C_  ( R1 `  ( rank `  A )
) )
123114, 115, 122sylancl 643 . . . 4  |-  ( A  e.  U. ( R1
" On )  ->  |^| { x  |  ( A  C_  x  /\  Tr  x ) }  C_  ( R1 `  ( rank `  A ) ) )
124113, 123eqsstrd 3225 . . 3  |-  ( A  e.  U. ( R1
" On )  -> 
( TC `  A
)  C_  ( R1 `  ( rank `  A
) ) )
125 imass2 5065 . . . 4  |-  ( ( TC `  A ) 
C_  ( R1 `  ( rank `  A )
)  ->  ( rank " ( TC `  A
) )  C_  ( rank " ( R1 `  ( rank `  A )
) ) )
126 ffun 5407 . . . . . . . 8  |-  ( rank
: U. ( R1
" On ) --> On 
->  Fun  rank )
12757, 126ax-mp 8 . . . . . . 7  |-  Fun  rank
128 fvelima 5590 . . . . . . 7  |-  ( ( Fun  rank  /\  x  e.  ( rank " ( R1 `  ( rank `  A
) ) ) )  ->  E. y  e.  ( R1 `  ( rank `  A ) ) (
rank `  y )  =  x )
129127, 128mpan 651 . . . . . 6  |-  ( x  e.  ( rank " ( R1 `  ( rank `  A
) ) )  ->  E. y  e.  ( R1 `  ( rank `  A
) ) ( rank `  y )  =  x )
130 rankr1ai 7486 . . . . . . . 8  |-  ( y  e.  ( R1 `  ( rank `  A )
)  ->  ( rank `  y )  e.  (
rank `  A )
)
131 eleq1 2356 . . . . . . . 8  |-  ( (
rank `  y )  =  x  ->  ( (
rank `  y )  e.  ( rank `  A
)  <->  x  e.  ( rank `  A ) ) )
132130, 131syl5ibcom 211 . . . . . . 7  |-  ( y  e.  ( R1 `  ( rank `  A )
)  ->  ( ( rank `  y )  =  x  ->  x  e.  ( rank `  A )
) )
133132rexlimiv 2674 . . . . . 6  |-  ( E. y  e.  ( R1
`  ( rank `  A
) ) ( rank `  y )  =  x  ->  x  e.  (
rank `  A )
)
134129, 133syl 15 . . . . 5  |-  ( x  e.  ( rank " ( R1 `  ( rank `  A
) ) )  ->  x  e.  ( rank `  A ) )
135134ssriv 3197 . . . 4  |-  ( rank " ( R1 `  ( rank `  A )
) )  C_  ( rank `  A )
136125, 135syl6ss 3204 . . 3  |-  ( ( TC `  A ) 
C_  ( R1 `  ( rank `  A )
)  ->  ( rank " ( TC `  A
) )  C_  ( rank `  A ) )
137124, 136syl 15 . 2  |-  ( A  e.  U. ( R1
" On )  -> 
( rank " ( TC
`  A ) ) 
C_  ( rank `  A
) )
138112, 137eqssd 3209 1  |-  ( A  e.  U. ( R1
" On )  -> 
( rank `  A )  =  ( rank " ( TC `  A ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    \/ w3o 933    /\ w3a 934    = wceq 1632    e. wcel 1696   {cab 2282   A.wral 2556   E.wrex 2557   {crab 2560   _Vcvv 2801    C_ wss 3165   U.cuni 3843   |^|cint 3878   Tr wtr 4129   Ord word 4407   Oncon0 4408   suc csuc 4410   "cima 4708   Fun wfun 5265    Fn wfn 5266   -->wf 5267   ` cfv 5271   TCctc 7437   R1cr1 7450   rankcrnk 7451
This theorem is referenced by:  hsmexlem5  8072  grur1  8458
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-inf2 7358
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-reu 2563  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-int 3879  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-recs 6404  df-rdg 6439  df-tc 7438  df-r1 7452  df-rank 7453
  Copyright terms: Public domain W3C validator