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=xy|xOn×OnyOn×On1stx1sty1stx=1sty2ndx2ndy
Assertion leweon LWeOn×On

Proof

Step Hyp Ref Expression
1 leweon.1 L=xy|xOn×OnyOn×On1stx1sty1stx=1sty2ndx2ndy
2 epweon EWeOn
3 fvex 1styV
4 3 epeli 1stxE1sty1stx1sty
5 fvex 2ndyV
6 5 epeli 2ndxE2ndy2ndx2ndy
7 6 anbi2i 1stx=1sty2ndxE2ndy1stx=1sty2ndx2ndy
8 4 7 orbi12i 1stxE1sty1stx=1sty2ndxE2ndy1stx1sty1stx=1sty2ndx2ndy
9 8 anbi2i xOn×OnyOn×On1stxE1sty1stx=1sty2ndxE2ndyxOn×OnyOn×On1stx1sty1stx=1sty2ndx2ndy
10 9 opabbii xy|xOn×OnyOn×On1stxE1sty1stx=1sty2ndxE2ndy=xy|xOn×OnyOn×On1stx1sty1stx=1sty2ndx2ndy
11 1 10 eqtr4i L=xy|xOn×OnyOn×On1stxE1sty1stx=1sty2ndxE2ndy
12 11 wexp EWeOnEWeOnLWeOn×On
13 2 2 12 mp2an LWeOn×On