Metamath Proof Explorer

Theorem ordelord

Description: An element of an ordinal class is ordinal. Proposition 7.6 of TakeutiZaring p. 36. (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 syl5bir 
 |-  ( 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 )