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

Theorem ordelordALT 40869
 Description: An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 6212 using the Axiom of Regularity indirectly through dford2 9082. 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 40869 is ordelordALTVD 41199 without virtual deductions and was automatically derived from ordelordALTVD 41199 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 6204 . . . 4 (Ord 𝐴 → Tr 𝐴)
21adantr 483 . . 3 ((Ord 𝐴𝐵𝐴) → Tr 𝐴)
3 dford2 9082 . . . . . 6 (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥)))
43simprbi 499 . . . . 5 (Ord 𝐴 → ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
54adantr 483 . . . 4 ((Ord 𝐴𝐵𝐴) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
6 3orcomb 1090 . . . . 5 ((𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ (𝑥𝑦𝑦𝑥𝑥 = 𝑦))
762ralbii 3166 . . . 4 (∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦))
85, 7sylib 220 . . 3 ((Ord 𝐴𝐵𝐴) → ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦))
9 simpr 487 . . 3 ((Ord 𝐴𝐵𝐴) → 𝐵𝐴)
10 tratrb 40868 . . 3 ((Tr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴) → Tr 𝐵)
112, 8, 9, 10syl3anc 1367 . 2 ((Ord 𝐴𝐵𝐴) → Tr 𝐵)
12 trss 5180 . . . 4 (Tr 𝐴 → (𝐵𝐴𝐵𝐴))
132, 9, 12sylc 65 . . 3 ((Ord 𝐴𝐵𝐴) → 𝐵𝐴)
14 ssralv2 40863 . . . 4 ((𝐵𝐴𝐵𝐴) → (∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) → ∀𝑥𝐵𝑦𝐵 (𝑥𝑦𝑥 = 𝑦𝑦𝑥)))
1514ex 415 . . 3 (𝐵𝐴 → (𝐵𝐴 → (∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) → ∀𝑥𝐵𝑦𝐵 (𝑥𝑦𝑥 = 𝑦𝑦𝑥))))
1613, 13, 5, 15syl3c 66 . 2 ((Ord 𝐴𝐵𝐴) → ∀𝑥𝐵𝑦𝐵 (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
17 dford2 9082 . 2 (Ord 𝐵 ↔ (Tr 𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝑦𝑥 = 𝑦𝑦𝑥)))
1811, 16, 17sylanbrc 585 1 ((Ord 𝐴𝐵𝐴) → Ord 𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 398   ∨ w3o 1082   ∈ wcel 2110  ∀wral 3138   ⊆ wss 3935  Tr wtr 5171  Ord word 6189 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329  ax-un 7460  ax-reg 9055 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-tp 4571  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-tr 5172  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-we 5515  df-ord 6193 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator