Theorem ordelord 4762

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 2503	. . . . 5 |- ( x = B -> ( x e. A <-> B e. A ) )
2	1	anbi2d 703	. . . 4 |- ( x = B -> ( ( Ord A /\ x e. A ) <-> ( Ord A /\ B e. A ) ) )
3		ordeq 4747	. . . 4 |- ( x = B -> ( Ord x <-> Ord B ) )
4	2, 3	imbi12d 320	. . 3 |- ( x = B -> ( ( ( Ord A /\ x e. A ) -> Ord x ) <-> ( ( Ord A /\ B e. A ) -> Ord B ) ) )
5		simpll 753	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> Ord A )
6		3anrot 970	. . . . . . . . . . . 12 |- ( ( x e. A /\ z e. y /\ y e. x ) <-> ( z e. y /\ y e. x /\ x e. A ) )
7		3anass 969	. . . . . . . . . . . 12 |- ( ( x e. A /\ z e. y /\ y e. x ) <-> ( x e. A /\ ( z e. y /\ y e. x ) ) )
8	6, 7	bitr3i 251	. . . . . . . . . . 11 |- ( ( z e. y /\ y e. x /\ x e. A ) <-> ( x e. A /\ ( z e. y /\ y e. x ) ) )
9		ordtr 4754	. . . . . . . . . . . 12 |- ( Ord A -> Tr A )
10		trel3 4414	. . . . . . . . . . . 12 |- ( Tr A -> ( ( z e. y /\ y e. x /\ x e. A ) -> z e. A ) )
11	9, 10	syl 16	. . . . . . . . . . 11 |- ( Ord A -> ( ( z e. y /\ y e. x /\ x e. A ) -> z e. A ) )
12	8, 11	syl5bir 218	. . . . . . . . . 10 |- ( Ord A -> ( ( x e. A /\ ( z e. y /\ y e. x ) ) -> z e. A ) )
13	12	impl 620	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> z e. A )
14		trel 4413	. . . . . . . . . . . . 13 |- ( Tr A -> ( ( y e. x /\ x e. A ) -> y e. A ) )
15	9, 14	syl 16	. . . . . . . . . . . 12 |- ( Ord A -> ( ( y e. x /\ x e. A ) -> y e. A ) )
16	15	expcomd 438	. . . . . . . . . . 11 |- ( Ord A -> ( x e. A -> ( y e. x -> y e. A ) ) )
17	16	imp31 432	. . . . . . . . . 10 |- ( ( ( Ord A /\ x e. A ) /\ y e. x ) -> y e. A )
18	17	adantrl 715	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> y e. A )
19		simplr 754	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> x e. A )
20		ordwe 4753	. . . . . . . . . 10 |- ( Ord A -> _E We A )
21		wetrep 4734	. . . . . . . . . 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 471	. . . . . . . . 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 1220	. . . . . . . 8 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> ( ( z e. y /\ y e. x ) -> z e. x ) )
24	23	ex 434	. . . . . . 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 48	. . . . . 6 |- ( ( Ord A /\ x e. A ) -> ( ( z e. y /\ y e. x ) -> z e. x ) )
26	25	alrimivv 1686	. . . . 5 |- ( ( Ord A /\ x e. A ) -> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
27		dftr2 4408	. . . . 5 |- ( Tr x <-> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
28	26, 27	sylibr 212	. . . 4 |- ( ( Ord A /\ x e. A ) -> Tr x )
29		trss 4415	. . . . . . 7 |- ( Tr A -> ( x e. A -> x C_ A ) )
30	9, 29	syl 16	. . . . . 6 |- ( Ord A -> ( x e. A -> x C_ A ) )
31		wess 4728	. . . . . . 7 |- ( x C_ A -> ( _E We A -> _E We x ) )
32	20, 31	syl5com 30	. . . . . 6 |- ( Ord A -> ( x C_ A -> _E We x ) )
33	30, 32	syld 44	. . . . 5 |- ( Ord A -> ( x e. A -> _E We x ) )
34	33	imp 429	. . . 4 |- ( ( Ord A /\ x e. A ) -> _E We x )
35		df-ord 4743	. . . 4 |- ( Ord x <-> ( Tr x /\ _E We x ) )
36	28, 34, 35	sylanbrc 664	. . 3 |- ( ( Ord A /\ x e. A ) -> Ord x )
37	4, 36	vtoclg 3051	. 2 |- ( B e. A -> ( ( Ord A /\ B e. A ) -> Ord B ) )
38	37	anabsi7 815	1 |- ( ( Ord A /\ B e. A ) -> Ord B )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 965   A.wal 1367   = wceq 1369   e. wcel 1756   C_ wss 3349   Tr wtr 4406   _E cep 4651   We wwe 4699   Ord word 4739

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pr 4552

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-tr 4407  df-eprel 4653  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743

This theorem is referenced by:  tron  4763  ordelon  4764  ordtr2  4784  ordtr3  4785  ordintdif  4789  ordsuc  6446  ordsucss  6450  ordsucelsuc  6454  ordsucuniel  6456  limsssuc  6482  smores  6834  smo11  6846  smoord  6847  smoword  6848  smogt  6849  smorndom  6850  rdglim2  6909  oesuclem  6986  ordtypelem3  7755  r1val1  8014  rankr1ag  8030  fin23lem24  8512  onsuct0  28309  dford3  29403  ordpss  29733