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 bitrid 
 |-  ( 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 } )