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

Theorem ordelordALTVD 27923
Description: An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 4413 using the Axiom of Regularity indirectly through dford2 7317. 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. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. ordelordALT 27584 is ordelordALTVD 27923 without virtual deductions and was automatically derived from ordelordALTVD 27923 using the tools program translate..without..overwriting.cmd and Metamath's minimize command.
1::  |-  (. ( Ord  A  /\  B  e.  A )  ->.  ( Ord  A  /\  B  e.  A ) ).
2:1:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  Ord  A ).
3:1:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  B  e.  A ).
4:2:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  Tr  A ).
5:2:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  x  =  y  \/  y  e.  x ) ).
6:4,3:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  B  C_  A ).
7:6,6,5:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  A. x  e.  B  A. y  e.  B ( x  e.  y  \/  x  =  y  \/  y  e.  x ) ).
8::  |-  ( ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
9:8:  |-  A. y ( ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
10:9:  |-  A. y  e.  A ( ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
11:10:  |-  ( A. y  e.  A ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
12:11:  |-  A. x ( A. y  e.  A ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
13:12:  |-  A. x  e.  A ( A. y  e.  A ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
14:13:  |-  ( 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 ) )
15:14,5:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  A. x  e.  A  A. y  e.  A ( x  e.  y  \/  y  e.  x  \/  x  =  y ) ).
16:4,15,3:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  Tr  B ).
17:16,7:  |-  (. ( Ord  A  /\  B  e.  A )  ->.  Ord  B ).
qed:17:  |-  ( ( Ord  A  /\  B  e.  A )  ->  Ord  B )
(Contributed by Alan Sare, 12-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
ordelordALTVD  |-  ( ( Ord  A  /\  B  e.  A )  ->  Ord  B )

Proof of Theorem ordelordALTVD
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idn1 27625 . . . . . 6  |-  (. ( Ord  A  /\  B  e.  A )  ->.  ( Ord  A  /\  B  e.  A
) ).
2 simpl 443 . . . . . 6  |-  ( ( Ord  A  /\  B  e.  A )  ->  Ord  A )
31, 2e1_ 27679 . . . . 5  |-  (. ( Ord  A  /\  B  e.  A )  ->.  Ord  A ).
4 ordtr 4405 . . . . 5  |-  ( Ord 
A  ->  Tr  A
)
53, 4e1_ 27679 . . . 4  |-  (. ( Ord  A  /\  B  e.  A )  ->.  Tr  A ).
6 dford2 7317 . . . . . . 7  |-  ( Ord 
A  <->  ( Tr  A  /\  A. x  e.  A  A. y  e.  A  ( x  e.  y  \/  x  =  y  \/  y  e.  x
) ) )
76simprbi 450 . . . . . 6  |-  ( Ord 
A  ->  A. x  e.  A  A. y  e.  A  ( x  e.  y  \/  x  =  y  \/  y  e.  x ) )
83, 7e1_ 27679 . . . . 5  |-  (. ( Ord  A  /\  B  e.  A )  ->.  A. x  e.  A  A. y  e.  A  ( x  e.  y  \/  x  =  y  \/  y  e.  x ) ).
9 3orcomb 944 . . . . . . . . . . 11  |-  ( ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <-> 
( x  e.  y  \/  y  e.  x  \/  x  =  y
) )
109ax-gen 1533 . . . . . . . . . 10  |-  A. y
( ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
11 alral 2602 . . . . . . . . . 10  |-  ( A. y ( ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )  ->  A. y  e.  A  ( ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  ( x  e.  y  \/  y  e.  x  \/  x  =  y ) ) )
1210, 11e0_ 27827 . . . . . . . . 9  |-  A. y  e.  A  ( (
x  e.  y  \/  x  =  y  \/  y  e.  x )  <-> 
( x  e.  y  \/  y  e.  x  \/  x  =  y
) )
13 ralbi 2680 . . . . . . . . 9  |-  ( A. y  e.  A  (
( x  e.  y  \/  x  =  y  \/  y  e.  x
)  <->  ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )  -> 
( A. y  e.  A  ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  A. y  e.  A  ( x  e.  y  \/  y  e.  x  \/  x  =  y ) ) )
1412, 13e0_ 27827 . . . . . . . 8  |-  ( A. y  e.  A  (
x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  A. y  e.  A  ( x  e.  y  \/  y  e.  x  \/  x  =  y
) )
1514ax-gen 1533 . . . . . . 7  |-  A. x
( A. y  e.  A  ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  A. y  e.  A  ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
16 alral 2602 . . . . . . 7  |-  ( A. x ( A. y  e.  A  ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  A. y  e.  A  ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )  ->  A. x  e.  A  ( A. y  e.  A  ( x  e.  y  \/  x  =  y  \/  y  e.  x
)  <->  A. y  e.  A  ( x  e.  y  \/  y  e.  x  \/  x  =  y
) ) )
1715, 16e0_ 27827 . . . . . 6  |-  A. x  e.  A  ( A. y  e.  A  (
x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  A. y  e.  A  ( x  e.  y  \/  y  e.  x  \/  x  =  y
) )
18 ralbi 2680 . . . . . 6  |-  ( A. x  e.  A  ( A. y  e.  A  ( x  e.  y  \/  x  =  y  \/  y  e.  x
)  <->  A. y  e.  A  ( x  e.  y  \/  y  e.  x  \/  x  =  y
) )  ->  ( 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
) ) )
1917, 18e0_ 27827 . . . . 5  |-  ( 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
) )
208, 19e1bi 27681 . . . 4  |-  (. ( Ord  A  /\  B  e.  A )  ->.  A. x  e.  A  A. y  e.  A  ( x  e.  y  \/  y  e.  x  \/  x  =  y ) ).
21 simpr 447 . . . . 5  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  e.  A )
221, 21e1_ 27679 . . . 4  |-  (. ( Ord  A  /\  B  e.  A )  ->.  B  e.  A ).
23 tratrb 27582 . . . . 5  |-  ( ( Tr  A  /\  A. x  e.  A  A. y  e.  A  (
x  e.  y  \/  y  e.  x  \/  x  =  y )  /\  B  e.  A
)  ->  Tr  B
)
24233exp 1150 . . . 4  |-  ( Tr  A  ->  ( A. x  e.  A  A. y  e.  A  (
x  e.  y  \/  y  e.  x  \/  x  =  y )  ->  ( B  e.  A  ->  Tr  B
) ) )
255, 20, 22, 24e111 27726 . . 3  |-  (. ( Ord  A  /\  B  e.  A )  ->.  Tr  B ).
26 trss 4123 . . . . 5  |-  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A ) )
275, 22, 26e11 27740 . . . 4  |-  (. ( Ord  A  /\  B  e.  A )  ->.  B  C_  A ).
28 ssralv2 27577 . . . . 5  |-  ( ( 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 ) ) )
2928ex 423 . . . 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 ) ) ) )
3027, 27, 8, 29e111 27726 . . 3  |-  (. ( Ord  A  /\  B  e.  A )  ->.  A. x  e.  B  A. y  e.  B  ( x  e.  y  \/  x  =  y  \/  y  e.  x ) ).
31 dford2 7317 . . . 4  |-  ( Ord 
B  <->  ( Tr  B  /\  A. x  e.  B  A. y  e.  B  ( x  e.  y  \/  x  =  y  \/  y  e.  x
) ) )
3231simplbi2 608 . . 3  |-  ( Tr  B  ->  ( A. x  e.  B  A. y  e.  B  (
x  e.  y  \/  x  =  y  \/  y  e.  x )  ->  Ord  B )
)
3325, 30, 32e11 27740 . 2  |-  (. ( Ord  A  /\  B  e.  A )  ->.  Ord  B ).
3433in1 27622 1  |-  ( ( Ord  A  /\  B  e.  A )  ->  Ord  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    \/ w3o 933   A.wal 1527    = wceq 1623    e. wcel 1685   A.wral 2544    C_ wss 3153   Tr wtr 4114   Ord word 4390
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1636  ax-8 1644  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213  ax-un 4511  ax-reg 7302
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1631  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-sbc 2993  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-tp 3649  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-tr 4115  df-eprel 4304  df-po 4313  df-so 4314  df-fr 4351  df-we 4353  df-ord 4394  df-vd1 27621
  Copyright terms: Public domain W3C validator