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

Theorem tcrank 7554
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 7465 . . 3  |-  ( A  e.  U. ( R1
" On )  <->  E. y  e.  On  A  e.  ( R1 `  suc  y
) )
2 suceloni 4604 . . . . 5  |-  ( y  e.  On  ->  suc  y  e.  On )
3 fveq2 5525 . . . . . . . 8  |-  ( x  =  y  ->  ( R1 `  x )  =  ( R1 `  y
) )
43raleqdv 2742 . . . . . . 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 5525 . . . . . . . . 9  |-  ( z  =  u  ->  ( rank `  z )  =  ( rank `  u
) )
6 fveq2 5525 . . . . . . . . . 10  |-  ( z  =  u  ->  ( TC `  z )  =  ( TC `  u
) )
76imaeq2d 5012 . . . . . . . . 9  |-  ( z  =  u  ->  ( rank " ( TC `  z ) )  =  ( rank " ( TC `  u ) ) )
85, 7sseq12d 3207 . . . . . . . 8  |-  ( z  =  u  ->  (
( rank `  z )  C_  ( rank " ( TC `  z ) )  <-> 
( rank `  u )  C_  ( rank " ( TC `  u ) ) ) )
98cbvralv 2764 . . . . . . 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 5525 . . . . . . 7  |-  ( x  =  suc  y  -> 
( R1 `  x
)  =  ( R1
`  suc  y )
)
1211raleqdv 2742 . . . . . 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 7470 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( R1 `  x )  ->  ( rank `  z )  e.  x )
17 fveq2 5525 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  ( rank `  z
)  ->  ( R1 `  y )  =  ( R1 `  ( rank `  z ) ) )
1817raleqdv 2742 . . . . . . . . . . . . . . . . 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 2880 . . . . . . . . . . . . . . . 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 7468 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( R1 `  x )  ->  z  e.  U. ( R1 " On ) )
22 r1rankidb 7476 . . . . . . . . . . . . . . . 16  |-  ( z  e.  U. ( R1
" On )  -> 
z  C_  ( R1 `  ( rank `  z
) ) )
23 ssralv 3237 . . . . . . . . . . . . . . . 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 7498 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  U. ( R1
" On )  -> 
( rank `  z )  =  |^| { x  e.  On  |  A. u  e.  z  ( rank `  u )  e.  x } )
2827eleq2d 2350 . . . . . . . . . . . . . . . . . . 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 7467 . . . . . . . . . . . . . . . . . . . 20  |-  ( rank `  z )  e.  On
3130oneli 4500 . . . . . . . . . . . . . . . . . . 19  |-  ( w  e.  ( rank `  z
)  ->  w  e.  On )
32 eleq2 2344 . . . . . . . . . . . . . . . . . . . . 21  |-  ( x  =  w  ->  (
( rank `  u )  e.  x  <->  ( rank `  u
)  e.  w ) )
3332ralbidv 2563 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  =  w  ->  ( A. u  e.  z 
( rank `  u )  e.  x  <->  A. u  e.  z  ( rank `  u
)  e.  w ) )
3433onnminsb 4595 . . . . . . . . . . . . . . . . . . 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 2554 . . . . . . . . . . . . . . 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 2683 . . . . . . . . . . . . 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 2791 . . . . . . . . . . . . . . . . 17  |-  z  e. 
_V
46 tcid 7424 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  _V  ->  z  C_  ( TC `  z
) )
4745, 46ax-mp 8 . . . . . . . . . . . . . . . 16  |-  z  C_  ( TC `  z )
4847sseli 3176 . . . . . . . . . . . . . . 15  |-  ( u  e.  z  ->  u  e.  ( TC `  z
) )
49 fveq2 5525 . . . . . . . . . . . . . . . . . 18  |-  ( x  =  u  ->  ( rank `  x )  =  ( rank `  u
) )
5049eqeq1d 2291 . . . . . . . . . . . . . . . . 17  |-  ( x  =  u  ->  (
( rank `  x )  =  w  <->  ( rank `  u
)  =  w ) )
5150rspcev 2884 . . . . . . . . . . . . . . . 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 3179 . . . . . . . . . . . . . . 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 7466 . . . . . . . . . . . . . . . . . . 19  |-  rank : U. ( R1 " On ) --> On
58 ffn 5389 . . . . . . . . . . . . . . . . . . 19  |-  ( rank
: U. ( R1
" On ) --> On 
->  rank  Fn  U. ( R1 " On ) )
5957, 58ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  rank  Fn  U. ( R1 " On )
60 r1tr 7448 . . . . . . . . . . . . . . . . . . . 20  |-  Tr  ( R1 `  x )
61 trel 4120 . . . . . . . . . . . . . . . . . . . 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 7468 . . . . . . . . . . . . . . . . . . 19  |-  ( u  e.  ( R1 `  x )  ->  u  e.  U. ( R1 " On ) )
64 tcwf 7553 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  e.  U. ( R1
" On )  -> 
( TC `  u
)  e.  U. ( R1 " On ) )
65 fvex 5539 . . . . . . . . . . . . . . . . . . . . 21  |-  ( TC
`  u )  e. 
_V
6665r1elss 7478 . . . . . . . . . . . . . . . . . . . 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 5578 . . . . . . . . . . . . . . . . . 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 7430 . . . . . . . . . . . . . . . . . . 19  |-  ( u  e.  z  ->  ( TC `  u )  C_  ( TC `  z ) )
72 ssrexv 3238 . . . . . . . . . . . . . . . . . . 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 7467 . . . . . . . . . . . . . . . . . . 19  |-  ( rank `  u )  e.  On
79 eloni 4402 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
rank `  u )  e.  On  ->  Ord  ( rank `  u ) )
80 eloni 4402 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  e.  On  ->  Ord  w )
81 ordtri3or 4424 . . . . . . . . . . . . . . . . . . . 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 2669 . . . . . . . . . . . 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 7553 . . . . . . . . . . . . 13  |-  ( z  e.  U. ( R1
" On )  -> 
( TC `  z
)  e.  U. ( R1 " On ) )
94 r1elssi 7477 . . . . . . . . . . . . . 14  |-  ( ( TC `  z )  e.  U. ( R1
" On )  -> 
( TC `  z
)  C_  U. ( R1 " On ) )
95 fvelimab 5578 . . . . . . . . . . . . . 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 3185 . . . . . . . 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 2626 . . . . . . 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 4648 . . . . 5  |-  ( suc  y  e.  On  ->  A. z  e.  ( R1
`  suc  y )
( rank `  z )  C_  ( rank " ( TC `  z ) ) )
105 fveq2 5525 . . . . . . 7  |-  ( z  =  A  ->  ( rank `  z )  =  ( rank `  A
) )
106 fveq2 5525 . . . . . . . 8  |-  ( z  =  A  ->  ( TC `  z )  =  ( TC `  A
) )
107106imaeq2d 5012 . . . . . . 7  |-  ( z  =  A  ->  ( rank " ( TC `  z ) )  =  ( rank " ( TC `  A ) ) )
108105, 107sseq12d 3207 . . . . . 6  |-  ( z  =  A  ->  (
( rank `  z )  C_  ( rank " ( TC `  z ) )  <-> 
( rank `  A )  C_  ( rank " ( TC `  A ) ) ) )
109108rspccv 2881 . . . . 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 2661 . . 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 7423 . . . 4  |-  ( A  e.  U. ( R1
" On )  -> 
( TC `  A
)  =  |^| { x  |  ( A  C_  x  /\  Tr  x ) } )
114 r1rankidb 7476 . . . . 5  |-  ( A  e.  U. ( R1
" On )  ->  A  C_  ( R1 `  ( rank `  A )
) )
115 r1tr 7448 . . . . 5  |-  Tr  ( R1 `  ( rank `  A
) )
116 fvex 5539 . . . . . . 7  |-  ( R1
`  ( rank `  A
) )  e.  _V
117 sseq2 3200 . . . . . . . 8  |-  ( x  =  ( R1 `  ( rank `  A )
)  ->  ( A  C_  x  <->  A  C_  ( R1
`  ( rank `  A
) ) ) )
118 treq 4119 . . . . . . . 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 2914 . . . . . 6  |-  ( ( R1 `  ( rank `  A ) )  e. 
{ x  |  ( A  C_  x  /\  Tr  x ) }  <->  ( A  C_  ( R1 `  ( rank `  A ) )  /\  Tr  ( R1
`  ( rank `  A
) ) ) )
121 intss1 3877 . . . . . 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 3212 . . 3  |-  ( A  e.  U. ( R1
" On )  -> 
( TC `  A
)  C_  ( R1 `  ( rank `  A
) ) )
125 imass2 5049 . . . 4  |-  ( ( TC `  A ) 
C_  ( R1 `  ( rank `  A )
)  ->  ( rank " ( TC `  A
) )  C_  ( rank " ( R1 `  ( rank `  A )
) ) )
126 ffun 5391 . . . . . . . 8  |-  ( rank
: U. ( R1
" On ) --> On 
->  Fun  rank )
12757, 126ax-mp 8 . . . . . . 7  |-  Fun  rank
128 fvelima 5574 . . . . . . 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 7470 . . . . . . . 8  |-  ( y  e.  ( R1 `  ( rank `  A )
)  ->  ( rank `  y )  e.  (
rank `  A )
)
131 eleq1 2343 . . . . . . . 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 2661 . . . . . 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 3184 . . . 4  |-  ( rank " ( R1 `  ( rank `  A )
) )  C_  ( rank `  A )
136125, 135syl6ss 3191 . . 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 3196 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 1623    e. wcel 1684   {cab 2269   A.wral 2543   E.wrex 2544   {crab 2547   _Vcvv 2788    C_ wss 3152   U.cuni 3827   |^|cint 3862   Tr wtr 4113   Ord word 4391   Oncon0 4392   suc csuc 4394   "cima 4692   Fun wfun 5249    Fn wfn 5250   -->wf 5251   ` cfv 5255   TCctc 7421   R1cr1 7434   rankcrnk 7435
This theorem is referenced by:  hsmexlem5  8056  grur1  8442
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-inf2 7342
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 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-recs 6388  df-rdg 6423  df-tc 7422  df-r1 7436  df-rank 7437
  Copyright terms: Public domain W3C validator