Theorem ordelord 5745

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 2689	. . . . 5 |- ( x = B -> ( x e. A <-> B e. A ) )
2	1	anbi2d 740	. . . 4 |- ( x = B -> ( ( Ord A /\ x e. A ) <-> ( Ord A /\ B e. A ) ) )
3		ordeq 5730	. . . 4 |- ( x = B -> ( Ord x <-> Ord B ) )
4	2, 3	imbi12d 334	. . 3 |- ( x = B -> ( ( ( Ord A /\ x e. A ) -> Ord x ) <-> ( ( Ord A /\ B e. A ) -> Ord B ) ) )
5		simpll 790	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> Ord A )
6		3anrot 1043	. . . . . . . . . . . 12 |- ( ( x e. A /\ z e. y /\ y e. x ) <-> ( z e. y /\ y e. x /\ x e. A ) )
7		3anass 1042	. . . . . . . . . . . 12 |- ( ( x e. A /\ z e. y /\ y e. x ) <-> ( x e. A /\ ( z e. y /\ y e. x ) ) )
8	6, 7	bitr3i 266	. . . . . . . . . . 11 |- ( ( z e. y /\ y e. x /\ x e. A ) <-> ( x e. A /\ ( z e. y /\ y e. x ) ) )
9		ordtr 5737	. . . . . . . . . . . 12 |- ( Ord A -> Tr A )
10		trel3 4760	. . . . . . . . . . . 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 233	. . . . . . . . . 10 |- ( Ord A -> ( ( x e. A /\ ( z e. y /\ y e. x ) ) -> z e. A ) )
13	12	impl 650	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> z e. A )
14		trel 4759	. . . . . . . . . . . . 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 454	. . . . . . . . . . 11 |- ( Ord A -> ( x e. A -> ( y e. x -> y e. A ) ) )
17	16	imp31 448	. . . . . . . . . 10 |- ( ( ( Ord A /\ x e. A ) /\ y e. x ) -> y e. A )
18	17	adantrl 752	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> y e. A )
19		simplr 792	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> x e. A )
20		ordwe 5736	. . . . . . . . . 10 |- ( Ord A -> _E We A )
21		wetrep 5107	. . . . . . . . . 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 488	. . . . . . . . 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 1328	. . . . . . . 8 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> ( ( z e. y /\ y e. x ) -> z e. x ) )
24	23	ex 450	. . . . . . 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 53	. . . . . 6 |- ( ( Ord A /\ x e. A ) -> ( ( z e. y /\ y e. x ) -> z e. x ) )
26	25	alrimivv 1856	. . . . 5 |- ( ( Ord A /\ x e. A ) -> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
27		dftr2 4754	. . . . 5 |- ( Tr x <-> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
28	26, 27	sylibr 224	. . . 4 |- ( ( Ord A /\ x e. A ) -> Tr x )
29		trss 4761	. . . . . . 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 5101	. . . . . 6 |- ( x C_ A -> ( _E We A -> _E We x ) )
32	30, 20, 31	syl6ci 71	. . . . 5 |- ( Ord A -> ( x e. A -> _E We x ) )
33	32	imp 445	. . . 4 |- ( ( Ord A /\ x e. A ) -> _E We x )
34		df-ord 5726	. . . 4 |- ( Ord x <-> ( Tr x /\ _E We x ) )
35	28, 33, 34	sylanbrc 698	. . 3 |- ( ( Ord A /\ x e. A ) -> Ord x )
36	4, 35	vtoclg 3266	. 2 |- ( B e. A -> ( ( Ord A /\ B e. A ) -> Ord B ) )
37	36	anabsi7 860	1 |- ( ( Ord A /\ B e. A ) -> Ord B )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037   A.wal 1481   = wceq 1483   e. wcel 1990   C_ wss 3574   Tr wtr 4752   _E cep 5028   We wwe 5072   Ord word 5722

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-tr 4753  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-ord 5726

This theorem is referenced by:  tron  5746  ordelon  5747  ordtr2  5768  ordtr3OLD  5770  ordintdif  5774  ordsuc  7014  ordsucss  7018  ordsucelsuc  7022  ordsucuniel  7024  limsssuc  7050  smores  7449  smo11  7461  smoord  7462  smoword  7463  smogt  7464  smorndom  7465  rdglim2  7528  oesuclem  7605  ordtypelem3  8425  r1val1  8649  rankr1ag  8665  fin23lem24  9144  onsuct0  32440  dford3  37595  ordpss  38655