Step |
Hyp |
Ref |
Expression |
1 |
|
ordtypelem.1 |
|- F = recs ( G ) |
2 |
|
ordtypelem.2 |
|- C = { w e. A | A. j e. ran h j R w } |
3 |
|
ordtypelem.3 |
|- G = ( h e. _V |-> ( iota_ v e. C A. u e. C -. u R v ) ) |
4 |
|
ordtypelem.5 |
|- T = { x e. On | E. t e. A A. z e. ( F " x ) z R t } |
5 |
|
ordtypelem.6 |
|- O = OrdIso ( R , A ) |
6 |
|
ordtypelem.7 |
|- ( ph -> R We A ) |
7 |
|
ordtypelem.8 |
|- ( ph -> R Se A ) |
8 |
4
|
ssrab3 |
|- T C_ On |
9 |
8
|
a1i |
|- ( ph -> T C_ On ) |
10 |
9
|
sselda |
|- ( ( ph /\ a e. T ) -> a e. On ) |
11 |
|
onss |
|- ( a e. On -> a C_ On ) |
12 |
10 11
|
syl |
|- ( ( ph /\ a e. T ) -> a C_ On ) |
13 |
|
eloni |
|- ( a e. On -> Ord a ) |
14 |
10 13
|
syl |
|- ( ( ph /\ a e. T ) -> Ord a ) |
15 |
|
imaeq2 |
|- ( x = a -> ( F " x ) = ( F " a ) ) |
16 |
15
|
raleqdv |
|- ( x = a -> ( A. z e. ( F " x ) z R t <-> A. z e. ( F " a ) z R t ) ) |
17 |
16
|
rexbidv |
|- ( x = a -> ( E. t e. A A. z e. ( F " x ) z R t <-> E. t e. A A. z e. ( F " a ) z R t ) ) |
18 |
17 4
|
elrab2 |
|- ( a e. T <-> ( a e. On /\ E. t e. A A. z e. ( F " a ) z R t ) ) |
19 |
18
|
simprbi |
|- ( a e. T -> E. t e. A A. z e. ( F " a ) z R t ) |
20 |
19
|
adantl |
|- ( ( ph /\ a e. T ) -> E. t e. A A. z e. ( F " a ) z R t ) |
21 |
|
ordelss |
|- ( ( Ord a /\ x e. a ) -> x C_ a ) |
22 |
|
imass2 |
|- ( x C_ a -> ( F " x ) C_ ( F " a ) ) |
23 |
|
ssralv |
|- ( ( F " x ) C_ ( F " a ) -> ( A. z e. ( F " a ) z R t -> A. z e. ( F " x ) z R t ) ) |
24 |
23
|
reximdv |
|- ( ( F " x ) C_ ( F " a ) -> ( E. t e. A A. z e. ( F " a ) z R t -> E. t e. A A. z e. ( F " x ) z R t ) ) |
25 |
21 22 24
|
3syl |
|- ( ( Ord a /\ x e. a ) -> ( E. t e. A A. z e. ( F " a ) z R t -> E. t e. A A. z e. ( F " x ) z R t ) ) |
26 |
25
|
ralrimdva |
|- ( Ord a -> ( E. t e. A A. z e. ( F " a ) z R t -> A. x e. a E. t e. A A. z e. ( F " x ) z R t ) ) |
27 |
14 20 26
|
sylc |
|- ( ( ph /\ a e. T ) -> A. x e. a E. t e. A A. z e. ( F " x ) z R t ) |
28 |
|
ssrab |
|- ( a C_ { x e. On | E. t e. A A. z e. ( F " x ) z R t } <-> ( a C_ On /\ A. x e. a E. t e. A A. z e. ( F " x ) z R t ) ) |
29 |
12 27 28
|
sylanbrc |
|- ( ( ph /\ a e. T ) -> a C_ { x e. On | E. t e. A A. z e. ( F " x ) z R t } ) |
30 |
29 4
|
sseqtrrdi |
|- ( ( ph /\ a e. T ) -> a C_ T ) |
31 |
30
|
ralrimiva |
|- ( ph -> A. a e. T a C_ T ) |
32 |
|
dftr3 |
|- ( Tr T <-> A. a e. T a C_ T ) |
33 |
31 32
|
sylibr |
|- ( ph -> Tr T ) |
34 |
|
ordon |
|- Ord On |
35 |
|
trssord |
|- ( ( Tr T /\ T C_ On /\ Ord On ) -> Ord T ) |
36 |
8 34 35
|
mp3an23 |
|- ( Tr T -> Ord T ) |
37 |
33 36
|
syl |
|- ( ph -> Ord T ) |