Theorem ordelordALTVD 44367

Description: An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 6387 using the Axiom of Regularity indirectly through dford2 9638. 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 44037 is ordelordALTVD 44367 without virtual deductions and was automatically derived from ordelordALTVD 44367 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 44074	. . . . . 6 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   )
2		simpl 481	. . . . . 6 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐴)
3	1, 2	e1a 44127	. . . . 5 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   Ord 𝐴   )
4		ordtr 6379	. . . . 5 ⊢ (Ord 𝐴 → Tr 𝐴)
5	3, 4	e1a 44127	. . . 4 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   Tr 𝐴   )
6		dford2 9638	. . . . . . 7 ⊢ (Ord 𝐴 ↔ (Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)))
7	6	simprbi 495	. . . . . 6 ⊢ (Ord 𝐴 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))
8	3, 7	e1a 44127	. . . . 5 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)   )
9		3orcomb 1091	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
10	9	ax-gen 1789	. . . . . . . . . 10 ⊢ ∀𝑦((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
11		alral 3065	. . . . . . . . . 10 ⊢ (∀𝑦((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)))
12	10, 11	e0a 44272	. . . . . . . . 9 ⊢ ∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
13		ralbi 3093	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐴 ((𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)))
14	12, 13	e0a 44272	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
15	14	ax-gen 1789	. . . . . . 7 ⊢ ∀𝑥(∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
16		alral 3065	. . . . . . 7 ⊢ (∀𝑥(∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)))
17	15, 16	e0a 44272	. . . . . 6 ⊢ ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
18		ralbi 3093	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)))
19	17, 18	e0a 44272	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦))
20	8, 19	e1bi 44129	. . . 4 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦)   )
21		simpr 483	. . . . 5 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → 𝐵 ∈ 𝐴)
22	1, 21	e1a 44127	. . . 4 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   𝐵 ∈ 𝐴   )
23		tratrb 44036	. . . . 5 ⊢ ((Tr 𝐴 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) ∧ 𝐵 ∈ 𝐴) → Tr 𝐵)
24	23	3exp 1116	. . . 4 ⊢ (Tr 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦) → (𝐵 ∈ 𝐴 → Tr 𝐵)))
25	5, 20, 22, 24	e111 44174	. . 3 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   Tr 𝐵   )
26		trss 5272	. . . . 5 ⊢ (Tr 𝐴 → (𝐵 ∈ 𝐴 → 𝐵 ⊆ 𝐴))
27	5, 22, 26	e11 44188	. . . 4 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   𝐵 ⊆ 𝐴   )
28		ssralv2 44031	. . . . 5 ⊢ ((𝐵 ⊆ 𝐴 ∧ 𝐵 ⊆ 𝐴) → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)))
29	28	ex 411	. . . 4 ⊢ (𝐵 ⊆ 𝐴 → (𝐵 ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥))))
30	27, 27, 8, 29	e111 44174	. . 3 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)   )
31		dford2 9638	. . . 4 ⊢ (Ord 𝐵 ↔ (Tr 𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥)))
32	31	simplbi2 499	. . 3 ⊢ (Tr 𝐵 → (∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∨ 𝑥 = 𝑦 ∨ 𝑦 ∈ 𝑥) → Ord 𝐵))
33	25, 30, 32	e11 44188	. 2 ⊢ (   (Ord 𝐴 ∧ 𝐵 ∈ 𝐴)   ▶   Ord 𝐵   )
34	33	in1 44071	1 ⊢ ((Ord 𝐴 ∧ 𝐵 ∈ 𝐴) → Ord 𝐵)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∨ w3o 1083  ∀wal 1531   = wceq 1533   ∈ wcel 2098  ∀wral 3051   ⊆ wss 3941  Tr wtr 5261  Ord word 6364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-sep 5295  ax-nul 5302  ax-pr 5424  ax-un 7735  ax-reg 9610

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-ral 3052  df-rex 3061  df-rab 3420  df-v 3465  df-sbc 3771  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4905  df-br 5145  df-opab 5207  df-tr 5262  df-eprel 5577  df-po 5585  df-so 5586  df-fr 5628  df-we 5630  df-ord 6368  df-vd1 44070

This theorem is referenced by: (None)