Metamath Proof Explorer

Theorem leweon

Description: Lexicographical order is a well-ordering of On X. On . Proposition 7.56(1) of TakeutiZaring p. 54. Note that unlike r0weon , this order isnot set-like, as the preimage of <. 1o , (/) >. is the proper class ( { (/) } X. On ) . (Contributed by Mario Carneiro, 9-Mar-2013)

Ref Expression
Hypothesis leweon.1 
|- L = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) }
Assertion leweon 
|- L We ( On X. On )

Proof

Step Hyp Ref Expression
1 leweon.1 
 |-  L = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) }
2 epweon 
 |-  _E We On
3 fvex 
 |-  ( 1st ` y ) e. _V
4 3 epeli 
 |-  ( ( 1st ` x ) _E ( 1st ` y ) <-> ( 1st ` x ) e. ( 1st ` y ) )
5 fvex 
 |-  ( 2nd ` y ) e. _V
6 5 epeli 
 |-  ( ( 2nd ` x ) _E ( 2nd ` y ) <-> ( 2nd ` x ) e. ( 2nd ` y ) )
7 6 anbi2i 
 |-  ( ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) _E ( 2nd ` y ) ) <-> ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) )
8 4 7 orbi12i 
 |-  ( ( ( 1st ` x ) _E ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) _E ( 2nd ` y ) ) ) <-> ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) )
9 8 anbi2i 
 |-  ( ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) _E ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) _E ( 2nd ` y ) ) ) ) <-> ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) )
10 9 opabbii 
 |-  { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) _E ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) _E ( 2nd ` y ) ) ) ) } = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) e. ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) e. ( 2nd ` y ) ) ) ) }
11 1 10 eqtr4i 
 |-  L = { <. x , y >. | ( ( x e. ( On X. On ) /\ y e. ( On X. On ) ) /\ ( ( 1st ` x ) _E ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) _E ( 2nd ` y ) ) ) ) }
12 11 wexp 
 |-  ( ( _E We On /\ _E We On ) -> L We ( On X. On ) )
13 2 2 12 mp2an 
 |-  L We ( On X. On )