Metamath Proof Explorer


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 ) )