Theorem ordelordALTVD 33400

Description: An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 4890 using the Axiom of Regularity indirectly through dford2 8040. dford2 is a weaker definition of ordinal number. Given the Axiom of Regularity, it need not be assumed that _E Fr A 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 33041 is ordelordALTVD 33400 without virtual deductions and was automatically derived from ordelordALTVD 33400 using the tools program translate..without..overwriting.cmd and Metamath's minimize command.

1::	|- (. ( Ord A /\ B e. A ) ->. ( Ord A /\ B e. A ) ).
2:1:	|- (. ( Ord A /\ B e. A ) ->. Ord A ).
3:1:	|- (. ( Ord A /\ B e. A ) ->. B e. A ).
4:2:	|- (. ( Ord A /\ B e. A ) ->. Tr A ).
5:2:	|- (. ( Ord A /\ B e. A ) ->. A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ).
6:4,3:	|- (. ( Ord A /\ B e. A ) ->. B C_ A ).
7:6,6,5:	|- (. ( Ord A /\ B e. A ) ->. A. x e. B A. y e. B ( x e. y \/ x = y \/ y e. x ) ).
8::	|- ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) )
9:8:	|- A. y ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) )
10:9:	|- A. y e. A ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) )
11:10:	|- ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) )
12:11:	|- A. x ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) )
13:12:	|- A. x e. A ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) )
14:13:	|- ( A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) )
15:14,5:	|- (. ( Ord A /\ B e. A ) ->. A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) ).
16:4,15,3:	|- (. ( Ord A /\ B e. A ) ->. Tr B ).
17:16,7:	|- (. ( Ord A /\ B e. A ) ->. Ord B ).
qed:17:	|- ( ( Ord A /\ B e. A ) -> Ord B )

(Contributed by Alan Sare, 12-Feb-2012.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
ordelordALTVD	|- ( ( Ord A /\ B e. A ) -> Ord B )

Proof of Theorem ordelordALTVD

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		idn1 33084	. . . . . 6 |- (. ( Ord A /\ B e. A ) ->. ( Ord A /\ B e. A ) ).
2		simpl 457	. . . . . 6 |- ( ( Ord A /\ B e. A ) -> Ord A )
3	1, 2	e1a 33146	. . . . 5 |- (. ( Ord A /\ B e. A ) ->. Ord A ).
4		ordtr 4882	. . . . 5 |- ( Ord A -> Tr A )
5	3, 4	e1a 33146	. . . 4 |- (. ( Ord A /\ B e. A ) ->. Tr A ).
6		dford2 8040	. . . . . . 7 |- ( Ord A <-> ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ) )
7	6	simprbi 464	. . . . . 6 |- ( Ord A -> A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) )
8	3, 7	e1a 33146	. . . . 5 |- (. ( Ord A /\ B e. A ) ->. A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ).
9		3orcomb 984	. . . . . . . . . . 11 |- ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) )
10	9	ax-gen 1605	. . . . . . . . . 10 |- A. y ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) )
11		alral 2808	. . . . . . . . . 10 |- ( A. y ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) ) -> A. y e. A ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) ) )
12	10, 11	e0a 33302	. . . . . . . . 9 |- A. y e. A ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) )
13		ralbi 2974	. . . . . . . . 9 |- ( A. y e. A ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) ) -> ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) ) )
14	12, 13	e0a 33302	. . . . . . . 8 |- ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) )
15	14	ax-gen 1605	. . . . . . 7 |- A. x ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) )
16		alral 2808	. . . . . . 7 |- ( A. x ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) ) -> A. x e. A ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) ) )
17	15, 16	e0a 33302	. . . . . 6 |- A. x e. A ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) )
18		ralbi 2974	. . . . . 6 |- ( A. x e. A ( A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. y e. A ( x e. y \/ y e. x \/ x = y ) ) -> ( A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) ) )
19	17, 18	e0a 33302	. . . . 5 |- ( A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) <-> A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) )
20	8, 19	e1bi 33148	. . . 4 |- (. ( Ord A /\ B e. A ) ->. A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) ).
21		simpr 461	. . . . 5 |- ( ( Ord A /\ B e. A ) -> B e. A )
22	1, 21	e1a 33146	. . . 4 |- (. ( Ord A /\ B e. A ) ->. B e. A ).
23		tratrb 33040	. . . . 5 |- ( ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) /\ B e. A ) -> Tr B )
24	23	3exp 1196	. . . 4 |- ( Tr A -> ( A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) -> ( B e. A -> Tr B ) ) )
25	5, 20, 22, 24	e111 33193	. . 3 |- (. ( Ord A /\ B e. A ) ->. Tr B ).
26		trss 4539	. . . . 5 |- ( Tr A -> ( B e. A -> B C_ A ) )
27	5, 22, 26	e11 33207	. . . 4 |- (. ( Ord A /\ B e. A ) ->. B C_ A ).
28		ssralv2 33034	. . . . 5 |- ( ( B C_ A /\ B C_ A ) -> ( A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) -> A. x e. B A. y e. B ( x e. y \/ x = y \/ y e. x ) ) )
29	28	ex 434	. . . 4 |- ( B C_ A -> ( B C_ A -> ( A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) -> A. x e. B A. y e. B ( x e. y \/ x = y \/ y e. x ) ) ) )
30	27, 27, 8, 29	e111 33193	. . 3 |- (. ( Ord A /\ B e. A ) ->. A. x e. B A. y e. B ( x e. y \/ x = y \/ y e. x ) ).
31		dford2 8040	. . . 4 |- ( Ord B <-> ( Tr B /\ A. x e. B A. y e. B ( x e. y \/ x = y \/ y e. x ) ) )
32	31	simplbi2 625	. . 3 |- ( Tr B -> ( A. x e. B A. y e. B ( x e. y \/ x = y \/ y e. x ) -> Ord B ) )
33	25, 30, 32	e11 33207	. 2 |- (. ( Ord A /\ B e. A ) ->. Ord B ).
34	33	in1 33081	1 |- ( ( Ord A /\ B e. A ) -> Ord B )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   \/ w3o 973   A.wal 1381   = wceq 1383   e. wcel 1804   A.wral 2793   C_ wss 3461   Tr wtr 4530   Ord word 4867

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676  ax-un 6577  ax-reg 8021

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-tr 4531  df-eprel 4781  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-vd1 33080

This theorem is referenced by: (None)