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

Theorem ordelordALTVD 28692
Description: An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 4567 using the Axiom of Regularity indirectly through dford2 7535. 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 28337 is ordelordALTVD 28692 without virtual deductions and was automatically derived from ordelordALTVD 28692 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 28378 . . . . . 6  |-  (. ( Ord  A  /\  B  e.  A )  ->.  ( Ord  A  /\  B  e.  A
) ).
2 simpl 444 . . . . . 6  |-  ( ( Ord  A  /\  B  e.  A )  ->  Ord  A )
31, 2e1_ 28441 . . . . 5  |-  (. ( Ord  A  /\  B  e.  A )  ->.  Ord  A ).
4 ordtr 4559 . . . . 5  |-  ( Ord 
A  ->  Tr  A
)
53, 4e1_ 28441 . . . 4  |-  (. ( Ord  A  /\  B  e.  A )  ->.  Tr  A ).
6 dford2 7535 . . . . . . 7  |-  ( Ord 
A  <->  ( Tr  A  /\  A. x  e.  A  A. y  e.  A  ( x  e.  y  \/  x  =  y  \/  y  e.  x
) ) )
76simprbi 451 . . . . . 6  |-  ( Ord 
A  ->  A. x  e.  A  A. y  e.  A  ( x  e.  y  \/  x  =  y  \/  y  e.  x ) )
83, 7e1_ 28441 . . . . 5  |-  (. ( Ord  A  /\  B  e.  A )  ->.  A. x  e.  A  A. y  e.  A  ( x  e.  y  \/  x  =  y  \/  y  e.  x ) ).
9 3orcomb 946 . . . . . . . . . . 11  |-  ( ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <-> 
( x  e.  y  \/  y  e.  x  \/  x  =  y
) )
109ax-gen 1552 . . . . . . . . . 10  |-  A. y
( ( x  e.  y  \/  x  =  y  \/  y  e.  x )  <->  ( x  e.  y  \/  y  e.  x  \/  x  =  y ) )
11 alral 2728 . . . . . . . . . 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_ 28597 . . . . . . . . 9  |-  A. y  e.  A  ( (
x  e.  y  \/  x  =  y  \/  y  e.  x )  <-> 
( x  e.  y  \/  y  e.  x  \/  x  =  y
) )
13 ralbi 2806 . . . . . . . . 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_ 28597 . . . . . . . 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 1552 . . . . . . 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 2728 . . . . . . 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_ 28597 . . . . . 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 2806 . . . . . 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_ 28597 . . . . 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 28443 . . . 4  |-  (. ( Ord  A  /\  B  e.  A )  ->.  A. x  e.  A  A. y  e.  A  ( x  e.  y  \/  y  e.  x  \/  x  =  y ) ).
21 simpr 448 . . . . 5  |-  ( ( Ord  A  /\  B  e.  A )  ->  B  e.  A )
221, 21e1_ 28441 . . . 4  |-  (. ( Ord  A  /\  B  e.  A )  ->.  B  e.  A ).
23 tratrb 28335 . . . . 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 1152 . . . 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 28488 . . 3  |-  (. ( Ord  A  /\  B  e.  A )  ->.  Tr  B ).
26 trss 4275 . . . . 5  |-  ( Tr  A  ->  ( B  e.  A  ->  B  C_  A ) )
275, 22, 26e11 28502 . . . 4  |-  (. ( Ord  A  /\  B  e.  A )  ->.  B  C_  A ).
28 ssralv2 28330 . . . . 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 424 . . . 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 28488 . . 3  |-  (. ( Ord  A  /\  B  e.  A )  ->.  A. x  e.  B  A. y  e.  B  ( x  e.  y  \/  x  =  y  \/  y  e.  x ) ).
31 dford2 7535 . . . 4  |-  ( Ord 
B  <->  ( Tr  B  /\  A. x  e.  B  A. y  e.  B  ( x  e.  y  \/  x  =  y  \/  y  e.  x
) ) )
3231simplbi2 609 . . 3  |-  ( Tr  B  ->  ( A. x  e.  B  A. y  e.  B  (
x  e.  y  \/  x  =  y  \/  y  e.  x )  ->  Ord  B )
)
3325, 30, 32e11 28502 . 2  |-  (. ( Ord  A  /\  B  e.  A )  ->.  Ord  B ).
3433in1 28375 1  |-  ( ( Ord  A  /\  B  e.  A )  ->  Ord  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    \/ w3o 935   A.wal 1546    = wceq 1649    e. wcel 1721   A.wral 2670    C_ wss 3284   Tr wtr 4266   Ord word 4544
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-sep 4294  ax-nul 4302  ax-pr 4367  ax-un 4664  ax-reg 7520
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-ral 2675  df-rex 2676  df-rab 2679  df-v 2922  df-sbc 3126  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-nul 3593  df-if 3704  df-sn 3784  df-pr 3785  df-tp 3786  df-op 3787  df-uni 3980  df-br 4177  df-opab 4231  df-tr 4267  df-eprel 4458  df-po 4467  df-so 4468  df-fr 4505  df-we 4507  df-ord 4548  df-vd1 28374
  Copyright terms: Public domain W3C validator