Theorem ordelordALTVD 42487

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. 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 42157 is ordelordALTVD 42487 without virtual deductions and was automatically derived from ordelordALTVD 42487 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 42194	. . . . . 6 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   )
2		simpl 483	. . . . . 6 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐴)
3	1, 2	e1a 42247	. . . . 5 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   Ord 𝐴   )
4		ordtr 6280	. . . . 5 ⊢ (Ord 𝐴 → Tr 𝐴)
5	3, 4	e1a 42247	. . . 4 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   Tr 𝐴   )
6		dford2 9378	. . . . . . 7 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)))
7	6	simprbi 497	. . . . . 6 ⊢ (Ord 𝐴 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
8	3, 7	e1a 42247	. . . . 5 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)   )
9		3orcomb 1093	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
10	9	ax-gen 1798	. . . . . . . . . 10 ⊢ ∀𝑦((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
11		alral 3080	. . . . . . . . . 10 ⊢ (∀𝑦((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)))
12	10, 11	e0a 42392	. . . . . . . . 9 ⊢ ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
13		ralbi 3089	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)))
14	12, 13	e0a 42392	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
15	14	ax-gen 1798	. . . . . . 7 ⊢ ∀𝑥(∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
16		alral 3080	. . . . . . 7 ⊢ (∀𝑥(∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)))
17	15, 16	e0a 42392	. . . . . 6 ⊢ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
18		ralbi 3089	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)))
19	17, 18	e0a 42392	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
20	8, 19	e1bi 42249	. . . 4 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
21		simpr 485	. . . . 5 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐴)
22	1, 21	e1a 42247	. . . 4 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   𝐵 ∈ 𝐴   )
23		tratrb 42156	. . . . 5 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → Tr 𝐵)
24	23	3exp 1118	. . . 4 ⊢ (Tr 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → (𝐵 ∈ 𝐴 → Tr 𝐵)))
25	5, 20, 22, 24	e111 42294	. . 3 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   Tr 𝐵   )
26		trss 5200	. . . . 5 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
27	5, 22, 26	e11 42308	. . . 4 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   𝐵 ⊆ 𝐴   )
28		ssralv2 42151	. . . . 5 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)))
29	28	ex 413	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))))
30	27, 27, 8, 29	e111 42294	. . 3 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)   )
31		dford2 9378	. . . 4 ⊢ (Ord 𝐵 ↔ (Tr 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)))
32	31	simplbi2 501	. . 3 ⊢ (Tr 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → Ord 𝐵))
33	25, 30, 32	e11 42308	. 2 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   Ord 𝐵   )
34	33	in1 42191	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∨ w3o 1085  ∀wal 1537   = wceq 1539   ∈ 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  df-vd1 42190

This theorem is referenced by: (None)