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 |
1
|
tfr1a |
|- ( Fun F /\ Lim dom F ) |
9 |
8
|
simpli |
|- Fun F |
10 |
|
funres |
|- ( Fun F -> Fun ( F |` T ) ) |
11 |
9 10
|
mp1i |
|- ( ph -> Fun ( F |` T ) ) |
12 |
11
|
funfnd |
|- ( ph -> ( F |` T ) Fn dom ( F |` T ) ) |
13 |
|
dmres |
|- dom ( F |` T ) = ( T i^i dom F ) |
14 |
13
|
fneq2i |
|- ( ( F |` T ) Fn dom ( F |` T ) <-> ( F |` T ) Fn ( T i^i dom F ) ) |
15 |
12 14
|
sylib |
|- ( ph -> ( F |` T ) Fn ( T i^i dom F ) ) |
16 |
|
simpr |
|- ( ( ph /\ a e. ( T i^i dom F ) ) -> a e. ( T i^i dom F ) ) |
17 |
16
|
elin1d |
|- ( ( ph /\ a e. ( T i^i dom F ) ) -> a e. T ) |
18 |
17
|
fvresd |
|- ( ( ph /\ a e. ( T i^i dom F ) ) -> ( ( F |` T ) ` a ) = ( F ` a ) ) |
19 |
|
ssrab2 |
|- { v e. { w e. A | A. j e. ( F " a ) j R w } | A. u e. { w e. A | A. j e. ( F " a ) j R w } -. u R v } C_ { w e. A | A. j e. ( F " a ) j R w } |
20 |
|
ssrab2 |
|- { w e. A | A. j e. ( F " a ) j R w } C_ A |
21 |
19 20
|
sstri |
|- { v e. { w e. A | A. j e. ( F " a ) j R w } | A. u e. { w e. A | A. j e. ( F " a ) j R w } -. u R v } C_ A |
22 |
1 2 3 4 5 6 7
|
ordtypelem3 |
|- ( ( ph /\ a e. ( T i^i dom F ) ) -> ( F ` a ) e. { v e. { w e. A | A. j e. ( F " a ) j R w } | A. u e. { w e. A | A. j e. ( F " a ) j R w } -. u R v } ) |
23 |
21 22
|
sselid |
|- ( ( ph /\ a e. ( T i^i dom F ) ) -> ( F ` a ) e. A ) |
24 |
18 23
|
eqeltrd |
|- ( ( ph /\ a e. ( T i^i dom F ) ) -> ( ( F |` T ) ` a ) e. A ) |
25 |
24
|
ralrimiva |
|- ( ph -> A. a e. ( T i^i dom F ) ( ( F |` T ) ` a ) e. A ) |
26 |
|
ffnfv |
|- ( ( F |` T ) : ( T i^i dom F ) --> A <-> ( ( F |` T ) Fn ( T i^i dom F ) /\ A. a e. ( T i^i dom F ) ( ( F |` T ) ` a ) e. A ) ) |
27 |
15 25 26
|
sylanbrc |
|- ( ph -> ( F |` T ) : ( T i^i dom F ) --> A ) |
28 |
1 2 3 4 5 6 7
|
ordtypelem1 |
|- ( ph -> O = ( F |` T ) ) |
29 |
28
|
feq1d |
|- ( ph -> ( O : ( T i^i dom F ) --> A <-> ( F |` T ) : ( T i^i dom F ) --> A ) ) |
30 |
27 29
|
mpbird |
|- ( ph -> O : ( T i^i dom F ) --> A ) |