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 = { <. x , y >. | ( ( x e. ( A X. B ) /\ y e. ( A X. B ) ) /\ ( ( 1st ` x ) R ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) S ( 2nd ` y ) ) ) ) }
Assertion	wexp	|- ( ( R We A /\ S We B ) -> T We ( A X. B ) )

Proof

Step	Hyp	Ref	Expression
1		wexp.1	|- T = { <. x , y >. | ( ( x e. ( A X. B ) /\ y e. ( A X. B ) ) /\ ( ( 1st ` x ) R ( 1st ` y ) \/ ( ( 1st ` x ) = ( 1st ` y ) /\ ( 2nd ` x ) S ( 2nd ` y ) ) ) ) }
2		wefr	|- ( R We A -> R Fr A )
3		wefr	|- ( S We B -> S Fr B )
4	1	frxp	|- ( ( R Fr A /\ S Fr B ) -> T Fr ( A X. B ) )
5	2 3 4	syl2an	|- ( ( R We A /\ S We B ) -> T Fr ( A X. B ) )
6		weso	|- ( R We A -> R Or A )
7		weso	|- ( S We B -> S Or B )
8	1	soxp	|- ( ( R Or A /\ S Or B ) -> T Or ( A X. B ) )
9	6 7 8	syl2an	|- ( ( R We A /\ S We B ) -> T Or ( A X. B ) )
10		df-we	|- ( T We ( A X. B ) <-> ( T Fr ( A X. B ) /\ T Or ( A X. B ) ) )
11	5 9 10	sylanbrc	|- ( ( R We A /\ S We B ) -> T We ( A X. B ) )