Metamath Proof Explorer

Theorem soxp

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

Ref Expression
Hypothesis soxp.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 soxp 
|- ( ( R Or A /\ S Or B ) -> T Or ( A X. B ) )

Proof

Step Hyp Ref Expression
1 soxp.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 sopo 
 |-  ( R Or A -> R Po A )
3 sopo 
 |-  ( S Or B -> S Po B )
4 1 poxp 
 |-  ( ( R Po A /\ S Po B ) -> T Po ( A X. B ) )
5 2 3 4 syl2an 
 |-  ( ( R Or A /\ S Or B ) -> T Po ( A X. B ) )
6 elxp 
 |-  ( t e. ( A X. B ) <-> E. a E. b ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) )
7 elxp 
 |-  ( u e. ( A X. B ) <-> E. c E. d ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) )
8 ioran 
 |-  ( -. ( ( a R c \/ ( a = c /\ b S d ) ) \/ ( a = c /\ b = d ) ) <-> ( -. ( a R c \/ ( a = c /\ b S d ) ) /\ -. ( a = c /\ b = d ) ) )
9 ioran 
 |-  ( -. ( a R c \/ ( a = c /\ b S d ) ) <-> ( -. a R c /\ -. ( a = c /\ b S d ) ) )
10 ianor 
 |-  ( -. ( a = c /\ b S d ) <-> ( -. a = c \/ -. b S d ) )
11 10 anbi2i 
 |-  ( ( -. a R c /\ -. ( a = c /\ b S d ) ) <-> ( -. a R c /\ ( -. a = c \/ -. b S d ) ) )
12 9 11 bitri 
 |-  ( -. ( a R c \/ ( a = c /\ b S d ) ) <-> ( -. a R c /\ ( -. a = c \/ -. b S d ) ) )
13 ianor 
 |-  ( -. ( a = c /\ b = d ) <-> ( -. a = c \/ -. b = d ) )
14 12 13 anbi12i 
 |-  ( ( -. ( a R c \/ ( a = c /\ b S d ) ) /\ -. ( a = c /\ b = d ) ) <-> ( ( -. a R c /\ ( -. a = c \/ -. b S d ) ) /\ ( -. a = c \/ -. b = d ) ) )
15 8 14 bitri 
 |-  ( -. ( ( a R c \/ ( a = c /\ b S d ) ) \/ ( a = c /\ b = d ) ) <-> ( ( -. a R c /\ ( -. a = c \/ -. b S d ) ) /\ ( -. a = c \/ -. b = d ) ) )
16 solin 
 |-  ( ( R Or A /\ ( a e. A /\ c e. A ) ) -> ( a R c \/ a = c \/ c R a ) )
17 3orass 
 |-  ( ( a R c \/ a = c \/ c R a ) <-> ( a R c \/ ( a = c \/ c R a ) ) )
18 df-or 
 |-  ( ( a R c \/ ( a = c \/ c R a ) ) <-> ( -. a R c -> ( a = c \/ c R a ) ) )
19 17 18 bitri 
 |-  ( ( a R c \/ a = c \/ c R a ) <-> ( -. a R c -> ( a = c \/ c R a ) ) )
20 16 19 sylib 
 |-  ( ( R Or A /\ ( a e. A /\ c e. A ) ) -> ( -. a R c -> ( a = c \/ c R a ) ) )
21 solin 
 |-  ( ( S Or B /\ ( b e. B /\ d e. B ) ) -> ( b S d \/ b = d \/ d S b ) )
22 3orass 
 |-  ( ( b S d \/ b = d \/ d S b ) <-> ( b S d \/ ( b = d \/ d S b ) ) )
23 df-or 
 |-  ( ( b S d \/ ( b = d \/ d S b ) ) <-> ( -. b S d -> ( b = d \/ d S b ) ) )
24 22 23 bitri 
 |-  ( ( b S d \/ b = d \/ d S b ) <-> ( -. b S d -> ( b = d \/ d S b ) ) )
25 21 24 sylib 
 |-  ( ( S Or B /\ ( b e. B /\ d e. B ) ) -> ( -. b S d -> ( b = d \/ d S b ) ) )
