Theorem ordelordALTVD 37258

Description: An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. This is an alternate proof of ordelord 5444 using the Axiom of Regularity indirectly through dford2 8122. 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 36892 is ordelordALTVD 37258 without virtual deductions and was automatically derived from ordelordALTVD 37258 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 36938	. . . . . 6 |- (. ( Ord A /\ B e. A ) ->. ( Ord A /\ B e. A ) ).
2		simpl 459	. . . . . 6 |- ( ( Ord A /\ B e. A ) -> Ord A )
3	1, 2	e1a 37000	. . . . 5 |- (. ( Ord A /\ B e. A ) ->. Ord A ).
4		ordtr 5436	. . . . 5 |- ( Ord A -> Tr A )
5	3, 4	e1a 37000	. . . 4 |- (. ( Ord A /\ B e. A ) ->. Tr A ).
6		dford2 8122	. . . . . . 7 |- ( Ord A <-> ( Tr A /\ A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ) )
7	6	simprbi 466	. . . . . 6 |- ( Ord A -> A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) )
8	3, 7	e1a 37000	. . . . 5 |- (. ( Ord A /\ B e. A ) ->. A. x e. A A. y e. A ( x e. y \/ x = y \/ y e. x ) ).
9		3orcomb 994	. . . . . . . . . . 11 |- ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) )
10	9	ax-gen 1668	. . . . . . . . . 10 |- A. y ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) )
11		alral 2752	. . . . . . . . . 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 37153	. . . . . . . . 9 |- A. y e. A ( ( x e. y \/ x = y \/ y e. x ) <-> ( x e. y \/ y e. x \/ x = y ) )
13		ralbi 2920	. . . . . . . . 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 37153	. . . . . . . 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 1668	. . . . . . 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 2752	. . . . . . 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 37153	. . . . . 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 2920	. . . . . 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 37153	. . . . 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 37002	. . . 4 |- (. ( Ord A /\ B e. A ) ->. A. x e. A A. y e. A ( x e. y \/ y e. x \/ x = y ) ).
21		simpr 463	. . . . 5 |- ( ( Ord A /\ B e. A ) -> B e. A )
22	1, 21	e1a 37000	. . . 4 |- (. ( Ord A /\ B e. A ) ->. B e. A ).
23		tratrb 36891	. . . . 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 1206	. . . 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 37047	. . 3 |- (. ( Ord A /\ B e. A ) ->. Tr B ).
26		trss 4505	. . . . 5 |- ( Tr A -> ( B e. A -> B C_ A ) )
27	5, 22, 26	e11 37061	. . . 4 |- (. ( Ord A /\ B e. A ) ->. B C_ A ).
28		ssralv2 36882	. . . . 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 436	. . . 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 37047	. . 3 |- (. ( Ord A /\ B e. A ) ->. A. x e. B A. y e. B ( x e. y \/ x = y \/ y e. x ) ).
31		dford2 8122	. . . 4 |- ( Ord B <-> ( Tr B /\ A. x e. B A. y e. B ( x e. y \/ x = y \/ y e. x ) ) )
32	31	simplbi2 630	. . 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 37061	. 2 |- (. ( Ord A /\ B e. A ) ->. Ord B ).
34	33	in1 36935	1 |- ( ( Ord A /\ B e. A ) -> Ord B )

Syntax hints:   -> wi 4   <-> wb 188   /\ wa 371   \/ w3o 983   A.wal 1441   = wceq 1443   e. wcel 1886   A.wral 2736   C_ wss 3403   Tr wtr 4496   Ord word 5421

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638  ax-un 6580  ax-reg 8104

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-ral 2741  df-rex 2742  df-rab 2745  df-v 3046  df-sbc 3267  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-br 4402  df-opab 4461  df-tr 4497  df-eprel 4744  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-ord 5425  df-vd1 36934

This theorem is referenced by: (None)