Theorem ordelord 5464

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 2495	. . . . 5 |- ( x = B -> ( x e. A <-> B e. A ) )
2	1	anbi2d 708	. . . 4 |- ( x = B -> ( ( Ord A /\ x e. A ) <-> ( Ord A /\ B e. A ) ) )
3		ordeq 5449	. . . 4 |- ( x = B -> ( Ord x <-> Ord B ) )
4	2, 3	imbi12d 321	. . 3 |- ( x = B -> ( ( ( Ord A /\ x e. A ) -> Ord x ) <-> ( ( Ord A /\ B e. A ) -> Ord B ) ) )
5		simpll 758	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> Ord A )
6		3anrot 987	. . . . . . . . . . . 12 |- ( ( x e. A /\ z e. y /\ y e. x ) <-> ( z e. y /\ y e. x /\ x e. A ) )
7		3anass 986	. . . . . . . . . . . 12 |- ( ( x e. A /\ z e. y /\ y e. x ) <-> ( x e. A /\ ( z e. y /\ y e. x ) ) )
8	6, 7	bitr3i 254	. . . . . . . . . . 11 |- ( ( z e. y /\ y e. x /\ x e. A ) <-> ( x e. A /\ ( z e. y /\ y e. x ) ) )
9		ordtr 5456	. . . . . . . . . . . 12 |- ( Ord A -> Tr A )
10		trel3 4526	. . . . . . . . . . . 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 221	. . . . . . . . . 10 |- ( Ord A -> ( ( x e. A /\ ( z e. y /\ y e. x ) ) -> z e. A ) )
13	12	impl 624	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> z e. A )
14		trel 4525	. . . . . . . . . . . . 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 439	. . . . . . . . . . 11 |- ( Ord A -> ( x e. A -> ( y e. x -> y e. A ) ) )
17	16	imp31 433	. . . . . . . . . 10 |- ( ( ( Ord A /\ x e. A ) /\ y e. x ) -> y e. A )
18	17	adantrl 720	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> y e. A )
19		simplr 760	. . . . . . . . 9 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> x e. A )
20		ordwe 5455	. . . . . . . . . 10 |- ( Ord A -> _E We A )
21		wetrep 4846	. . . . . . . . . 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 473	. . . . . . . . 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 1266	. . . . . . . 8 |- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> ( ( z e. y /\ y e. x ) -> z e. x ) )
24	23	ex 435	. . . . . . 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 50	. . . . . 6 |- ( ( Ord A /\ x e. A ) -> ( ( z e. y /\ y e. x ) -> z e. x ) )
26	25	alrimivv 1768	. . . . 5 |- ( ( Ord A /\ x e. A ) -> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
27		dftr2 4520	. . . . 5 |- ( Tr x <-> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
28	26, 27	sylibr 215	. . . 4 |- ( ( Ord A /\ x e. A ) -> Tr x )
29		trss 4527	. . . . . . 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 4840	. . . . . 6 |- ( x C_ A -> ( _E We A -> _E We x ) )
32	30, 20, 31	syl6ci 67	. . . . 5 |- ( Ord A -> ( x e. A -> _E We x ) )
33	32	imp 430	. . . 4 |- ( ( Ord A /\ x e. A ) -> _E We x )
34		df-ord 5445	. . . 4 |- ( Ord x <-> ( Tr x /\ _E We x ) )
35	28, 33, 34	sylanbrc 668	. . 3 |- ( ( Ord A /\ x e. A ) -> Ord x )
36	4, 35	vtoclg 3139	. 2 |- ( B e. A -> ( ( Ord A /\ B e. A ) -> Ord B ) )
37	36	anabsi7 826	1 |- ( ( Ord A /\ B e. A ) -> Ord B )

Syntax hints:   -> wi 4   /\ wa 370   /\ w3a 982   A.wal 1435   = wceq 1437   e. wcel 1872   C_ wss 3436   Tr wtr 4518   _E cep 4762   We wwe 4811   Ord word 5441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-tr 4519  df-eprel 4764  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-ord 5445

This theorem is referenced by:  tron  5465  ordelon  5466  ordtr2  5486  ordtr3  5487  ordintdif  5491  ordsuc  6655  ordsucss  6659  ordsucelsuc  6663  ordsucuniel  6665  limsssuc  6691  smores  7082  smo11  7094  smoord  7095  smoword  7096  smogt  7097  smorndom  7098  rdglim2  7161  oesuclem  7238  ordtypelem3  8044  r1val1  8265  rankr1ag  8281  fin23lem24  8759  onsuct0  31106  dford3  35853  ordpss  36774