Metamath Proof Explorer


Theorem ordtypelem4

Description: Lemma for ordtype . (Contributed by Mario Carneiro, 24-Jun-2015)

Ref Expression
Hypotheses ordtypelem.1
|- F = recs ( G )
ordtypelem.2
|- C = { w e. A | A. j e. ran h j R w }
ordtypelem.3
|- G = ( h e. _V |-> ( iota_ v e. C A. u e. C -. u R v ) )
ordtypelem.5
|- T = { x e. On | E. t e. A A. z e. ( F " x ) z R t }
ordtypelem.6
|- O = OrdIso ( R , A )
ordtypelem.7
|- ( ph -> R We A )
ordtypelem.8
|- ( ph -> R Se A )
Assertion ordtypelem4
|- ( ph -> O : ( T i^i dom F ) --> A )

Proof

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 )