Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ordelordALT Unicode version

Theorem ordelordALT 27338
Description: An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 4372 using the Axiom of Regularity indirectly through dford2 7275. dford2 is a weaker definition of ordinal number. Given the Axiom of Regularity, it need not be assumed that  _E  Fr  A because this is inferred by the Axiom of Regularity. ordelordALT 27338 is ordelordALTVD 27677 without virtual deductions and was automatically derived from ordelordALTVD 27677 using the tools program translate..without..overwriting.cmd and Metamath's minimize command. (Contributed by Alan Sare, 18-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ordelordALT  |-  ( ( Ord  A  /\  B  e.  A )  ->  Ord  B )

Proof of Theorem ordelordALT
StepHypRef Expression
1 ordtr 4364 . . . 4  |-  ( Ord 
A  ->  Tr  A
)
21adantr 453 . . 3  |-  ( ( Ord  A  /\  B  e.  A )  ->  Tr  A )
3 dford2 7275 . . . . . 6  |-  ( Ord 
A  <->  ( Tr  A  /\  A. x  e.  A  A. y  e.  A  ( x  e.  y  \/  x  =  y  \/  y  e.  x
) ) )
43simprbi 452 . . . . 5  |-  ( Ord 
A  ->  A. x  e.  A  A. y  e.  A  ( x  e.  y  \/  x  =  y  \/  y  e.  x ) )
54adantr 453 . . . 4  |-  ( ( Ord  A  /\  B  e.  A )  ->  A. x  e.  A  A. y  e.  A  ( x  e.  y  \/  x  =  y  \/  y  e.  x ) )
6 3orcomb 949 . . . . 5  |-  ( ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <-> 
( x  e.  y  \/  y  e.  x  \/  x  =  y
) )
762ralbii 2542 . . . 4  |-  ( A. x  e.  A  A. y  e.  A  (
x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  A. x  e.  A  A. y  e.  A  ( x  e.  y  \/  y  e.  x  \/  x  =  y
) )
85, 7sylib 190 . . 3  |-  ( ( Ord  A  /\  B  e.  A )  ->  A. x  e.  A  A. y  e.  A  ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
9 simpr 449 . . 3  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  e.  A )
10 tratrb 27336 . . 3  |-  ( ( Tr  A  /\  A. x  e.  A  A. y  e.  A  (
x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A
)  ->  Tr  B
)
112, 8, 9, 10syl3anc 1187 . 2  |-  ( ( Ord  A  /\  B  e.  A )  ->  Tr  B )
12 trss 4082 . . . 4  |-  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A ) )
132, 9, 12sylc 58 . . 3  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  C_  A )
14 ssralv2 27331 . . . 4  |-  ( ( B  C_  A  /\  B  C_  A )  -> 
( A. x  e.  A  A. y  e.  A  ( x  e.  y  \/  x  =  y  \/  y  e.  x )  ->  A. x  e.  B  A. y  e.  B  ( x  e.  y  \/  x  =  y  \/  y  e.  x ) ) )
1514ex 425 . . 3  |-  ( B 
C_  A  ->  ( B  C_  A  ->  ( A. x  e.  A  A. y  e.  A  ( x  e.  y  \/  x  =  y  \/  y  e.  x
)  ->  A. x  e.  B  A. y  e.  B  ( x  e.  y  \/  x  =  y  \/  y  e.  x ) ) ) )
1613, 13, 5, 15syl3c 59 . 2  |-  ( ( Ord  A  /\  B  e.  A )  ->  A. x  e.  B  A. y  e.  B  ( x  e.  y  \/  x  =  y  \/  y  e.  x ) )
17 dford2 7275 . 2  |-  ( Ord 
B  <->  ( Tr  B  /\  A. x  e.  B  A. y  e.  B  ( x  e.  y  \/  x  =  y  \/  y  e.  x
) ) )
1811, 16, 17sylanbrc 648 1  |-  ( ( Ord  A  /\  B  e.  A )  ->  Ord  B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    /\ wa 360    \/ w3o 938    e. wcel 1621   A.wral 2516    C_ wss 3113   Tr wtr 4073   Ord word 4349
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4101  ax-nul 4109  ax-pr 4172  ax-un 4470  ax-reg 7260
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2521  df-rex 2522  df-rab 2525  df-v 2759  df-sbc 2953  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-tp 3608  df-op 3609  df-uni 3788  df-br 3984  df-opab 4038  df-tr 4074  df-eprel 4263  df-po 4272  df-so 4273  df-fr 4310  df-we 4312  df-ord 4353
  Copyright terms: Public domain W3C validator