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 sseldi 
 |-  ( ( 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 )