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

Theorem ordelord 5464
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 2495 . . . . 5  |-  ( x  =  B  ->  (
x  e.  A  <->  B  e.  A ) )
21anbi2d 708 . . . 4  |-  ( x  =  B  ->  (
( Ord  A  /\  x  e.  A )  <->  ( Ord  A  /\  B  e.  A ) ) )
3 ordeq 5449 . . . 4  |-  ( x  =  B  ->  ( Ord  x  <->  Ord  B ) )
42, 3imbi12d 321 . . 3  |-  ( x  =  B  ->  (
( ( Ord  A  /\  x  e.  A
)  ->  Ord  x )  <-> 
( ( Ord  A  /\  B  e.  A
)  ->  Ord  B ) ) )
5 simpll 758 . . . . . . . . 9  |-  ( ( ( Ord  A  /\  x  e.  A )  /\  ( z  e.  y  /\  y  e.  x
) )  ->  Ord  A )
6 3anrot 987 . . . . . . . . . . . 12  |-  ( ( x  e.  A  /\  z  e.  y  /\  y  e.  x )  <->  ( z  e.  y  /\  y  e.  x  /\  x  e.  A )
)
7 3anass 986 . . . . . . . . . . . 12  |-  ( ( x  e.  A  /\  z  e.  y  /\  y  e.  x )  <->  ( x  e.  A  /\  ( z  e.  y  /\  y  e.  x
) ) )
86, 7bitr3i 254 . . . . . . . . . . 11  |-  ( ( z  e.  y  /\  y  e.  x  /\  x  e.  A )  <->  ( x  e.  A  /\  ( z  e.  y  /\  y  e.  x
) ) )
9 ordtr 5456 . . . . . . . . . . . 12  |-  ( Ord 
A  ->  Tr  A
)
10 trel3 4526 . . . . . . . . . . . 12  |-  ( Tr  A  ->  ( (
z  e.  y  /\  y  e.  x  /\  x  e.  A )  ->  z  e.  A ) )
119, 10syl 17 . . . . . . . . . . 11  |-  ( Ord 
A  ->  ( (
z  e.  y  /\  y  e.  x  /\  x  e.  A )  ->  z  e.  A ) )
128, 11syl5bir 221 . . . . . . . . . 10  |-  ( Ord 
A  ->  ( (
x  e.  A  /\  ( z  e.  y  /\  y  e.  x
) )  ->  z  e.  A ) )
1312impl 624 . . . . . . . . 9  |-  ( ( ( Ord  A  /\  x  e.  A )  /\  ( z  e.  y  /\  y  e.  x
) )  ->  z  e.  A )
14 trel 4525 . . . . . . . . . . . . 13  |-  ( Tr  A  ->  ( (
y  e.  x  /\  x  e.  A )  ->  y  e.  A ) )
159, 14syl 17 . . . . . . . . . . . 12  |-  ( Ord 
A  ->  ( (
y  e.  x  /\  x  e.  A )  ->  y  e.  A ) )
1615expcomd 439 . . . . . . . . . . 11  |-  ( Ord 
A  ->  ( x  e.  A  ->  ( y  e.  x  ->  y  e.  A ) ) )
1716imp31 433 . . . . . . . . . 10  |-  ( ( ( Ord  A  /\  x  e.  A )  /\  y  e.  x
)  ->  y  e.  A )
1817adantrl 720 . . . . . . . . 9  |-  ( ( ( Ord  A  /\  x  e.  A )  /\  ( z  e.  y  /\  y  e.  x
) )  ->  y  e.  A )
19 simplr 760 . . . . . . . . 9  |-  ( ( ( Ord  A  /\  x  e.  A )  /\  ( z  e.  y  /\  y  e.  x
) )  ->  x  e.  A )
20 ordwe 5455 . . . . . . . . . 10  |-  ( Ord 
A  ->  _E  We  A )
21 wetrep 4846 . . . . . . . . . 10  |-  ( (  _E  We  A  /\  ( z  e.  A  /\  y  e.  A  /\  x  e.  A
) )  ->  (
( z  e.  y  /\  y  e.  x
)  ->  z  e.  x ) )
2220, 21sylan 473 . . . . . . . . 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 1266 . . . . . . . 8  |-  ( ( ( Ord  A  /\  x  e.  A )  /\  ( z  e.  y  /\  y  e.  x
) )  ->  (
( z  e.  y  /\  y  e.  x
)  ->  z  e.  x ) )
2423ex 435 . . . . . . 7  |-  ( ( Ord  A  /\  x  e.  A )  ->  (
( z  e.  y  /\  y  e.  x
)  ->  ( (
z  e.  y  /\  y  e.  x )  ->  z  e.  x ) ) )
2524pm2.43d 50 . . . . . 6  |-  ( ( Ord  A  /\  x  e.  A )  ->  (
( z  e.  y  /\  y  e.  x
)  ->  z  e.  x ) )
2625alrimivv 1768 . . . . 5  |-  ( ( Ord  A  /\  x  e.  A )  ->  A. z A. y ( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
27 dftr2 4520 . . . . 5  |-  ( Tr  x  <->  A. z A. y
( ( z  e.  y  /\  y  e.  x )  ->  z  e.  x ) )
2826, 27sylibr 215 . . . 4  |-  ( ( Ord  A  /\  x  e.  A )  ->  Tr  x )
29 trss 4527 . . . . . . 7  |-  ( Tr  A  ->  ( x  e.  A  ->  x  C_  A ) )
309, 29syl 17 . . . . . 6  |-  ( Ord 
A  ->  ( x  e.  A  ->  x  C_  A ) )
31 wess 4840 . . . . . 6  |-  ( x 
C_  A  ->  (  _E  We  A  ->  _E  We  x ) )
3230, 20, 31syl6ci 67 . . . . 5  |-  ( Ord 
A  ->  ( x  e.  A  ->  _E  We  x ) )
3332imp 430 . . . 4  |-  ( ( Ord  A  /\  x  e.  A )  ->  _E  We  x )
34 df-ord 5445 . . . 4  |-  ( Ord  x  <->  ( Tr  x  /\  _E  We  x ) )
3528, 33, 34sylanbrc 668 . . 3  |-  ( ( Ord  A  /\  x  e.  A )  ->  Ord  x )
364, 35vtoclg 3139 . 2  |-  ( B  e.  A  ->  (
( Ord  A  /\  B  e.  A )  ->  Ord  B ) )
3736anabsi7 826 1  |-  ( ( Ord  A  /\  B  e.  A )  ->  Ord  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    /\ w3a 982   A.wal 1435    = wceq 1437    e. wcel 1872    C_ wss 3436   Tr wtr 4518    _E cep 4762    We wwe 4811   Ord word 5441
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-tr 4519  df-eprel 4764  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-ord 5445
This theorem is referenced by:  tron  5465  ordelon  5466  ordtr2  5486  ordtr3  5487  ordintdif  5491  ordsuc  6655  ordsucss  6659  ordsucelsuc  6663  ordsucuniel  6665  limsssuc  6691  smores  7082  smo11  7094  smoord  7095  smoword  7096  smogt  7097  smorndom  7098  rdglim2  7161  oesuclem  7238  ordtypelem3  8044  r1val1  8265  rankr1ag  8281  fin23lem24  8759  onsuct0  31106  dford3  35853  ordpss  36774
  Copyright terms: Public domain W3C validator