Theorem wexp

Description: A lexicographical ordering of two well-ordered classes. (Contributed by Scott Fenton, 17-Mar-2011) (Revised by Mario Carneiro, 7-Mar-2013)

	Ref	Expression
Hypothesis	wexp.1	$$⊢T=\left\{⟨x,y⟩|\left(\left(x\in \left(A\times B\right)\wedge y\in \left(A\times B\right)\right)\wedge \left(1^{st}\left(x\right)R{1}^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)S{2}^{nd}\left(y\right)\right)\right)\right)\right\}$$
Assertion	wexp	$$⊢\left(R\mathrm{We}A\wedge S\mathrm{We}B\right)\to T\mathrm{We}\left(A\times B\right)$$

Proof

Step	Hyp	Ref	Expression
1		wexp.1	$$⊢T=\left\{⟨x,y⟩|\left(\left(x\in \left(A\times B\right)\wedge y\in \left(A\times B\right)\right)\wedge \left(1^{st}\left(x\right)R{1}^{st}\left(y\right)\vee \left(1^{st}\left(x\right)=1^{st}\left(y\right)\wedge 2^{nd}\left(x\right)S{2}^{nd}\left(y\right)\right)\right)\right)\right\}$$
2		wefr	$$⊢R\mathrm{We}A\to R\mathrm{Fr}A$$
3		wefr	$$⊢S\mathrm{We}B\to S\mathrm{Fr}B$$
4	1	frxp	$$⊢\left(R\mathrm{Fr}A\wedge S\mathrm{Fr}B\right)\to T\mathrm{Fr}\left(A\times B\right)$$
5	2 3 4	syl2an	$$⊢\left(R\mathrm{We}A\wedge S\mathrm{We}B\right)\to T\mathrm{Fr}\left(A\times B\right)$$
6		weso	$$⊢R\mathrm{We}A\to R\mathrm{Or}A$$
7		weso	$$⊢S\mathrm{We}B\to S\mathrm{Or}B$$
8	1	soxp	$$⊢\left(R\mathrm{Or}A\wedge S\mathrm{Or}B\right)\to T\mathrm{Or}\left(A\times B\right)$$
9	6 7 8	syl2an	$$⊢\left(R\mathrm{We}A\wedge S\mathrm{We}B\right)\to T\mathrm{Or}\left(A\times B\right)$$
10		df-we	$$⊢T\mathrm{We}\left(A\times B\right)\leftrightarrow \left(T\mathrm{Fr}\left(A\times B\right)\wedge T\mathrm{Or}\left(A\times B\right)\right)$$
11	5 9 10	sylanbrc	$$⊢\left(R\mathrm{We}A\wedge S\mathrm{We}B\right)\to T\mathrm{We}\left(A\times B\right)$$