Metamath Proof Explorer


Theorem xporderlem

Description: Lemma for lexicographical ordering theorems. (Contributed by Scott Fenton, 16-Mar-2011)

Ref Expression
Hypothesis xporderlem.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 xporderlem a b T c d a A c A b B d B a R c a = c b S d

Proof

Step Hyp Ref Expression
1 xporderlem.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 df-br a b T c d a b c d T
3 1 eleq2i a b c d T a b c d 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
4 2 3 bitri a b T c d a b c d 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
5 opex a b V
6 opex c d V
7 eleq1 x = a b x A × B a b A × B
8 opelxp a b A × B a A b B
9 7 8 bitrdi x = a b x A × B a A b B
10 9 anbi1d x = a b x A × B y A × B a A b B y A × B
11 vex a V
12 vex b V
13 11 12 op1std x = a b 1 st x = a
14 13 breq1d x = a b 1 st x R 1 st y a R 1 st y
15 13 eqeq1d x = a b 1 st x = 1 st y a = 1 st y
16 11 12 op2ndd x = a b 2 nd x = b
17 16 breq1d x = a b 2 nd x S 2 nd y b S 2 nd y
18 15 17 anbi12d x = a b 1 st x = 1 st y 2 nd x S 2 nd y a = 1 st y b S 2 nd y
19 14 18 orbi12d x = a b 1 st x R 1 st y 1 st x = 1 st y 2 nd x S 2 nd y a R 1 st y a = 1 st y b S 2 nd y
20 10 19 anbi12d x = a b 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 a A b B y A × B a R 1 st y a = 1 st y b S 2 nd y
21 eleq1 y = c d y A × B c d A × B
22 opelxp c d A × B c A d B
23 21 22 bitrdi y = c d y A × B c A d B
24 23 anbi2d y = c d a A b B y A × B a A b B c A d B
25 vex c V
26 vex d V
27 25 26 op1std y = c d 1 st y = c
28 27 breq2d y = c d a R 1 st y a R c
29 27 eqeq2d y = c d a = 1 st y a = c
30 25 26 op2ndd y = c d 2 nd y = d
31 30 breq2d y = c d b S 2 nd y b S d
32 29 31 anbi12d y = c d a = 1 st y b S 2 nd y a = c b S d
33 28 32 orbi12d y = c d a R 1 st y a = 1 st y b S 2 nd y a R c a = c b S d
34 24 33 anbi12d y = c d a A b B y A × B a R 1 st y a = 1 st y b S 2 nd y a A b B c A d B a R c a = c b S d
35 5 6 20 34 opelopab a b c d 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 a A b B c A d B a R c a = c b S d
36 an4 a A b B c A d B a A c A b B d B
37 36 anbi1i a A b B c A d B a R c a = c b S d a A c A b B d B a R c a = c b S d
38 4 35 37 3bitri a b T c d a A c A b B d B a R c a = c b S d