Metamath Proof Explorer


Theorem poxp

Description: A lexicographical ordering of two posets. (Contributed by Scott Fenton, 16-Mar-2011) (Revised by Mario Carneiro, 7-Mar-2013)

Ref Expression
Hypothesis poxp.1 T = x y | x A × B y A × B 1 st x R 1 st y 1 st x = 1 st y 2 nd x S 2 nd y
Assertion poxp R Po A S Po B T Po A × B

Proof

Step Hyp Ref Expression
1 poxp.1 T = x y | x A × B y A × B 1 st x R 1 st y 1 st x = 1 st y 2 nd x S 2 nd y
2 elxp t A × B a b t = a b a A b B
3 elxp u A × B c d u = c d c A d B
4 elxp v A × B e f v = e f e A f B
5 3an6 t = a b a A b B u = c d c A d B v = e f e A f B t = a b u = c d v = e f a A b B c A d B e A f B
6 poirr R Po A a A ¬ a R a
7 6 ex R Po A a A ¬ a R a
8 poirr S Po B b B ¬ b S b
9 8 intnand S Po B b B ¬ a = a b S b
10 9 ex S Po B b B ¬ a = a b S b
11 7 10 im2anan9 R Po A S Po B a A b B ¬ a R a ¬ a = a b S b
12 ioran ¬ a R a a = a b S b ¬ a R a ¬ a = a b S b
13 11 12 syl6ibr R Po A S Po B a A b B ¬ a R a a = a b S b
14 13 imp R Po A S Po B a A b B ¬ a R a a = a b S b
15 14 intnand R Po A S Po B a A b B ¬ a A a A b B b B a R a a = a b S b
16 15 3ad2antr1 R Po A S Po B a A b B c A d B e A f B ¬ a A a A b B b B a R a a = a b S b
17 an4 a A c A b B d B a R c a = c b S d c A e A d B f B c R e c = e d S f a A c A b B d B c A e A d B f B a R c a = c b S d c R e c = e d S f
18 3an6 a A b B c A d B e A f B a A c A e A b B d B f B
19 potr R Po A a A c A e A a R c c R e a R e
20 19 3impia R Po A a A c A e A a R c c R e a R e
21 20 orcd R Po A a A c A e A a R c c R e a R e a = e b S f
22 21 3expia R Po A a A c A e A a R c c R e a R e a = e b S f
23 22 expdimp R Po A a A c A e A a R c c R e a R e a = e b S f
24 breq2 c = e a R c a R e
25 24 biimpa c = e a R c a R e
26 25 orcd c = e a R c a R e a = e b S f
27 26 expcom a R c c = e a R e a = e b S f
28 27 adantrd a R c c = e d S f a R e a = e b S f
29 28 adantl R Po A a A c A e A a R c c = e d S f a R e a = e b S f
30 23 29 jaod R Po A a A c A e A a R c c R e c = e d S f a R e a = e b S f
31 30 ex R Po A a A c A e A a R c c R e c = e d S f a R e a = e b S f
32 potr S Po B b B d B f B b S d d S f b S f
33 32 expdimp S Po B b B d B f B b S d d S f b S f
34 33 anim2d S Po B b B d B f B b S d c = e d S f c = e b S f
35 34 orim2d S Po B b B d B f B b S d c R e c = e d S f c R e c = e b S f
36 breq1 a = c a R e c R e
37 equequ1 a = c a = e c = e
38 37 anbi1d a = c a = e b S f c = e b S f
39 36 38 orbi12d a = c a R e a = e b S f c R e c = e b S f
40 39 imbi2d a = c c R e c = e d S f a R e a = e b S f c R e c = e d S f c R e c = e b S f
41 35 40 syl5ibr a = c S Po B b B d B f B b S d c R e c = e d S f a R e a = e b S f
42 41 expd a = c S Po B b B d B f B b S d c R e c = e d S f a R e a = e b S f
43 42 com12 S Po B b B d B f B a = c b S d c R e c = e d S f a R e a = e b S f
44 43 impd S Po B b B d B f B a = c b S d c R e c = e d S f a R e a = e b S f
45 31 44 jaao R Po A a A c A e A S Po B b B d B f B a R c a = c b S d c R e c = e d S f a R e a = e b S f
46 45 impd R Po A a A c A e A S Po B b B d B f B a R c a = c b S d c R e c = e d S f a R e a = e b S f
47 46 an4s R Po A S Po B a A c A e A b B d B f B a R c a = c b S d c R e c = e d S f a R e a = e b S f
48 18 47 sylan2b R Po A S Po B a A b B c A d B e A f B a R c a = c b S d c R e c = e d S f a R e a = e b S f
49 an4 a A b B e A f B a A e A b B f B
50 49 biimpi a A b B e A f B a A e A b B f B
51 50 3adant2 a A b B c A d B e A f B a A e A b B f B
52 51 adantl R Po A S Po B a A b B c A d B e A f B a A e A b B f B
53 48 52 jctild R Po A S Po B a A b B c A d B e A f B a R c a = c b S d c R e c = e d S f a A e A b B f B a R e a = e b S f
54 53 adantld R Po A S Po B a A b B c A d B e A f B a A c A b B d B c A e A d B f B a R c a = c b S d c R e c = e d S f a A e A b B f B a R e a = e b S f
55 17 54 syl5bi R Po A S Po B a A b B c A d B e A f B a A c A b B d B a R c a = c b S d c A e A d B f B c R e c = e d S f a A e A b B f B a R e a = e b S f
56 16 55 jca R Po A S Po B a A b B c A d B e A f B ¬ a A a A b B b B a R a a = a b S b a A c A b B d B a R c a = c b S d c A e A d B f B c R e c = e d S f a A e A b B f B a R e a = e b S f
57 breq12 t = a b t = a b t T t a b T a b
58 57 anidms t = a b t T t a b T a b
59 58 notbid t = a b ¬ t T t ¬ a b T a b
60 59 3ad2ant1 t = a b u = c d v = e f ¬ t T t ¬ a b T a b
61 breq12 t = a b u = c d t T u a b T c d
62 61 3adant3 t = a b u = c d v = e f t T u a b T c d
63 breq12 u = c d v = e f u T v c d T e f
64 63 3adant1 t = a b u = c d v = e f u T v c d T e f
65 62 64 anbi12d t = a b u = c d v = e f t T u u T v a b T c d c d T e f
66 breq12 t = a b v = e f t T v a b T e f
67 66 3adant2 t = a b u = c d v = e f t T v a b T e f
68 65 67 imbi12d t = a b u = c d v = e f t T u u T v t T v a b T c d c d T e f a b T e f
69 60 68 anbi12d t = a b u = c d v = e f ¬ t T t t T u u T v t T v ¬ a b T a b a b T c d c d T e f a b T e f
70 1 xporderlem a b T a b a A a A b B b B a R a a = a b S b
71 70 notbii ¬ a b T a b ¬ a A a A b B b B a R a a = a b S b
72 1 xporderlem a b T c d a A c A b B d B a R c a = c b S d
73 1 xporderlem c d T e f c A e A d B f B c R e c = e d S f
74 72 73 anbi12i a b T c d c d T e f a A c A b B d B a R c a = c b S d c A e A d B f B c R e c = e d S f
75 1 xporderlem a b T e f a A e A b B f B a R e a = e b S f
76 74 75 imbi12i a b T c d c d T e f a b T e f a A c A b B d B a R c a = c b S d c A e A d B f B c R e c = e d S f a A e A b B f B a R e a = e b S f
77 71 76 anbi12i ¬ a b T a b a b T c d c d T e f a b T e f ¬ a A a A b B b B a R a a = a b S b a A c A b B d B a R c a = c b S d c A e A d B f B c R e c = e d S f a A e A b B f B a R e a = e b S f
78 69 77 bitrdi t = a b u = c d v = e f ¬ t T t t T u u T v t T v ¬ a A a A b B b B a R a a = a b S b a A c A b B d B a R c a = c b S d c A e A d B f B c R e c = e d S f a A e A b B f B a R e a = e b S f
79 56 78 syl5ibr t = a b u = c d v = e f R Po A S Po B a A b B c A d B e A f B ¬ t T t t T u u T v t T v
80 79 expcomd t = a b u = c d v = e f a A b B c A d B e A f B R Po A S Po B ¬ t T t t T u u T v t T v
81 80 imp t = a b u = c d v = e f a A b B c A d B e A f B R Po A S Po B ¬ t T t t T u u T v t T v
82 5 81 sylbi t = a b a A b B u = c d c A d B v = e f e A f B R Po A S Po B ¬ t T t t T u u T v t T v
83 82 3exp t = a b a A b B u = c d c A d B v = e f e A f B R Po A S Po B ¬ t T t t T u u T v t T v
84 83 com3l u = c d c A d B v = e f e A f B t = a b a A b B R Po A S Po B ¬ t T t t T u u T v t T v
85 84 exlimivv c d u = c d c A d B v = e f e A f B t = a b a A b B R Po A S Po B ¬ t T t t T u u T v t T v
86 85 com3l v = e f e A f B t = a b a A b B c d u = c d c A d B R Po A S Po B ¬ t T t t T u u T v t T v
87 86 exlimivv e f v = e f e A f B t = a b a A b B c d u = c d c A d B R Po A S Po B ¬ t T t t T u u T v t T v
88 87 com3l t = a b a A b B c d u = c d c A d B e f v = e f e A f B R Po A S Po B ¬ t T t t T u u T v t T v
89 88 exlimivv a b t = a b a A b B c d u = c d c A d B e f v = e f e A f B R Po A S Po B ¬ t T t t T u u T v t T v
90 89 3imp a b t = a b a A b B c d u = c d c A d B e f v = e f e A f B R Po A S Po B ¬ t T t t T u u T v t T v
91 2 3 4 90 syl3anb t A × B u A × B v A × B R Po A S Po B ¬ t T t t T u u T v t T v
92 91 3expia t A × B u A × B v A × B R Po A S Po B ¬ t T t t T u u T v t T v
93 92 com3r R Po A S Po B t A × B u A × B v A × B ¬ t T t t T u u T v t T v
94 93 imp R Po A S Po B t A × B u A × B v A × B ¬ t T t t T u u T v t T v
95 94 ralrimiv R Po A S Po B t A × B u A × B v A × B ¬ t T t t T u u T v t T v
96 95 ralrimivva R Po A S Po B t A × B u A × B v A × B ¬ t T t t T u u T v t T v
97 df-po T Po A × B t A × B u A × B v A × B ¬ t T t t T u u T v t T v
98 96 97 sylibr R Po A S Po B T Po A × B