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

Theorem ordelord 4762
Description: An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. (Contributed by NM, 23-Apr-1994.)
Assertion
Ref Expression
ordelord  |-  ( ( Ord  A  /\  B  e.  A )  ->  Ord  B )

Proof of Theorem ordelord
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq1 2503 . . . . 5  |-  ( x  =  B  ->  (
x  e.  A  <->  B  e.  A ) )
21anbi2d 703 . . . 4  |-  ( x  =  B  ->  (
( Ord  A  /\  x  e.  A )  <->  ( Ord  A  /\  B  e.  A ) ) )
3 ordeq 4747 . . . 4  |-  ( x  =  B  ->  ( Ord  x  <->  Ord  B ) )
42, 3imbi12d 320 . . 3  |-  ( x  =  B  ->  (
( ( Ord  A  /\  x  e.  A
)  ->  Ord  x )  <-> 
( ( Ord  A  /\  B  e.  A
)  ->  Ord  B ) ) )
5 simpll 753 . . . . . . . . 9  |-  ( ( ( Ord  A  /\  x  e.  A )  /\  ( z  e.  y  /\  y  e.  x
) )  ->  Ord  A )
6 3anrot 970 . . . . . . . . . . . 12  |-  ( ( x  e.  A  /\  z  e.  y  /\  y  e.  x )  <->  ( z  e.  y  /\  y  e.  x  /\  x  e.  A )
)
7 3anass 969 . . . . . . . . . . . 12  |-  ( ( x  e.  A  /\  z  e.  y  /\  y  e.  x )  <->  ( x  e.  A  /\  ( z  e.  y  /\  y  e.  x
) ) )
86, 7bitr3i 251 . . . . . . . . . . 11  |-  ( ( z  e.  y  /\  y  e.  x  /\  x  e.  A )  <->  ( x  e.  A  /\  ( z  e.  y  /\  y  e.  x
) ) )
9 ordtr 4754 . . . . . . . . . . . 12  |-  ( Ord 
A  ->  Tr  A
)
10 trel3 4414 . . . . . . . . . . . 12  |-  ( Tr  A  ->  ( (
z  e.  y  /\  y  e.  x  /\  x  e.  A )  ->  z  e.  A ) )
119, 10syl 16 . . . . . . . . . . 11  |-  ( Ord 
A  ->  ( (
z  e.  y  /\  y  e.  x  /\  x  e.  A )  ->  z  e.  A ) )
128, 11syl5bir 218 . . . . . . . . . 10  |-  ( Ord 
A  ->  ( (
x  e.  A  /\  ( z  e.  y  /\  y  e.  x
) )  ->  z  e.  A ) )
1312impl 620 . . . . . . . . 9  |-  ( ( ( Ord  A  /\  x  e.  A )  /\  ( z  e.  y  /\  y  e.  x
) )  ->  z  e.  A )
14 trel 4413 . . . . . . . . . . . . 13  |-  ( Tr  A  ->  ( (
y  e.  x  /\  x  e.  A )  ->  y  e.  A ) )
159, 14syl 16 . . . . . . . . . . . 12  |-  ( Ord 
A  ->  ( (
y  e.  x  /\  x  e.  A )  ->  y  e.  A ) )
1615expcomd 438 . . . . . . . . . . 11  |-  ( Ord 
A  ->  ( x  e.  A  ->  ( y  e.  x  ->  y  e.  A ) ) )
1716imp31 432 . . . . . . . . . 10  |-  ( ( ( Ord  A  /\  x  e.  A )  /\  y  e.  x
)  ->  y  e.  A )
1817adantrl 715 . . . . . . . . 9  |-  ( ( ( Ord  A  /\  x  e.  A )  /\  ( z  e.  y  /\  y  e.  x
) )  ->  y  e.  A )
19 simplr 754 . . . . . . . . 9  |-  ( ( ( Ord  A  /\  x  e.  A )  /\  ( z  e.  y  /\  y  e.  x
) )  ->  x  e.  A )
20 ordwe 4753 . . . . . . . . . 10  |-  ( Ord 
A  ->  _E  We  A )
21 wetrep 4734 . . . . . . . . . 10  |-  ( (  _E  We  A  /\  ( z  e.  A  /\  y  e.  A  /\  x  e.  A
) )  ->  (
( z  e.  y  /\  y  e.  x
)  ->  z  e.  x ) )
2220, 21sylan 471 . . . . . . . . 9  |-  ( ( Ord  A  /\  (
z  e.  A  /\  y  e.  A  /\  x  e.  A )
)  ->  ( (
z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
235, 13, 18, 19, 22syl13anc 1220 . . . . . . . 8  |-  ( ( ( Ord  A  /\  x  e.  A )  /\  ( z  e.  y  /\  y  e.  x
) )  ->  (
( z  e.  y  /\  y  e.  x
)  ->  z  e.  x ) )
2423ex 434 . . . . . . 7  |-  ( ( Ord  A  /\  x  e.  A )  ->  (
( z  e.  y  /\  y  e.  x
)  ->  ( (
z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) )
2524pm2.43d 48 . . . . . 6  |-  ( ( Ord  A  /\  x  e.  A )  ->  (
( z  e.  y  /\  y  e.  x
)  ->  z  e.  x ) )
2625alrimivv 1686 . . . . 5  |-  ( ( Ord  A  /\  x  e.  A )  ->  A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
27 dftr2 4408 . . . . 5  |-  ( Tr  x  <->  A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
2826, 27sylibr 212 . . . 4  |-  ( ( Ord  A  /\  x  e.  A )  ->  Tr  x )
29 trss 4415 . . . . . . 7  |-  ( Tr  A  ->  ( x  e.  A  ->  x  C_  A ) )
309, 29syl 16 . . . . . 6  |-  ( Ord 
A  ->  ( x  e.  A  ->  x  C_  A ) )
31 wess 4728 . . . . . . 7  |-  ( x 
C_  A  ->  (  _E  We  A  ->  _E  We  x ) )
3220, 31syl5com 30 . . . . . 6  |-  ( Ord 
A  ->  ( x  C_  A  ->  _E  We  x ) )
3330, 32syld 44 . . . . 5  |-  ( Ord 
A  ->  ( x  e.  A  ->  _E  We  x ) )
3433imp 429 . . . 4  |-  ( ( Ord  A  /\  x  e.  A )  ->  _E  We  x )
35 df-ord 4743 . . . 4  |-  ( Ord  x  <->  ( Tr  x  /\  _E  We  x ) )
3628, 34, 35sylanbrc 664 . . 3  |-  ( ( Ord  A  /\  x  e.  A )  ->  Ord  x )
374, 36vtoclg 3051 . 2  |-  ( B  e.  A  ->  (
( Ord  A  /\  B  e.  A )  ->  Ord  B ) )
3837anabsi7 815 1  |-  ( ( Ord  A  /\  B  e.  A )  ->  Ord  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    /\ w3a 965   A.wal 1367    = wceq 1369    e. wcel 1756    C_ wss 3349   Tr wtr 4406    _E cep 4651    We wwe 4699   Ord word 4739
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pr 4552
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-tr 4407  df-eprel 4653  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743
This theorem is referenced by:  tron  4763  ordelon  4764  ordtr2  4784  ordtr3  4785  ordintdif  4789  ordsuc  6446  ordsucss  6450  ordsucelsuc  6454  ordsucuniel  6456  limsssuc  6482  smores  6834  smo11  6846  smoord  6847  smoword  6848  smogt  6849  smorndom  6850  rdglim2  6909  oesuclem  6986  ordtypelem3  7755  r1val1  8014  rankr1ag  8030  fin23lem24  8512  onsuct0  28309  dford3  29403  ordpss  29733
  Copyright terms: Public domain W3C validator