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=\left\{⟨x,y⟩|\left(\left(x\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge y\in \left(\mathrm{On}\times \mathrm{On}\right)\right)\wedge \left(1^{st}\left(x\right)\in 1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\in 2^{nd}\left(y\right)\right)\right)\right)\right\}$$
Assertion	leweon	$$⊢L\mathrm{We}\left(\mathrm{On}\times \mathrm{On}\right)$$

Proof

Step	Hyp	Ref	Expression
1		leweon.1	$$⊢L=\left\{⟨x,y⟩|\left(\left(x\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge y\in \left(\mathrm{On}\times \mathrm{On}\right)\right)\wedge \left(1^{st}\left(x\right)\in 1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\in 2^{nd}\left(y\right)\right)\right)\right)\right\}$$
2		epweon	$$⊢\mathrm{E}\mathrm{We}\mathrm{On}$$
3		fvex	$$⊢1^{st}\left(y\right)\in \mathrm{V}$$
4	3	epeli	$$⊢1^{st}\left(x\right)\mathrm{E}{1}^{st}\left(y\right)\leftrightarrow 1^{st}\left(x\right)\in 1^{st}\left(y\right)$$
5		fvex	$$⊢2^{nd}\left(y\right)\in \mathrm{V}$$
6	5	epeli	$$⊢2^{nd}\left(x\right)\mathrm{E}{2}^{nd}\left(y\right)\leftrightarrow 2^{nd}\left(x\right)\in 2^{nd}\left(y\right)$$
7	6	anbi2i	$$⊢\left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\mathrm{E}{2}^{nd}\left(y\right)\right)\leftrightarrow \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\in 2^{nd}\left(y\right)\right)$$
8	4 7	orbi12i	$$⊢\left(1^{st}\left(x\right)\mathrm{E}{1}^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\mathrm{E}{2}^{nd}\left(y\right)\right)\right)\leftrightarrow \left(1^{st}\left(x\right)\in 1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\in 2^{nd}\left(y\right)\right)\right)$$
9	8	anbi2i	$$⊢\left(\left(x\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge y\in \left(\mathrm{On}\times \mathrm{On}\right)\right)\wedge \left(1^{st}\left(x\right)\mathrm{E}{1}^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\mathrm{E}{2}^{nd}\left(y\right)\right)\right)\right)\leftrightarrow \left(\left(x\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge y\in \left(\mathrm{On}\times \mathrm{On}\right)\right)\wedge \left(1^{st}\left(x\right)\in 1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\in 2^{nd}\left(y\right)\right)\right)\right)$$
10	9	opabbii	$$⊢\left\{⟨x,y⟩|\left(\left(x\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge y\in \left(\mathrm{On}\times \mathrm{On}\right)\right)\wedge \left(1^{st}\left(x\right)\mathrm{E}{1}^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\mathrm{E}{2}^{nd}\left(y\right)\right)\right)\right)\right\}=\left\{⟨x,y⟩|\left(\left(x\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge y\in \left(\mathrm{On}\times \mathrm{On}\right)\right)\wedge \left(1^{st}\left(x\right)\in 1^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\in 2^{nd}\left(y\right)\right)\right)\right)\right\}$$
11	1 10	eqtr4i	$$⊢L=\left\{⟨x,y⟩|\left(\left(x\in \left(\mathrm{On}\times \mathrm{On}\right)\wedge y\in \left(\mathrm{On}\times \mathrm{On}\right)\right)\wedge \left(1^{st}\left(x\right)\mathrm{E}{1}^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)\mathrm{E}{2}^{nd}\left(y\right)\right)\right)\right)\right\}$$
12	11	wexp	$$⊢\left(\mathrm{E}\mathrm{We}\mathrm{On}\wedge \mathrm{E}\mathrm{We}\mathrm{On}\right)\to L\mathrm{We}\left(\mathrm{On}\times \mathrm{On}\right)$$
13	2 2 12	mp2an	$$⊢L\mathrm{We}\left(\mathrm{On}\times \mathrm{On}\right)$$