Theorem ordelord

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

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

Proof

Step	Hyp	Ref	Expression
1		eleq1	|- ( x = B -> ( x e. A <-> B e. A ) )
2	1	anbi2d	|- ( x = B -> ( ( Ord A /\ x e. A ) <-> ( Ord A /\ B e. A ) ) )
3		ordeq	|- ( x = B -> ( Ord x <-> Ord B ) )
4	2 3	imbi12d	|- ( x = B -> ( ( ( Ord A /\ x e. A ) -> Ord x ) <-> ( ( Ord A /\ B e. A ) -> Ord B ) ) )
5		simpll	|- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> Ord A )
6		3anrot	|- ( ( x e. A /\ z e. y /\ y e. x ) <-> ( z e. y /\ y e. x /\ x e. A ) )
7		3anass	|- ( ( x e. A /\ z e. y /\ y e. x ) <-> ( x e. A /\ ( z e. y /\ y e. x ) ) )
8	6 7	bitr3i	|- ( ( z e. y /\ y e. x /\ x e. A ) <-> ( x e. A /\ ( z e. y /\ y e. x ) ) )
9		ordtr	|- ( Ord A -> Tr A )
10		trel3	|- ( Tr A -> ( ( z e. y /\ y e. x /\ x e. A ) -> z e. A ) )
11	9 10	syl	|- ( Ord A -> ( ( z e. y /\ y e. x /\ x e. A ) -> z e. A ) )
12	8 11	biimtrrid	|- ( Ord A -> ( ( x e. A /\ ( z e. y /\ y e. x ) ) -> z e. A ) )
13	12	impl	|- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> z e. A )
14		trel	|- ( Tr A -> ( ( y e. x /\ x e. A ) -> y e. A ) )
15	9 14	syl	|- ( Ord A -> ( ( y e. x /\ x e. A ) -> y e. A ) )
16	15	expcomd	|- ( Ord A -> ( x e. A -> ( y e. x -> y e. A ) ) )
17	16	imp31	|- ( ( ( Ord A /\ x e. A ) /\ y e. x ) -> y e. A )
18	17	adantrl	|- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> y e. A )
19		simplr	|- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> x e. A )
20		ordwe	|- ( Ord A -> _E We A )
21		wetrep	|- ( ( _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	|- ( ( 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	|- ( ( ( Ord A /\ x e. A ) /\ ( z e. y /\ y e. x ) ) -> ( ( z e. y /\ y e. x ) -> z e. x ) )
24	23	ex	|- ( ( Ord A /\ x e. A ) -> ( ( z e. y /\ y e. x ) -> ( ( z e. y /\ y e. x ) -> z e. x ) ) )
25	24	pm2.43d	|- ( ( Ord A /\ x e. A ) -> ( ( z e. y /\ y e. x ) -> z e. x ) )
26	25	alrimivv	|- ( ( Ord A /\ x e. A ) -> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
27		dftr2	|- ( Tr x <-> A. z A. y ( ( z e. y /\ y e. x ) -> z e. x ) )
28	26 27	sylibr	|- ( ( Ord A /\ x e. A ) -> Tr x )
29		trss	|- ( Tr A -> ( x e. A -> x C_ A ) )
30	9 29	syl	|- ( Ord A -> ( x e. A -> x C_ A ) )
31		wess	|- ( x C_ A -> ( _E We A -> _E We x ) )
32	30 20 31	syl6ci	|- ( Ord A -> ( x e. A -> _E We x ) )
33	32	imp	|- ( ( Ord A /\ x e. A ) -> _E We x )
34		df-ord	|- ( Ord x <-> ( Tr x /\ _E We x ) )
35	28 33 34	sylanbrc	|- ( ( Ord A /\ x e. A ) -> Ord x )
36	4 35	vtoclg	|- ( B e. A -> ( ( Ord A /\ B e. A ) -> Ord B ) )
37	36	anabsi7	|- ( ( Ord A /\ B e. A ) -> Ord B )