Theorem ordelord 5434

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 2476	. . . . 5 |- ( x = B -> ( x e. A <-> B e. A ) )
2	1	anbi2d 704	. . . 4 |- ( x = B -> ( ( Ord A /\ x e. A ) <-> ( Ord A /\ B e. A ) ) )
3		ordeq 5419	. . . 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 754	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> Ord A )
6		3anrot 981	. . . . . . . . . . . 12 |- ( ( x e. A /\ z e. y /\ y e. x ) <-> ( z e. y /\ y e. x /\ x e. A ) )
7		3anass 980	. . . . . . . . . . . 12 |- ( ( x e. A /\ z e. y /\ y e. x ) <-> ( x e. A /\ ( z e. y /\ y e. x ) ) )
8	6, 7	bitr3i 253	. . . . . . . . . . 11 |- ( ( z e. y /\ y e. x /\ x e. A ) <-> ( x e. A /\ ( z e. y /\ y e. x ) ) )
9		ordtr 5426	. . . . . . . . . . . 12 |- ( Ord A -> Tr A )
10		trel3 4499	. . . . . . . . . . . 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 220	. . . . . . . . . 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 4498	. . . . . . . . . . . . 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 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 716	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> y e. A )
19		simplr 756	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> x e. A )
20		ordwe 5425	. . . . . . . . . 10 |- ( Ord A -> _E We A )
21		wetrep 4818	. . . . . . . . . 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 1234	. . . . . . . 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 49	. . . . . 6 |- ( ( Ord A /\ x e. A ) -> ( ( z e. y /\ y e. x ) -> z e. x ) )
26	25	alrimivv 1743	. . . . 5 |- ( ( Ord A /\ x e. A ) -> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
27		dftr2 4493	. . . . 5 |- ( Tr x <-> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
28	26, 27	sylibr 214	. . . 4 |- ( ( Ord A /\ x e. A ) -> Tr x )
29		trss 4500	. . . . . . 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 4812	. . . . . 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 429	. . . 4 |- ( ( Ord A /\ x e. A ) -> _E We x )
34		df-ord 5415	. . . 4 |- ( Ord x <-> ( Tr x /\ _E We x ) )
35	28, 33, 34	sylanbrc 664	. . 3 |- ( ( Ord A /\ x e. A ) -> Ord x )
36	4, 35	vtoclg 3119	. 2 |- ( B e. A -> ( ( Ord A /\ B e. A ) -> Ord B ) )
37	36	anabsi7 822	1 |- ( ( Ord A /\ B e. A ) -> Ord B )

Syntax hints:   -> wi 4   /\ wa 369   /\ w3a 976   A.wal 1405   = wceq 1407   e. wcel 1844   C_ wss 3416   Tr wtr 4491   _E cep 4734   We wwe 4783   Ord word 5411

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-9 1848  ax-10 1863  ax-11 1868  ax-12 1880  ax-13 2028  ax-ext 2382  ax-sep 4519  ax-nul 4527  ax-pr 4632

This theorem depends on definitions:  df-bi 187  df-or 370  df-an 371  df-3an 978  df-tru 1410  df-ex 1636  df-nf 1640  df-sb 1766  df-eu 2244  df-mo 2245  df-clab 2390  df-cleq 2396  df-clel 2399  df-nfc 2554  df-ne 2602  df-ral 2761  df-rex 2762  df-rab 2765  df-v 3063  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3741  df-if 3888  df-sn 3975  df-pr 3977  df-op 3981  df-uni 4194  df-br 4398  df-opab 4456  df-tr 4492  df-eprel 4736  df-po 4746  df-so 4747  df-fr 4784  df-we 4786  df-ord 5415

This theorem is referenced by:  tron  5435  ordelon  5436  ordtr2  5456  ordtr3  5457  ordintdif  5461  ordsuc  6634  ordsucss  6638  ordsucelsuc  6642  ordsucuniel  6644  limsssuc  6670  smores  7058  smo11  7070  smoord  7071  smoword  7072  smogt  7073  smorndom  7074  rdglim2  7137  oesuclem  7214  ordtypelem3  7981  r1val1  8238  rankr1ag  8254  fin23lem24  8736  onsuct0  30686  dford3  35345  ordpss  36221