26 25 orim2d 
 |-  ( ( S Or B /\ ( b e. B /\ d e. B ) ) -> ( ( -. a = c \/ -. b S d ) -> ( -. a = c \/ ( b = d \/ d S b ) ) ) )
27 20 26 im2anan9 
 |-  ( ( ( R Or A /\ ( a e. A /\ c e. A ) ) /\ ( S Or B /\ ( b e. B /\ d e. B ) ) ) -> ( ( -. a R c /\ ( -. a = c \/ -. b S d ) ) -> ( ( a = c \/ c R a ) /\ ( -. a = c \/ ( b = d \/ d S b ) ) ) ) )
28 pm2.53 
 |-  ( ( a = c \/ c R a ) -> ( -. a = c -> c R a ) )
29 orc 
 |-  ( c R a -> ( c R a \/ ( c = a /\ d S b ) ) )
30 28 29 syl6 
 |-  ( ( a = c \/ c R a ) -> ( -. a = c -> ( c R a \/ ( c = a /\ d S b ) ) ) )
31 30 adantr 
 |-  ( ( ( a = c \/ c R a ) /\ ( -. a = c \/ ( b = d \/ d S b ) ) ) -> ( -. a = c -> ( c R a \/ ( c = a /\ d S b ) ) ) )
32 orel1 
 |-  ( -. b = d -> ( ( b = d \/ d S b ) -> d S b ) )
33 32 orim2d 
 |-  ( -. b = d -> ( ( -. a = c \/ ( b = d \/ d S b ) ) -> ( -. a = c \/ d S b ) ) )
34 33 anim2d 
 |-  ( -. b = d -> ( ( ( a = c \/ c R a ) /\ ( -. a = c \/ ( b = d \/ d S b ) ) ) -> ( ( a = c \/ c R a ) /\ ( -. a = c \/ d S b ) ) ) )
35 imor 
 |-  ( ( a = c -> d S b ) <-> ( -. a = c \/ d S b ) )
36 35 biimpri 
 |-  ( ( -. a = c \/ d S b ) -> ( a = c -> d S b ) )
37 36 com12 
 |-  ( a = c -> ( ( -. a = c \/ d S b ) -> d S b ) )
38 equcomi 
 |-  ( a = c -> c = a )
39 38 anim1i 
 |-  ( ( a = c /\ d S b ) -> ( c = a /\ d S b ) )
40 39 olcd 
 |-  ( ( a = c /\ d S b ) -> ( c R a \/ ( c = a /\ d S b ) ) )
41 40 ex 
 |-  ( a = c -> ( d S b -> ( c R a \/ ( c = a /\ d S b ) ) ) )
42 37 41 syld 
 |-  ( a = c -> ( ( -. a = c \/ d S b ) -> ( c R a \/ ( c = a /\ d S b ) ) ) )
43 29 a1d 
 |-  ( c R a -> ( ( -. a = c \/ d S b ) -> ( c R a \/ ( c = a /\ d S b ) ) ) )
44 42 43 jaoi 
 |-  ( ( a = c \/ c R a ) -> ( ( -. a = c \/ d S b ) -> ( c R a \/ ( c = a /\ d S b ) ) ) )
45 44 imp 
 |-  ( ( ( a = c \/ c R a ) /\ ( -. a = c \/ d S b ) ) -> ( c R a \/ ( c = a /\ d S b ) ) )
46 34 45 syl6com 
 |-  ( ( ( a = c \/ c R a ) /\ ( -. a = c \/ ( b = d \/ d S b ) ) ) -> ( -. b = d -> ( c R a \/ ( c = a /\ d S b ) ) ) )
47 31 46 jaod 
 |-  ( ( ( a = c \/ c R a ) /\ ( -. a = c \/ ( b = d \/ d S b ) ) ) -> ( ( -. a = c \/ -. b = d ) -> ( c R a \/ ( c = a /\ d S b ) ) ) )
48 27 47 syl6 
 |-  ( ( ( R Or A /\ ( a e. A /\ c e. A ) ) /\ ( S Or B /\ ( b e. B /\ d e. B ) ) ) -> ( ( -. a R c /\ ( -. a = c \/ -. b S d ) ) -> ( ( -. a = c \/ -. b = d ) -> ( c R a \/ ( c = a /\ d S b ) ) ) ) )
