Theorem ordelord 5452

Description: An element of an ordinal class is ordinal. Proposition 7.6 of [TakeutiZaring] p. 36. (Contributed by NM, 23-Apr-1994.)

Assertion

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

Proof of Theorem ordelord

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

Step	Hyp	Ref	Expression
1		eleq1 2537	. . . . 5 |- ( x = B -> ( x e. A <-> B e. A ) )
2	1	anbi2d 718	. . . 4 |- ( x = B -> ( ( Ord A /\ x e. A ) <-> ( Ord A /\ B e. A ) ) )
3		ordeq 5437	. . . 4 |- ( x = B -> ( Ord x <-> Ord B ) )
4	2, 3	imbi12d 327	. . 3 |- ( x = B -> ( ( ( Ord A /\ x e. A ) -> Ord x ) <-> ( ( Ord A /\ B e. A ) -> Ord B ) ) )
5		simpll 768	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> Ord A )
6		3anrot 1012	. . . . . . . . . . . 12 |- ( ( x e. A /\ z e. y /\ y e. x ) <-> ( z e. y /\ y e. x /\ x e. A ) )
7		3anass 1011	. . . . . . . . . . . 12 |- ( ( x e. A /\ z e. y /\ y e. x ) <-> ( x e. A /\ ( z e. y /\ y e. x ) ) )
8	6, 7	bitr3i 259	. . . . . . . . . . 11 |- ( ( z e. y /\ y e. x /\ x e. A ) <-> ( x e. A /\ ( z e. y /\ y e. x ) ) )
9		ordtr 5444	. . . . . . . . . . . 12 |- ( Ord A -> Tr A )
10		trel3 4498	. . . . . . . . . . . 12 |- ( Tr A -> ( ( z e. y /\ y e. x /\ x e. A ) -> z e. A ) )
11	9, 10	syl 17	. . . . . . . . . . 11 |- ( Ord A -> ( ( z e. y /\ y e. x /\ x e. A ) -> z e. A ) )
12	8, 11	syl5bir 226	. . . . . . . . . 10 |- ( Ord A -> ( ( x e. A /\ ( z e. y /\ y e. x ) ) -> z e. A ) )
13	12	impl 632	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> z e. A )
14		trel 4497	. . . . . . . . . . . . 13 |- ( Tr A -> ( ( y e. x /\ x e. A ) -> y e. A ) )
15	9, 14	syl 17	. . . . . . . . . . . 12 |- ( Ord A -> ( ( y e. x /\ x e. A ) -> y e. A ) )
16	15	expcomd 445	. . . . . . . . . . 11 |- ( Ord A -> ( x e. A -> ( y e. x -> y e. A ) ) )
17	16	imp31 439	. . . . . . . . . 10 |- ( ( ( Ord A /\ x e. A ) /\ y e. x ) -> y e. A )
18	17	adantrl 730	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> y e. A )
19		simplr 770	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> x e. A )
20		ordwe 5443	. . . . . . . . . 10 |- ( Ord A -> _E We A )
21		wetrep 4832	. . . . . . . . . 10 |- ( ( _E We A /\ ( z e. A /\ y e. A /\ x e. A ) ) -> ( ( z e. y /\ y e. x ) -> z e. x ) )
22	20, 21	sylan 479	. . . . . . . . 9 |- ( ( Ord A /\ ( z e. A /\ y e. A /\ x e. A ) ) -> ( ( z e. y /\ y e. x ) -> z e. x ) )
23	5, 13, 18, 19, 22	syl13anc 1294	. . . . . . . 8 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> ( ( z e. y /\ y e. x ) -> z e. x ) )
24	23	ex 441	. . . . . . 7 |- ( ( Ord A /\ x e. A ) -> ( ( z e. y /\ y e. x ) -> ( ( z e. y /\ y e. x ) -> z e. x ) ) )
25	24	pm2.43d 49	. . . . . 6 |- ( ( Ord A /\ x e. A ) -> ( ( z e. y /\ y e. x ) -> z e. x ) )
26	25	alrimivv 1782	. . . . 5 |- ( ( Ord A /\ x e. A ) -> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
27		dftr2 4492	. . . . 5 |- ( Tr x <-> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
28	26, 27	sylibr 217	. . . 4 |- ( ( Ord A /\ x e. A ) -> Tr x )
29		trss 4499	. . . . . . 7 |- ( Tr A -> ( x e. A -> x C_ A ) )
30	9, 29	syl 17	. . . . . 6 |- ( Ord A -> ( x e. A -> x C_ A ) )
31		wess 4826	. . . . . 6 |- ( x C_ A -> ( _E We A -> _E We x ) )
32	30, 20, 31	syl6ci 66	. . . . 5 |- ( Ord A -> ( x e. A -> _E We x ) )
33	32	imp 436	. . . 4 |- ( ( Ord A /\ x e. A ) -> _E We x )
34		df-ord 5433	. . . 4 |- ( Ord x <-> ( Tr x /\ _E We x ) )
35	28, 33, 34	sylanbrc 677	. . 3 |- ( ( Ord A /\ x e. A ) -> Ord x )
36	4, 35	vtoclg 3093	. 2 |- ( B e. A -> ( ( Ord A /\ B e. A ) -> Ord B ) )
37	36	anabsi7 835	1 |- ( ( Ord A /\ B e. A ) -> Ord B )

Syntax hints:   -> wi 4   /\ wa 376   /\ w3a 1007   A.wal 1450   = wceq 1452   e. wcel 1904   C_ wss 3390   Tr wtr 4490   _E cep 4748   We wwe 4797   Ord word 5429

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-tr 4491  df-eprel 4750  df-po 4760  df-so 4761  df-fr 4798  df-we 4800  df-ord 5433

This theorem is referenced by:  tron  5453  ordelon  5454  ordtr2  5474  ordtr3  5475  ordintdif  5479  ordsuc  6660  ordsucss  6664  ordsucelsuc  6668  ordsucuniel  6670  limsssuc  6696  smores  7089  smo11  7101  smoord  7102  smoword  7103  smogt  7104  smorndom  7105  rdglim2  7168  oesuclem  7245  ordtypelem3  8053  r1val1  8275  rankr1ag  8291  fin23lem24  8770  onsuct0  31172  dford3  35954  ordpss  36874