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

Theorem ordelordALT 42157
Description: An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 6288 using the Axiom of Regularity indirectly through dford2 9378. dford2 is a weaker definition of ordinal number. Given the Axiom of Regularity, it need not be assumed that E Fr 𝐴 because this is inferred by the Axiom of Regularity. ordelordALT 42157 is ordelordALTVD 42487 without virtual deductions and was automatically derived from ordelordALTVD 42487 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 𝐴𝐵𝐴) → Ord 𝐵)

Proof of Theorem ordelordALT
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ordtr 6280 . . . 4 (Ord 𝐴 → Tr 𝐴)
21adantr 481 . . 3 ((Ord 𝐴𝐵𝐴) → Tr 𝐴)
3 dford2 9378 . . . . . 6 (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥)))
43simprbi 497 . . . . 5 (Ord 𝐴 → ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
54adantr 481 . . . 4 ((Ord 𝐴𝐵𝐴) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
6 3orcomb 1093 . . . . 5 ((𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ (𝑥𝑦𝑦𝑥𝑥 = 𝑦))
762ralbii 3093 . . . 4 (∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦))
85, 7sylib 217 . . 3 ((Ord 𝐴𝐵𝐴) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦))
9 simpr 485 . . 3 ((Ord 𝐴𝐵𝐴) → 𝐵𝐴)
10 tratrb 42156 . . 3 ((Tr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴) → Tr 𝐵)
112, 8, 9, 10syl3anc 1370 . 2 ((Ord 𝐴𝐵𝐴) → Tr 𝐵)
12 trss 5200 . . . 4 (Tr 𝐴 → (𝐵𝐴𝐵𝐴))
132, 9, 12sylc 65 . . 3 ((Ord 𝐴𝐵𝐴) → 𝐵𝐴)
14 ssralv2 42151 . . . 4 ((𝐵𝐴𝐵𝐴) → (∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) → ∀𝑥𝐵𝑦𝐵 (𝑥𝑦𝑥 = 𝑦𝑦𝑥)))
1514ex 413 . . 3 (𝐵𝐴 → (𝐵𝐴 → (∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) → ∀𝑥𝐵𝑦𝐵 (𝑥𝑦𝑥 = 𝑦𝑦𝑥))))
1613, 13, 5, 15syl3c 66 . 2 ((Ord 𝐴𝐵𝐴) → ∀𝑥𝐵𝑦𝐵 (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
17 dford2 9378 . 2 (Ord 𝐵 ↔ (Tr 𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝑦𝑥 = 𝑦𝑦𝑥)))
1811, 16, 17sylanbrc 583 1 ((Ord 𝐴𝐵𝐴) → Ord 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3o 1085  wcel 2106  wral 3064  wss 3887  Tr wtr 5191  Ord word 6265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588  ax-reg 9351
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-tr 5192  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-ord 6269
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator