Metamath Proof Explorer

Theorem tcrank

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 ( rankA ) , 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 ( TCA ) 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)

Ref Expression
Assertion tcrank 
|- ( A e. U. ( R1 " On ) -> ( rank ` A ) = ( rank " ( TC ` A ) ) )

Proof

Step Hyp Ref Expression
1 rankwflemb 
 |-  ( A e. U. ( R1 " On ) <-> E. y e. On A e. ( R1 ` suc y ) )
2 suceloni 
 |-  ( y e. On -> suc y e. On )
3 fveq2 
 |-  ( x = y -> ( R1 ` x ) = ( R1 ` y ) )
4 3 raleqdv 
 |-  ( 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 
 |-  ( z = u -> ( rank ` z ) = ( rank ` u ) )
6 fveq2 
 |-  ( z = u -> ( TC ` z ) = ( TC ` u ) )
7 6 imaeq2d 
 |-  ( z = u -> ( rank " ( TC ` z ) ) = ( rank " ( TC ` u ) ) )
8 5 7 sseq12d 
 |-  ( z = u -> ( ( rank ` z ) C_ ( rank " ( TC ` z ) ) <-> ( rank ` u ) C_ ( rank " ( TC ` u ) ) ) )
9 8 cbvralvw 
 |-  ( A. z e. ( R1 ` y ) ( rank ` z ) C_ ( rank " ( TC ` z ) ) <-> A. u e. ( R1 ` y ) ( rank ` u ) C_ ( rank " ( TC ` u ) ) )
10 4 9 bitrdi 
 |-  ( 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 
 |-  ( x = suc y -> ( R1 ` x ) = ( R1 ` suc y ) )
12 11 raleqdv 
 |-  ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( ( ( 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 
 |-  ( z e. ( R1 ` x ) -> ( rank ` z ) e. x )
17 fveq2 
 |-  ( y = ( rank ` z ) -> ( R1 ` y ) = ( R1 ` ( rank ` z ) ) )
18 17 raleqdv 
 |-  ( 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 ) ) ) )
19 18 rspcv 
 |-  ( ( 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 ) ) ) )
20 16 19 syl 
 |-  ( 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 
 |-  ( z e. ( R1 ` x ) -> z e. U. ( R1 " On ) )
22 r1rankidb 
 |-  ( z e. U. ( R1 " On ) -> z C_ ( R1 ` ( rank ` z ) ) )
23 ssralv 
 |-  ( 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 ) ) ) )
24 21 22 23 3syl 
 |-  ( 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 ) ) ) )
25 20 24 syld 
 |-  ( 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 ) ) ) )
26 14 15 25 sylc 
 |-  ( ( ( 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 
 |-  ( z e. U. ( R1 " On ) -> ( rank ` z ) = |^| { x e. On | A. u e. z ( rank ` u ) e. x } )
28 27 eleq2d 
 |-  ( z e. U. ( R1 " On ) -> ( w e. ( rank ` z ) <-> w e. |^| { x e. On | A. u e. z ( rank ` u ) e. x } ) )
29 28 biimpd 
 |-  ( z e. U. ( R1 " On ) -> ( w e. ( rank ` z ) -> w e. |^| { x e. On | A. u e. z ( rank ` u ) e. x } ) )
30 rankon 
 |-  ( rank ` z ) e. On
31 30 oneli 
 |-  ( w e. ( rank ` z ) -> w e. On )
32 eleq2w 
 |-  ( x = w -> ( ( rank ` u ) e. x <-> ( rank ` u ) e. w ) )
33 32 ralbidv 
 |-  ( x = w -> ( A. u e. z ( rank ` u ) e. x <-> A. u e. z ( rank ` u ) e. w ) )
34 33 onnminsb 
 |-  ( w e. On -> ( w e. |^| { x e. On | A. u e. z ( rank ` u ) e. x } -> -. A. u e. z ( rank ` u ) e. w ) )
35 31 34 syl 
 |-  ( 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 ) )
36 29 35 sylcom 
 |-  ( z e. U. ( R1 " On ) -> ( w e. ( rank ` z ) -> -. A. u e. z ( rank ` u ) e. w ) )
37 21 36 syl 
 |-  ( z e. ( R1 ` x ) -> ( w e. ( rank ` z ) -> -. A. u e. z ( rank ` u ) e. w ) )
38 37 imp 
 |-  ( ( z e. ( R1 ` x ) /\ w e. ( rank ` z ) ) -> -. A. u e. z ( rank ` u ) e. w )
39 rexnal 
 |-  ( E. u e. z -. ( rank ` u ) e. w <-> -. A. u e. z ( rank ` u ) e. w )
40 38 39 sylibr 
 |-  ( ( z e. ( R1 ` x ) /\ w e. ( rank ` z ) ) -> E. u e. z -. ( rank ` u ) e. w )
41 40 adantl 
 |-  ( ( ( 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 
 |-  ( ( 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 ) )
43 26 41 42 syl2anc 
 |-  ( ( ( 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 
 |-  ( ( ( 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 tcid 
 |-  ( z e. _V -> z C_ ( TC ` z ) )
46 45 elv 
 |-  z C_ ( TC ` z )
47 46 sseli 
 |-  ( u e. z -> u e. ( TC ` z ) )
48 fveqeq2 
 |-  ( x = u -> ( ( rank ` x ) = w <-> ( rank ` u ) = w ) )
49 48 rspcev 
 |-  ( ( u e. ( TC ` z ) /\ ( rank ` u ) = w ) -> E. x e. ( TC ` z ) ( rank ` x ) = w )
50 49 ex 
 |-  ( u e. ( TC ` z ) -> ( ( rank ` u ) = w -> E. x e. ( TC ` z ) ( rank ` x ) = w ) )
51 44 47 50 3syl 
 |-  ( ( ( 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 ) )
52 simp3l 
 |-  ( ( ( 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 ) ) )
53 52 sseld 
 |-  ( ( ( 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 ) ) ) )
54 simp1l 
 |-  ( ( ( 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 ) )
55 rankf 
 |-  rank : U. ( R1 " On ) --> On
56 ffn 
 |-  ( rank : U. ( R1 " On ) --> On -> rank Fn U. ( R1 " On ) )
57 55 56 ax-mp 
 |-  rank Fn U. ( R1 " On )
58 r1tr 
 |-  Tr ( R1 ` x )
59 trel 
 |-  ( Tr ( R1 ` x ) -> ( ( u e. z /\ z e. ( R1 ` x ) ) -> u e. ( R1 ` x ) ) )
60 58 59 ax-mp 
 |-  ( ( u e. z /\ z e. ( R1 ` x ) ) -> u e. ( R1 ` x ) )
61 r1elwf 
 |-  ( u e. ( R1 ` x ) -> u e. U. ( R1 " On ) )
62 tcwf 
 |-  ( u e. U. ( R1 " On ) -> ( TC ` u ) e. U. ( R1 " On ) )
63 fvex 
 |-  ( TC ` u ) e. _V
64 63 r1elss 
 |-  ( ( TC ` u ) e. U. ( R1 " On ) <-> ( TC ` u ) C_ U. ( R1 " On ) )
65 62 64 sylib 
 |-  ( u e. U. ( R1 " On ) -> ( TC ` u ) C_ U. ( R1 " On ) )
66 60 61 65 3syl 
 |-  ( ( u e. z /\ z e. ( R1 ` x ) ) -> ( TC ` u ) C_ U. ( R1 " On ) )
67 fvelimab 
 |-  ( ( rank Fn U. ( R1 " On ) /\ ( TC ` u ) C_ U. ( R1 " On ) ) -> ( w e. ( rank " ( TC ` u ) ) <-> E. x e. ( TC ` u ) ( rank ` x ) = w ) )
68 57 66 67 sylancr 
 |-  ( ( u e. z /\ z e. ( R1 ` x ) ) -> ( w e. ( rank " ( TC ` u ) ) <-> E. x e. ( TC ` u ) ( rank ` x ) = w ) )
69 vex 
 |-  z e. _V
70 69 tcel 
 |-  ( u e. z -> ( TC ` u ) C_ ( TC ` z ) )
71 ssrexv 
 |-  ( ( TC ` u ) C_ ( TC ` z ) -> ( E. x e. ( TC ` u ) ( rank ` x ) = w -> E. x e. ( TC ` z ) ( rank ` x ) = w ) )
72 70 71 syl 
 |-  ( u e. z -> ( E. x e. ( TC ` u ) ( rank ` x ) = w -> E. x e. ( TC ` z ) ( rank ` x ) = w ) )
73 72 adantr 
 |-  ( ( u e. z /\ z e. ( R1 ` x ) ) -> ( E. x e. ( TC ` u ) ( rank ` x ) = w -> E. x e. ( TC ` z ) ( rank ` x ) = w ) )
74 68 73 sylbid 
 |-  ( ( u e. z /\ z e. ( R1 ` x ) ) -> ( w e. ( rank " ( TC ` u ) ) -> E. x e. ( TC ` z ) ( rank ` x ) = w ) )
75 44 54 74 syl2anc 
 |-  ( ( ( 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 ) )
76 53 75 syld 
 |-  ( ( ( 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 ) )
77 rankon 
 |-  ( rank ` u ) e. On
78 eloni 
 |-  ( ( rank ` u ) e. On -> Ord ( rank ` u ) )
79 eloni 
 |-  ( w e. On -> Ord w )
80 ordtri3or 
 |-  ( ( Ord ( rank ` u ) /\ Ord w ) -> ( ( rank ` u ) e. w \/ ( rank ` u ) = w \/ w e. ( rank ` u ) ) )
81 78 79 80 syl2an 
 |-  ( ( ( rank ` u ) e. On /\ w e. On ) -> ( ( rank ` u ) e. w \/ ( rank ` u ) = w \/ w e. ( rank ` u ) ) )
82 77 31 81 sylancr 
 |-  ( w e. ( rank ` z ) -> ( ( rank ` u ) e. w \/ ( rank ` u ) = w \/ w e. ( rank ` u ) ) )
83 3orass 
 |-  ( ( ( rank ` u ) e. w \/ ( rank ` u ) = w \/ w e. ( rank ` u ) ) <-> ( ( rank ` u ) e. w \/ ( ( rank ` u ) = w \/ w e. ( rank ` u ) ) ) )
84 82 83 sylib 
 |-  ( w e. ( rank ` z ) -> ( ( rank ` u ) e. w \/ ( ( rank ` u ) = w \/ w e. ( rank ` u ) ) ) )
85 84 orcanai 
 |-  ( ( w e. ( rank ` z ) /\ -. ( rank ` u ) e. w ) -> ( ( rank ` u ) = w \/ w e. ( rank ` u ) ) )
86 85 ad2ant2l 
 |-  ( ( ( 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 ) ) )
87 86 3adant2 
 |-  ( ( ( 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 ) ) )
88 51 76 87 mpjaod 
 |-  ( ( ( 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 )
89 88 rexlimdv3a 
 |-  ( ( 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 ) )
90 13 43 89 sylc 
 |-  ( ( ( 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 )
91 90 expr 
 |-  ( ( ( 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 ) )
92 tcwf 
 |-  ( z e. U. ( R1 " On ) -> ( TC ` z ) e. U. ( R1 " On ) )
93 r1elssi 
 |-  ( ( TC ` z ) e. U. ( R1 " On ) -> ( TC ` z ) C_ U. ( R1 " On ) )
94 fvelimab 
 |-  ( ( rank Fn U. ( R1 " On ) /\ ( TC ` z ) C_ U. ( R1 " On ) ) -> ( w e. ( rank " ( TC ` z ) ) <-> E. x e. ( TC ` z ) ( rank ` x ) = w ) )
95 93 94 sylan2 
 |-  ( ( rank Fn U. ( R1 " On ) /\ ( TC ` z ) e. U. ( R1 " On ) ) -> ( w e. ( rank " ( TC ` z ) ) <-> E. x e. ( TC ` z ) ( rank ` x ) = w ) )
96 57 92 95 sylancr 
 |-  ( z e. U. ( R1 " On ) -> ( w e. ( rank " ( TC ` z ) ) <-> E. x e. ( TC ` z ) ( rank ` x ) = w ) )
97 21 96 syl 
 |-  ( z e. ( R1 ` x ) -> ( w e. ( rank " ( TC ` z ) ) <-> E. x e. ( TC ` z ) ( rank ` x ) = w ) )
98 97 adantl 
 |-  ( ( ( 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 ) )
99 91 98 sylibrd 
 |-  ( ( ( 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 ) ) ) )
100 99 ssrdv 
 |-  ( ( ( 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 ) ) )
101 100 ralrimiva 
 |-  ( ( 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 ) ) )
102 101 ex 
 |-  ( 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 ) ) ) )
103 10 12 102 tfis3 
 |-  ( suc y e. On -> A. z e. ( R1 ` suc y ) ( rank ` z ) C_ ( rank " ( TC ` z ) ) )
104 fveq2 
 |-  ( z = A -> ( rank ` z ) = ( rank ` A ) )
105 fveq2 
 |-  ( z = A -> ( TC ` z ) = ( TC ` A ) )
106 105 imaeq2d 
 |-  ( z = A -> ( rank " ( TC ` z ) ) = ( rank " ( TC ` A ) ) )
107 104 106 sseq12d 
 |-  ( z = A -> ( ( rank ` z ) C_ ( rank " ( TC ` z ) ) <-> ( rank ` A ) C_ ( rank " ( TC ` A ) ) ) )
108 107 rspccv 
 |-  ( A. z e. ( R1 ` suc y ) ( rank ` z ) C_ ( rank " ( TC ` z ) ) -> ( A e. ( R1 ` suc y ) -> ( rank ` A ) C_ ( rank " ( TC ` A ) ) ) )
109 2 103 108 3syl 
 |-  ( y e. On -> ( A e. ( R1 ` suc y ) -> ( rank ` A ) C_ ( rank " ( TC ` A ) ) ) )
110 109 rexlimiv 
 |-  ( E. y e. On A e. ( R1 ` suc y ) -> ( rank ` A ) C_ ( rank " ( TC ` A ) ) )
111 1 110 sylbi 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) C_ ( rank " ( TC ` A ) ) )
112 tcvalg 
 |-  ( A e. U. ( R1 " On ) -> ( TC ` A ) = |^| { x | ( A C_ x /\ Tr x ) } )
113 r1rankidb 
 |-  ( A e. U. ( R1 " On ) -> A C_ ( R1 ` ( rank ` A ) ) )
114 r1tr 
 |-  Tr ( R1 ` ( rank ` A ) )
115 fvex 
 |-  ( R1 ` ( rank ` A ) ) e. _V
116 sseq2 
 |-  ( x = ( R1 ` ( rank ` A ) ) -> ( A C_ x <-> A C_ ( R1 ` ( rank ` A ) ) ) )
117 treq 
 |-  ( x = ( R1 ` ( rank ` A ) ) -> ( Tr x <-> Tr ( R1 ` ( rank ` A ) ) ) )
118 116 117 anbi12d 
 |-  ( x = ( R1 ` ( rank ` A ) ) -> ( ( A C_ x /\ Tr x ) <-> ( A C_ ( R1 ` ( rank ` A ) ) /\ Tr ( R1 ` ( rank ` A ) ) ) ) )
119 115 118 elab 
 |-  ( ( R1 ` ( rank ` A ) ) e. { x | ( A C_ x /\ Tr x ) } <-> ( A C_ ( R1 ` ( rank ` A ) ) /\ Tr ( R1 ` ( rank ` A ) ) ) )
120 intss1 
 |-  ( ( R1 ` ( rank ` A ) ) e. { x | ( A C_ x /\ Tr x ) } -> |^| { x | ( A C_ x /\ Tr x ) } C_ ( R1 ` ( rank ` A ) ) )
121 119 120 sylbir 
 |-  ( ( A C_ ( R1 ` ( rank ` A ) ) /\ Tr ( R1 ` ( rank ` A ) ) ) -> |^| { x | ( A C_ x /\ Tr x ) } C_ ( R1 ` ( rank ` A ) ) )
122 113 114 121 sylancl 
 |-  ( A e. U. ( R1 " On ) -> |^| { x | ( A C_ x /\ Tr x ) } C_ ( R1 ` ( rank ` A ) ) )
123 112 122 eqsstrd 
 |-  ( A e. U. ( R1 " On ) -> ( TC ` A ) C_ ( R1 ` ( rank ` A ) ) )
124 imass2 
 |-  ( ( TC ` A ) C_ ( R1 ` ( rank ` A ) ) -> ( rank " ( TC ` A ) ) C_ ( rank " ( R1 ` ( rank ` A ) ) ) )
125 ffun 
 |-  ( rank : U. ( R1 " On ) --> On -> Fun rank )
126 55 125 ax-mp 
 |-  Fun rank
127 fvelima 
 |-  ( ( Fun rank /\ x e. ( rank " ( R1 ` ( rank ` A ) ) ) ) -> E. y e. ( R1 ` ( rank ` A ) ) ( rank ` y ) = x )
128 126 127 mpan 
 |-  ( x e. ( rank " ( R1 ` ( rank ` A ) ) ) -> E. y e. ( R1 ` ( rank ` A ) ) ( rank ` y ) = x )
129 rankr1ai 
 |-  ( y e. ( R1 ` ( rank ` A ) ) -> ( rank ` y ) e. ( rank ` A ) )
130 eleq1 
 |-  ( ( rank ` y ) = x -> ( ( rank ` y ) e. ( rank ` A ) <-> x e. ( rank ` A ) ) )
131 129 130 syl5ibcom 
 |-  ( y e. ( R1 ` ( rank ` A ) ) -> ( ( rank ` y ) = x -> x e. ( rank ` A ) ) )
132 131 rexlimiv 
 |-  ( E. y e. ( R1 ` ( rank ` A ) ) ( rank ` y ) = x -> x e. ( rank ` A ) )
133 128 132 syl 
 |-  ( x e. ( rank " ( R1 ` ( rank ` A ) ) ) -> x e. ( rank ` A ) )
134 133 ssriv 
 |-  ( rank " ( R1 ` ( rank ` A ) ) ) C_ ( rank ` A )
135 124 134 sstrdi 
 |-  ( ( TC ` A ) C_ ( R1 ` ( rank ` A ) ) -> ( rank " ( TC ` A ) ) C_ ( rank ` A ) )
136 123 135 syl 
 |-  ( A e. U. ( R1 " On ) -> ( rank " ( TC ` A ) ) C_ ( rank ` A ) )
137 111 136 eqssd 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) = ( rank " ( TC ` A ) ) )