49 48 impd 
 |-  ( ( ( R Or A /\ ( a e. A /\ c e. A ) ) /\ ( S Or B /\ ( b e. B /\ d e. B ) ) ) -> ( ( ( -. a R c /\ ( -. a = c \/ -. b S d ) ) /\ ( -. a = c \/ -. b = d ) ) -> ( c R a \/ ( c = a /\ d S b ) ) ) )
50 15 49 syl5bi 
 |-  ( ( ( R Or A /\ ( a e. A /\ c e. A ) ) /\ ( S Or B /\ ( b e. B /\ d e. B ) ) ) -> ( -. ( ( a R c \/ ( a = c /\ b S d ) ) \/ ( a = c /\ b = d ) ) -> ( c R a \/ ( c = a /\ d S b ) ) ) )
51 df-3or 
 |-  ( ( ( a R c \/ ( a = c /\ b S d ) ) \/ ( a = c /\ b = d ) \/ ( c R a \/ ( c = a /\ d S b ) ) ) <-> ( ( ( a R c \/ ( a = c /\ b S d ) ) \/ ( a = c /\ b = d ) ) \/ ( c R a \/ ( c = a /\ d S b ) ) ) )
52 df-or 
 |-  ( ( ( ( a R c \/ ( a = c /\ b S d ) ) \/ ( a = c /\ b = d ) ) \/ ( c R a \/ ( c = a /\ d S b ) ) ) <-> ( -. ( ( a R c \/ ( a = c /\ b S d ) ) \/ ( a = c /\ b = d ) ) -> ( c R a \/ ( c = a /\ d S b ) ) ) )
53 51 52 bitri 
 |-  ( ( ( a R c \/ ( a = c /\ b S d ) ) \/ ( a = c /\ b = d ) \/ ( c R a \/ ( c = a /\ d S b ) ) ) <-> ( -. ( ( a R c \/ ( a = c /\ b S d ) ) \/ ( a = c /\ b = d ) ) -> ( c R a \/ ( c = a /\ d S b ) ) ) )
54 50 53 sylibr 
 |-  ( ( ( R Or A /\ ( a e. A /\ c e. A ) ) /\ ( S Or B /\ ( b e. B /\ d e. B ) ) ) -> ( ( a R c \/ ( a = c /\ b S d ) ) \/ ( a = c /\ b = d ) \/ ( c R a \/ ( c = a /\ d S b ) ) ) )
55 pm3.2 
 |-  ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) -> ( ( a R c \/ ( a = c /\ b S d ) ) -> ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) ) )
56 55 ad2ant2l 
 |-  ( ( ( R Or A /\ ( a e. A /\ c e. A ) ) /\ ( S Or B /\ ( b e. B /\ d e. B ) ) ) -> ( ( a R c \/ ( a = c /\ b S d ) ) -> ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) ) )
57 idd 
 |-  ( ( ( R Or A /\ ( a e. A /\ c e. A ) ) /\ ( S Or B /\ ( b e. B /\ d e. B ) ) ) -> ( ( a = c /\ b = d ) -> ( a = c /\ b = d ) ) )
58 simpr 
 |-  ( ( R Or A /\ ( a e. A /\ c e. A ) ) -> ( a e. A /\ c e. A ) )
59 58 ancomd 
 |-  ( ( R Or A /\ ( a e. A /\ c e. A ) ) -> ( c e. A /\ a e. A ) )
60 simpr 
 |-  ( ( S Or B /\ ( b e. B /\ d e. B ) ) -> ( b e. B /\ d e. B ) )
61 60 ancomd 
 |-  ( ( S Or B /\ ( b e. B /\ d e. B ) ) -> ( d e. B /\ b e. B ) )
62 pm3.2 
 |-  ( ( ( c e. A /\ a e. A ) /\ ( d e. B /\ b e. B ) ) -> ( ( c R a \/ ( c = a /\ d S b ) ) -> ( ( ( c e. A /\ a e. A ) /\ ( d e. B /\ b e. B ) ) /\ ( c R a \/ ( c = a /\ d S b ) ) ) ) )
