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

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

Proof of Theorem ordelordALTVD
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 idn1 37811 . . . . . 6 (   (Ord 𝐴𝐵𝐴)   ▶   (Ord 𝐴𝐵𝐴)   )
2 simpl 472 . . . . . 6 ((Ord 𝐴𝐵𝐴) → Ord 𝐴)
31, 2e1a 37873 . . . . 5 (   (Ord 𝐴𝐵𝐴)   ▶   Ord 𝐴   )
4 ordtr 5654 . . . . 5 (Ord 𝐴 → Tr 𝐴)
53, 4e1a 37873 . . . 4 (   (Ord 𝐴𝐵𝐴)   ▶   Tr 𝐴   )
6 dford2 8400 . . . . . . 7 (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥)))
76simprbi 479 . . . . . 6 (Ord 𝐴 → ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥))
83, 7e1a 37873 . . . . 5 (   (Ord 𝐴𝐵𝐴)   ▶   𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥)   )
9 3orcomb 1041 . . . . . . . . . . 11 ((𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ (𝑥𝑦𝑦𝑥𝑥 = 𝑦))
109ax-gen 1713 . . . . . . . . . 10 𝑦((𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ (𝑥𝑦𝑦𝑥𝑥 = 𝑦))
11 alral 2912 . . . . . . . . . 10 (∀𝑦((𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ (𝑥𝑦𝑦𝑥𝑥 = 𝑦)) → ∀𝑦𝐴 ((𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ (𝑥𝑦𝑦𝑥𝑥 = 𝑦)))
1210, 11e0a 38020 . . . . . . . . 9 𝑦𝐴 ((𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ (𝑥𝑦𝑦𝑥𝑥 = 𝑦))
13 ralbi 3050 . . . . . . . . 9 (∀𝑦𝐴 ((𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ (𝑥𝑦𝑦𝑥𝑥 = 𝑦)) → (∀𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ ∀𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦)))
1412, 13e0a 38020 . . . . . . . 8 (∀𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ ∀𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦))
1514ax-gen 1713 . . . . . . 7 𝑥(∀𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ ∀𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦))
16 alral 2912 . . . . . . 7 (∀𝑥(∀𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ ∀𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦)) → ∀𝑥𝐴 (∀𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ ∀𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦)))
1715, 16e0a 38020 . . . . . 6 𝑥𝐴 (∀𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ ∀𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦))
18 ralbi 3050 . . . . . 6 (∀𝑥𝐴 (∀𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ ∀𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦)) → (∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦)))
1917, 18e0a 38020 . . . . 5 (∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) ↔ ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦))
208, 19e1bi 37875 . . . 4 (   (Ord 𝐴𝐵𝐴)   ▶   𝑥𝐴𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦)   )
21 simpr 476 . . . . 5 ((Ord 𝐴𝐵𝐴) → 𝐵𝐴)
221, 21e1a 37873 . . . 4 (   (Ord 𝐴𝐵𝐴)   ▶   𝐵𝐴   )
23 tratrb 37767 . . . . 5 ((Tr 𝐴 ∧ ∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦) ∧ 𝐵𝐴) → Tr 𝐵)
24233exp 1256 . . . 4 (Tr 𝐴 → (∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑦𝑥𝑥 = 𝑦) → (𝐵𝐴 → Tr 𝐵)))
255, 20, 22, 24e111 37920 . . 3 (   (Ord 𝐴𝐵𝐴)   ▶   Tr 𝐵   )
26 trss 4689 . . . . 5 (Tr 𝐴 → (𝐵𝐴𝐵𝐴))
275, 22, 26e11 37934 . . . 4 (   (Ord 𝐴𝐵𝐴)   ▶   𝐵𝐴   )
28 ssralv2 37758 . . . . 5 ((𝐵𝐴𝐵𝐴) → (∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) → ∀𝑥𝐵𝑦𝐵 (𝑥𝑦𝑥 = 𝑦𝑦𝑥)))
2928ex 449 . . . 4 (𝐵𝐴 → (𝐵𝐴 → (∀𝑥𝐴𝑦𝐴 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) → ∀𝑥𝐵𝑦𝐵 (𝑥𝑦𝑥 = 𝑦𝑦𝑥))))
3027, 27, 8, 29e111 37920 . . 3 (   (Ord 𝐴𝐵𝐴)   ▶   𝑥𝐵𝑦𝐵 (𝑥𝑦𝑥 = 𝑦𝑦𝑥)   )
31 dford2 8400 . . . 4 (Ord 𝐵 ↔ (Tr 𝐵 ∧ ∀𝑥𝐵𝑦𝐵 (𝑥𝑦𝑥 = 𝑦𝑦𝑥)))
3231simplbi2 653 . . 3 (Tr 𝐵 → (∀𝑥𝐵𝑦𝐵 (𝑥𝑦𝑥 = 𝑦𝑦𝑥) → Ord 𝐵))
3325, 30, 32e11 37934 . 2 (   (Ord 𝐴𝐵𝐴)   ▶   Ord 𝐵   )
3433in1 37808 1 ((Ord 𝐴𝐵𝐴) → Ord 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195  wa 383  w3o 1030  wal 1473   = wceq 1475  wcel 1977  wral 2896  wss 3540  Tr wtr 4680  Ord word 5639
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847  ax-reg 8380
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-tr 4681  df-eprel 4949  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-ord 5643  df-vd1 37807
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator