Metamath Proof Explorer


Theorem ordtypelem3

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 ordtypelem3
|- ( ( ph /\ M e. ( T i^i dom F ) ) -> ( F ` M ) e. { v e. { w e. A | A. j e. ( F " M ) j R w } | A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v } )

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 simpr
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> M e. ( T i^i dom F ) )
9 8 elin2d
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> M e. dom F )
10 1 tfr2a
 |-  ( M e. dom F -> ( F ` M ) = ( G ` ( F |` M ) ) )
11 9 10 syl
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> ( F ` M ) = ( G ` ( F |` M ) ) )
12 1 tfr1a
 |-  ( Fun F /\ Lim dom F )
13 12 simpri
 |-  Lim dom F
14 limord
 |-  ( Lim dom F -> Ord dom F )
15 13 14 ax-mp
 |-  Ord dom F
16 ordelord
 |-  ( ( Ord dom F /\ M e. dom F ) -> Ord M )
17 15 9 16 sylancr
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> Ord M )
18 1 tfr2b
 |-  ( Ord M -> ( M e. dom F <-> ( F |` M ) e. _V ) )
19 17 18 syl
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> ( M e. dom F <-> ( F |` M ) e. _V ) )
20 9 19 mpbid
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> ( F |` M ) e. _V )
21 rneq
 |-  ( h = ( F |` M ) -> ran h = ran ( F |` M ) )
22 df-ima
 |-  ( F " M ) = ran ( F |` M )
23 21 22 eqtr4di
 |-  ( h = ( F |` M ) -> ran h = ( F " M ) )
24 23 raleqdv
 |-  ( h = ( F |` M ) -> ( A. j e. ran h j R w <-> A. j e. ( F " M ) j R w ) )
25 24 rabbidv
 |-  ( h = ( F |` M ) -> { w e. A | A. j e. ran h j R w } = { w e. A | A. j e. ( F " M ) j R w } )
26 2 25 eqtrid
 |-  ( h = ( F |` M ) -> C = { w e. A | A. j e. ( F " M ) j R w } )
27 26 raleqdv
 |-  ( h = ( F |` M ) -> ( A. u e. C -. u R v <-> A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v ) )
28 26 27 riotaeqbidv
 |-  ( h = ( F |` M ) -> ( iota_ v e. C A. u e. C -. u R v ) = ( iota_ v e. { w e. A | A. j e. ( F " M ) j R w } A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v ) )
29 riotaex
 |-  ( iota_ v e. { w e. A | A. j e. ( F " M ) j R w } A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v ) e. _V
30 28 3 29 fvmpt
 |-  ( ( F |` M ) e. _V -> ( G ` ( F |` M ) ) = ( iota_ v e. { w e. A | A. j e. ( F " M ) j R w } A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v ) )
31 20 30 syl
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> ( G ` ( F |` M ) ) = ( iota_ v e. { w e. A | A. j e. ( F " M ) j R w } A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v ) )
32 11 31 eqtrd
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> ( F ` M ) = ( iota_ v e. { w e. A | A. j e. ( F " M ) j R w } A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v ) )
33 6 adantr
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> R We A )
34 7 adantr
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> R Se A )
35 ssrab2
 |-  { w e. A | A. j e. ( F " M ) j R w } C_ A
36 35 a1i
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> { w e. A | A. j e. ( F " M ) j R w } C_ A )
37 8 elin1d
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> M e. T )
38 imaeq2
 |-  ( x = M -> ( F " x ) = ( F " M ) )
39 38 raleqdv
 |-  ( x = M -> ( A. z e. ( F " x ) z R t <-> A. z e. ( F " M ) z R t ) )
40 39 rexbidv
 |-  ( x = M -> ( E. t e. A A. z e. ( F " x ) z R t <-> E. t e. A A. z e. ( F " M ) z R t ) )
41 40 4 elrab2
 |-  ( M e. T <-> ( M e. On /\ E. t e. A A. z e. ( F " M ) z R t ) )
42 41 simprbi
 |-  ( M e. T -> E. t e. A A. z e. ( F " M ) z R t )
43 37 42 syl
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> E. t e. A A. z e. ( F " M ) z R t )
44 breq1
 |-  ( j = z -> ( j R w <-> z R w ) )
45 44 cbvralvw
 |-  ( A. j e. ( F " M ) j R w <-> A. z e. ( F " M ) z R w )
46 breq2
 |-  ( w = t -> ( z R w <-> z R t ) )
47 46 ralbidv
 |-  ( w = t -> ( A. z e. ( F " M ) z R w <-> A. z e. ( F " M ) z R t ) )
48 45 47 syl5bb
 |-  ( w = t -> ( A. j e. ( F " M ) j R w <-> A. z e. ( F " M ) z R t ) )
49 48 cbvrexvw
 |-  ( E. w e. A A. j e. ( F " M ) j R w <-> E. t e. A A. z e. ( F " M ) z R t )
50 43 49 sylibr
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> E. w e. A A. j e. ( F " M ) j R w )
51 rabn0
 |-  ( { w e. A | A. j e. ( F " M ) j R w } =/= (/) <-> E. w e. A A. j e. ( F " M ) j R w )
52 50 51 sylibr
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> { w e. A | A. j e. ( F " M ) j R w } =/= (/) )
53 wereu2
 |-  ( ( ( R We A /\ R Se A ) /\ ( { w e. A | A. j e. ( F " M ) j R w } C_ A /\ { w e. A | A. j e. ( F " M ) j R w } =/= (/) ) ) -> E! v e. { w e. A | A. j e. ( F " M ) j R w } A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v )
54 33 34 36 52 53 syl22anc
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> E! v e. { w e. A | A. j e. ( F " M ) j R w } A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v )
55 riotacl2
 |-  ( E! v e. { w e. A | A. j e. ( F " M ) j R w } A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v -> ( iota_ v e. { w e. A | A. j e. ( F " M ) j R w } A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v ) e. { v e. { w e. A | A. j e. ( F " M ) j R w } | A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v } )
56 54 55 syl
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> ( iota_ v e. { w e. A | A. j e. ( F " M ) j R w } A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v ) e. { v e. { w e. A | A. j e. ( F " M ) j R w } | A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v } )
57 32 56 eqeltrd
 |-  ( ( ph /\ M e. ( T i^i dom F ) ) -> ( F ` M ) e. { v e. { w e. A | A. j e. ( F " M ) j R w } | A. u e. { w e. A | A. j e. ( F " M ) j R w } -. u R v } )