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 | |
|
Assertion | leweon | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | leweon.1 | |
|
2 | epweon | |
|
3 | fvex | |
|
4 | 3 | epeli | |
5 | fvex | |
|
6 | 5 | epeli | |
7 | 6 | anbi2i | |
8 | 4 7 | orbi12i | |
9 | 8 | anbi2i | |
10 | 9 | opabbii | |
11 | 1 10 | eqtr4i | |
12 | 11 | wexp | |
13 | 2 2 12 | mp2an | |