Theorem ordelordALTVD 45319

Description: An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 6333 using the Axiom of Regularity indirectly through dford2 9533. 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 44990 is ordelordALTVD 45319 without virtual deductions and was automatically derived from ordelordALTVD 45319 using the tools program translate..without..overwriting.cmd and the Metamath program "MM-PA> MINIMIZE_WITH *" 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.

Step	Hyp	Ref	Expression
1		idn1 45027	. . . . . 6 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   )
2		simpl 483	. . . . . 6 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐴)
3	1, 2	e1a 45080	. . . . 5 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   Ord 𝐴   )
4		ordtr 6325	. . . . 5 ⊢ (Ord 𝐴 → Tr 𝐴)
5	3, 4	e1a 45080	. . . 4 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   Tr 𝐴   )
6		dford2 9533	. . . . . . 7 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)))
7	6	simprbi 498	. . . . . 6 ⊢ (Ord 𝐴 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
8	3, 7	e1a 45080	. . . . 5 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)   )
9		3orcomb 1099	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
10	9	ax-gen 1802	. . . . . . . . . 10 ⊢ ∀𝑦((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
11		alral 3068	. . . . . . . . . 10 ⊢ (∀𝑦((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)))
12	10, 11	e0a 45224	. . . . . . . . 9 ⊢ ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
13		ralbi 3094	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)))
14	12, 13	e0a 45224	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
15	14	ax-gen 1802	. . . . . . 7 ⊢ ∀𝑥(∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
16		alral 3068	. . . . . . 7 ⊢ (∀𝑥(∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)))
17	15, 16	e0a 45224	. . . . . 6 ⊢ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
18		ralbi 3094	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)))
19	17, 18	e0a 45224	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
20	8, 19	e1bi 45082	. . . 4 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
21		simpr 485	. . . . 5 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐴)
22	1, 21	e1a 45080	. . . 4 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   𝐵 ∈ 𝐴   )
23		tratrb 44989	. . . . 5 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → Tr 𝐵)
24	23	3exp 1125	. . . 4 ⊢ (Tr 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → (𝐵 ∈ 𝐴 → Tr 𝐵)))
25	5, 20, 22, 24	e111 45127	. . 3 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   Tr 𝐵   )
26		trss 5190	. . . . 5 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
27	5, 22, 26	e11 45141	. . . 4 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   𝐵 ⊆ 𝐴   )
28		ssralv2 44984	. . . . 5 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)))
29	28	ex 413	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))))
30	27, 27, 8, 29	e111 45127	. . 3 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)   )
31		dford2 9533	. . . 4 ⊢ (Ord 𝐵 ↔ (Tr 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)))
32	31	simplbi2 501	. . 3 ⊢ (Tr 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → Ord 𝐵))
33	25, 30, 32	e11 45141	. 2 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   Ord 𝐵   )
34	33	in1 45024	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∨ w3o 1091  ∀wal 1545   = wceq 1547   ∈ wcel 2119  ∀wral 3053   ⊆ wss 3883  Tr wtr 5180  Ord word 6310

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5219  ax-pr 5363  ax-un 7679  ax-reg 9498

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4263  df-if 4456  df-pw 4532  df-sn 4557  df-pr 4559  df-tp 4561  df-op 4563  df-uni 4840  df-br 5074  df-opab 5136  df-tr 5181  df-eprel 5519  df-po 5527  df-so 5528  df-fr 5572  df-we 5574  df-ord 6314  df-vd1 45023

This theorem is referenced by: (None)