63 59 61 62 syl2an 
 |-  ( ( ( R Or A /\ ( a e. A /\ c e. A ) ) /\ ( S Or B /\ ( b e. B /\ d e. B ) ) ) -> ( ( c R a \/ ( c = a /\ d S b ) ) -> ( ( ( c e. A /\ a e. A ) /\ ( d e. B /\ b e. B ) ) /\ ( c R a \/ ( c = a /\ d S b ) ) ) ) )
64 56 57 63 3orim123d 
 |-  ( ( ( R Or A /\ ( a e. A /\ c e. A ) ) /\ ( S Or B /\ ( b e. B /\ d e. B ) ) ) -> ( ( ( a R c \/ ( a = c /\ b S d ) ) \/ ( a = c /\ b = d ) \/ ( c R a \/ ( c = a /\ d S b ) ) ) -> ( ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) \/ ( a = c /\ b = d ) \/ ( ( ( c e. A /\ a e. A ) /\ ( d e. B /\ b e. B ) ) /\ ( c R a \/ ( c = a /\ d S b ) ) ) ) ) )
65 54 64 mpd 
 |-  ( ( ( R Or A /\ ( a e. A /\ c e. A ) ) /\ ( S Or B /\ ( b e. B /\ d e. B ) ) ) -> ( ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) \/ ( a = c /\ b = d ) \/ ( ( ( c e. A /\ a e. A ) /\ ( d e. B /\ b e. B ) ) /\ ( c R a \/ ( c = a /\ d S b ) ) ) ) )
66 65 an4s 
 |-  ( ( ( R Or A /\ S Or B ) /\ ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) ) -> ( ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) \/ ( a = c /\ b = d ) \/ ( ( ( c e. A /\ a e. A ) /\ ( d e. B /\ b e. B ) ) /\ ( c R a \/ ( c = a /\ d S b ) ) ) ) )
67 66 expcom 
 |-  ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) -> ( ( R Or A /\ S Or B ) -> ( ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) \/ ( a = c /\ b = d ) \/ ( ( ( c e. A /\ a e. A ) /\ ( d e. B /\ b e. B ) ) /\ ( c R a \/ ( c = a /\ d S b ) ) ) ) ) )
68 67 an4s 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( ( R Or A /\ S Or B ) -> ( ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) \/ ( a = c /\ b = d ) \/ ( ( ( c e. A /\ a e. A ) /\ ( d e. B /\ b e. B ) ) /\ ( c R a \/ ( c = a /\ d S b ) ) ) ) ) )
69 breq12 
 |-  ( ( t = <. a , b >. /\ u = <. c , d >. ) -> ( t T u <-> <. a , b >. T <. c , d >. ) )
70 eqeq12 
 |-  ( ( t = <. a , b >. /\ u = <. c , d >. ) -> ( t = u <-> <. a , b >. = <. c , d >. ) )
71 breq12 
 |-  ( ( u = <. c , d >. /\ t = <. a , b >. ) -> ( u T t <-> <. c , d >. T <. a , b >. ) )
72 71 ancoms 
 |-  ( ( t = <. a , b >. /\ u = <. c , d >. ) -> ( u T t <-> <. c , d >. T <. a , b >. ) )
73 69 70 72 3orbi123d 
 |-  ( ( t = <. a , b >. /\ u = <. c , d >. ) -> ( ( t T u \/ t = u \/ u T t ) <-> ( <. a , b >. T <. c , d >. \/ <. a , b >. = <. c , d >. \/ <. c , d >. T <. a , b >. ) ) )
74 1 xporderlem 
 |-  ( <. a , b >. T <. c , d >. <-> ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) )
75 vex 
 |-  a e. _V
76 vex 
 |-  b e. _V
77 75 76 opth 
 |-  ( <. a , b >. = <. c , d >. <-> ( a = c /\ b = d ) )
78 1 xporderlem 
 |-  ( <. c , d >. T <. a , b >. <-> ( ( ( c e. A /\ a e. A ) /\ ( d e. B /\ b e. B ) ) /\ ( c R a \/ ( c = a /\ d S b ) ) ) )
79 74 77 78 3orbi123i 
 |-  ( ( <. a , b >. T <. c , d >. \/ <. a , b >. = <. c , d >. \/ <. c , d >. T <. a , b >. ) <-> ( ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) \/ ( a = c /\ b = d ) \/ ( ( ( c e. A /\ a e. A ) /\ ( d e. B /\ b e. B ) ) /\ ( c R a \/ ( c = a /\ d S b ) ) ) ) )
