MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ordtypelem2 Structured version   Unicode version

Theorem ordtypelem2 7956
Description: Lemma for ordtype 7969. (Contributed by Mario Carneiro, 24-Jun-2015.)
Hypotheses
Ref Expression
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
Ref Expression
ordtypelem2  |-  ( ph  ->  Ord  T )
Distinct variable groups:    v, u, C    h, j, t, u, v, w, x, z, R    A, h, j, t, u, v, w, x, z    t, O, u, v, x    ph, t, x    h, F, j, t, u, v, w, x, z
Allowed substitution hints:    ph( z, w, v, u, h, j)    C( x, z, w, t, h, j)    T( x, z, w, v, u, t, h, j)    G( x, z, w, v, u, t, h, j)    O( z, w, h, j)

Proof of Theorem ordtypelem2
Dummy variable  a is distinct from all other variables.
StepHypRef Expression
1 ordtypelem.5 . . . . . . . . . 10  |-  T  =  { x  e.  On  |  E. t  e.  A  A. z  e.  ( F " x ) z R t }
2 ssrab2 3590 . . . . . . . . . 10  |-  { x  e.  On  |  E. t  e.  A  A. z  e.  ( F " x
) z R t }  C_  On
31, 2eqsstri 3539 . . . . . . . . 9  |-  T  C_  On
43a1i 11 . . . . . . . 8  |-  ( ph  ->  T  C_  On )
54sselda 3509 . . . . . . 7  |-  ( (
ph  /\  a  e.  T )  ->  a  e.  On )
6 onss 6621 . . . . . . 7  |-  ( a  e.  On  ->  a  C_  On )
75, 6syl 16 . . . . . 6  |-  ( (
ph  /\  a  e.  T )  ->  a  C_  On )
8 eloni 4894 . . . . . . . 8  |-  ( a  e.  On  ->  Ord  a )
95, 8syl 16 . . . . . . 7  |-  ( (
ph  /\  a  e.  T )  ->  Ord  a )
10 imaeq2 5339 . . . . . . . . . . . 12  |-  ( x  =  a  ->  ( F " x )  =  ( F " a
) )
1110raleqdv 3069 . . . . . . . . . . 11  |-  ( x  =  a  ->  ( A. z  e.  ( F " x ) z R t  <->  A. z  e.  ( F " a
) z R t ) )
1211rexbidv 2978 . . . . . . . . . 10  |-  ( x  =  a  ->  ( E. t  e.  A  A. z  e.  ( F " x ) z R t  <->  E. t  e.  A  A. z  e.  ( F " a
) z R t ) )
1312, 1elrab2 3268 . . . . . . . . 9  |-  ( a  e.  T  <->  ( a  e.  On  /\  E. t  e.  A  A. z  e.  ( F " a
) z R t ) )
1413simprbi 464 . . . . . . . 8  |-  ( a  e.  T  ->  E. t  e.  A  A. z  e.  ( F " a
) z R t )
1514adantl 466 . . . . . . 7  |-  ( (
ph  /\  a  e.  T )  ->  E. t  e.  A  A. z  e.  ( F " a
) z R t )
16 ordelss 4900 . . . . . . . . 9  |-  ( ( Ord  a  /\  x  e.  a )  ->  x  C_  a )
17 imass2 5378 . . . . . . . . 9  |-  ( x 
C_  a  ->  ( F " x )  C_  ( F " a ) )
18 ssralv 3569 . . . . . . . . . 10  |-  ( ( F " x ) 
C_  ( F "
a )  ->  ( A. z  e.  ( F " a ) z R t  ->  A. z  e.  ( F " x
) z R t ) )
1918reximdv 2941 . . . . . . . . 9  |-  ( ( F " x ) 
C_  ( F "
a )  ->  ( E. t  e.  A  A. z  e.  ( F " a ) z R t  ->  E. t  e.  A  A. z  e.  ( F " x
) z R t ) )
2016, 17, 193syl 20 . . . . . . . 8  |-  ( ( Ord  a  /\  x  e.  a )  ->  ( E. t  e.  A  A. z  e.  ( F " a ) z R t  ->  E. t  e.  A  A. z  e.  ( F " x
) z R t ) )
2120ralrimdva 2885 . . . . . . 7  |-  ( Ord  a  ->  ( E. t  e.  A  A. z  e.  ( F " a ) z R t  ->  A. x  e.  a  E. t  e.  A  A. z  e.  ( F " x
) z R t ) )
229, 15, 21sylc 60 . . . . . 6  |-  ( (
ph  /\  a  e.  T )  ->  A. x  e.  a  E. t  e.  A  A. z  e.  ( F " x
) z R t )
23 ssrab 3583 . . . . . 6  |-  ( a 
C_  { x  e.  On  |  E. t  e.  A  A. z  e.  ( F " x
) z R t }  <->  ( a  C_  On  /\  A. x  e.  a  E. t  e.  A  A. z  e.  ( F " x
) z R t ) )
247, 22, 23sylanbrc 664 . . . . 5  |-  ( (
ph  /\  a  e.  T )  ->  a  C_ 
{ x  e.  On  |  E. t  e.  A  A. z  e.  ( F " x ) z R t } )
2524, 1syl6sseqr 3556 . . . 4  |-  ( (
ph  /\  a  e.  T )  ->  a  C_  T )
2625ralrimiva 2881 . . 3  |-  ( ph  ->  A. a  e.  T  a  C_  T )
27 dftr3 4550 . . 3  |-  ( Tr  T  <->  A. a  e.  T  a  C_  T )
2826, 27sylibr 212 . 2  |-  ( ph  ->  Tr  T )
29 ordon 6613 . . 3  |-  Ord  On
30 trssord 4901 . . 3  |-  ( ( Tr  T  /\  T  C_  On  /\  Ord  On )  ->  Ord  T )
313, 29, 30mp3an23 1316 . 2  |-  ( Tr  T  ->  Ord  T )
3228, 31syl 16 1  |-  ( ph  ->  Ord  T )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    = wceq 1379    e. wcel 1767   A.wral 2817   E.wrex 2818   {crab 2821   _Vcvv 3118    C_ wss 3481   class class class wbr 4453    |-> cmpt 4511   Tr wtr 4546   Se wse 4842    We wwe 4843   Ord word 4883   Oncon0 4884   ran crn 5006   "cima 5008   iota_crio 6255  recscrecs 7053  OrdIsocoi 7946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pr 4692  ax-un 6587
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-br 4454  df-opab 4512  df-tr 4547  df-eprel 4797  df-po 4806  df-so 4807  df-fr 4844  df-we 4846  df-ord 4887  df-on 4888  df-xp 5011  df-cnv 5013  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018
This theorem is referenced by:  ordtypelem5  7959  ordtypelem6  7960  ordtypelem7  7961  ordtypelem8  7962  ordtypelem9  7963
  Copyright terms: Public domain W3C validator