80 73 79 bitrdi 
 |-  ( ( t = <. a , b >. /\ u = <. c , d >. ) -> ( ( t T u \/ t = u \/ u T t ) <-> ( ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) \/ ( a = c /\ b = d ) \/ ( ( ( c e. A /\ a e. A ) /\ ( d e. B /\ b e. B ) ) /\ ( c R a \/ ( c = a /\ d S b ) ) ) ) ) )
81 80 biimprcd 
 |-  ( ( ( ( ( a e. A /\ c e. A ) /\ ( b e. B /\ d e. B ) ) /\ ( a R c \/ ( a = c /\ b S d ) ) ) \/ ( a = c /\ b = d ) \/ ( ( ( c e. A /\ a e. A ) /\ ( d e. B /\ b e. B ) ) /\ ( c R a \/ ( c = a /\ d S b ) ) ) ) -> ( ( t = <. a , b >. /\ u = <. c , d >. ) -> ( t T u \/ t = u \/ u T t ) ) )
82 68 81 syl6 
 |-  ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( ( R Or A /\ S Or B ) -> ( ( t = <. a , b >. /\ u = <. c , d >. ) -> ( t T u \/ t = u \/ u T t ) ) ) )
83 82 com3r 
 |-  ( ( t = <. a , b >. /\ u = <. c , d >. ) -> ( ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) -> ( ( R Or A /\ S Or B ) -> ( t T u \/ t = u \/ u T t ) ) ) )
84 83 imp 
 |-  ( ( ( t = <. a , b >. /\ u = <. c , d >. ) /\ ( ( a e. A /\ b e. B ) /\ ( c e. A /\ d e. B ) ) ) -> ( ( R Or A /\ S Or B ) -> ( t T u \/ t = u \/ u T t ) ) )
85 84 an4s 
 |-  ( ( ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) ) -> ( ( R Or A /\ S Or B ) -> ( t T u \/ t = u \/ u T t ) ) )
86 85 expcom 
 |-  ( ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) -> ( ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) -> ( ( R Or A /\ S Or B ) -> ( t T u \/ t = u \/ u T t ) ) ) )
87 86 exlimivv 
 |-  ( E. c E. d ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) -> ( ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) -> ( ( R Or A /\ S Or B ) -> ( t T u \/ t = u \/ u T t ) ) ) )
88 87 com12 
 |-  ( ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) -> ( E. c E. d ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) -> ( ( R Or A /\ S Or B ) -> ( t T u \/ t = u \/ u T t ) ) ) )
89 88 exlimivv 
 |-  ( E. a E. b ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) -> ( E. c E. d ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) -> ( ( R Or A /\ S Or B ) -> ( t T u \/ t = u \/ u T t ) ) ) )
90 89 imp 
 |-  ( ( E. a E. b ( t = <. a , b >. /\ ( a e. A /\ b e. B ) ) /\ E. c E. d ( u = <. c , d >. /\ ( c e. A /\ d e. B ) ) ) -> ( ( R Or A /\ S Or B ) -> ( t T u \/ t = u \/ u T t ) ) )
91 6 7 90 syl2anb 
 |-  ( ( t e. ( A X. B ) /\ u e. ( A X. B ) ) -> ( ( R Or A /\ S Or B ) -> ( t T u \/ t = u \/ u T t ) ) )
92 91 com12 
 |-  ( ( R Or A /\ S Or B ) -> ( ( t e. ( A X. B ) /\ u e. ( A X. B ) ) -> ( t T u \/ t = u \/ u T t ) ) )
93 92 ralrimivv 
 |-  ( ( R Or A /\ S Or B ) -> A. t e. ( A X. B ) A. u e. ( A X. B ) ( t T u \/ t = u \/ u T t ) )
94 df-so 
 |-  ( T Or ( A X. B ) <-> ( T Po ( A X. B ) /\ A. t e. ( A X. B ) A. u e. ( A X. B ) ( t T u \/ t = u \/ u T t ) ) )
95 5 93 94 sylanbrc 
 |-  ( ( R Or A /\ S Or B ) -> T Or ( A X. B ) )