Metamath Proof Explorer


Theorem xpord3lem

Description: Lemma for triple ordering. Calculate the value of the relation. (Contributed by Scott Fenton, 21-Aug-2024)

Ref Expression
Hypothesis xpord3.1 U = x y | x A × B × C y A × B × C 1 st 1 st x R 1 st 1 st y 1 st 1 st x = 1 st 1 st y 2 nd 1 st x S 2 nd 1 st y 2 nd 1 st x = 2 nd 1 st y 2 nd x T 2 nd y 2 nd x = 2 nd y x y
Assertion xpord3lem a b c U d e f a A b B c C d A e B f C a R d a = d b S e b = e c T f c = f a d b e c f

Proof

Step Hyp Ref Expression
1 xpord3.1 U = x y | x A × B × C y A × B × C 1 st 1 st x R 1 st 1 st y 1 st 1 st x = 1 st 1 st y 2 nd 1 st x S 2 nd 1 st y 2 nd 1 st x = 2 nd 1 st y 2 nd x T 2 nd y 2 nd x = 2 nd y x y
2 otex a b c V
3 otex d e f V
4 eleq1 x = a b c x A × B × C a b c A × B × C
5 2fveq3 x = a b c 1 st 1 st x = 1 st 1 st a b c
6 vex a V
7 vex b V
8 vex c V
9 ot1stg a V b V c V 1 st 1 st a b c = a
10 6 7 8 9 mp3an 1 st 1 st a b c = a
11 5 10 eqtrdi x = a b c 1 st 1 st x = a
12 11 breq1d x = a b c 1 st 1 st x R 1 st 1 st y a R 1 st 1 st y
13 11 eqeq1d x = a b c 1 st 1 st x = 1 st 1 st y a = 1 st 1 st y
14 12 13 orbi12d x = a b c 1 st 1 st x R 1 st 1 st y 1 st 1 st x = 1 st 1 st y a R 1 st 1 st y a = 1 st 1 st y
15 2fveq3 x = a b c 2 nd 1 st x = 2 nd 1 st a b c
16 ot2ndg a V b V c V 2 nd 1 st a b c = b
17 6 7 8 16 mp3an 2 nd 1 st a b c = b
18 15 17 eqtrdi x = a b c 2 nd 1 st x = b
19 18 breq1d x = a b c 2 nd 1 st x S 2 nd 1 st y b S 2 nd 1 st y
20 18 eqeq1d x = a b c 2 nd 1 st x = 2 nd 1 st y b = 2 nd 1 st y
21 19 20 orbi12d x = a b c 2 nd 1 st x S 2 nd 1 st y 2 nd 1 st x = 2 nd 1 st y b S 2 nd 1 st y b = 2 nd 1 st y
22 fveq2 x = a b c 2 nd x = 2 nd a b c
23 ot3rdg c V 2 nd a b c = c
24 23 elv 2 nd a b c = c
25 22 24 eqtrdi x = a b c 2 nd x = c
26 25 breq1d x = a b c 2 nd x T 2 nd y c T 2 nd y
27 25 eqeq1d x = a b c 2 nd x = 2 nd y c = 2 nd y
28 26 27 orbi12d x = a b c 2 nd x T 2 nd y 2 nd x = 2 nd y c T 2 nd y c = 2 nd y
29 14 21 28 3anbi123d x = a b c 1 st 1 st x R 1 st 1 st y 1 st 1 st x = 1 st 1 st y 2 nd 1 st x S 2 nd 1 st y 2 nd 1 st x = 2 nd 1 st y 2 nd x T 2 nd y 2 nd x = 2 nd y a R 1 st 1 st y a = 1 st 1 st y b S 2 nd 1 st y b = 2 nd 1 st y c T 2 nd y c = 2 nd y
30 neeq1 x = a b c x y a b c y
31 29 30 anbi12d x = a b c 1 st 1 st x R 1 st 1 st y 1 st 1 st x = 1 st 1 st y 2 nd 1 st x S 2 nd 1 st y 2 nd 1 st x = 2 nd 1 st y 2 nd x T 2 nd y 2 nd x = 2 nd y x y a R 1 st 1 st y a = 1 st 1 st y b S 2 nd 1 st y b = 2 nd 1 st y c T 2 nd y c = 2 nd y a b c y
32 4 31 3anbi13d x = a b c x A × B × C y A × B × C 1 st 1 st x R 1 st 1 st y 1 st 1 st x = 1 st 1 st y 2 nd 1 st x S 2 nd 1 st y 2 nd 1 st x = 2 nd 1 st y 2 nd x T 2 nd y 2 nd x = 2 nd y x y a b c A × B × C y A × B × C a R 1 st 1 st y a = 1 st 1 st y b S 2 nd 1 st y b = 2 nd 1 st y c T 2 nd y c = 2 nd y a b c y
33 eleq1 y = d e f y A × B × C d e f A × B × C
34 2fveq3 y = d e f 1 st 1 st y = 1 st 1 st d e f
35 vex d V
36 vex e V
37 vex f V
38 ot1stg d V e V f V 1 st 1 st d e f = d
39 35 36 37 38 mp3an 1 st 1 st d e f = d
40 34 39 eqtrdi y = d e f 1 st 1 st y = d
41 40 breq2d y = d e f a R 1 st 1 st y a R d
42 40 eqeq2d y = d e f a = 1 st 1 st y a = d
43 41 42 orbi12d y = d e f a R 1 st 1 st y a = 1 st 1 st y a R d a = d
44 2fveq3 y = d e f 2 nd 1 st y = 2 nd 1 st d e f
45 ot2ndg d V e V f V 2 nd 1 st d e f = e
46 35 36 37 45 mp3an 2 nd 1 st d e f = e
47 44 46 eqtrdi y = d e f 2 nd 1 st y = e
48 47 breq2d y = d e f b S 2 nd 1 st y b S e
49 47 eqeq2d y = d e f b = 2 nd 1 st y b = e
50 48 49 orbi12d y = d e f b S 2 nd 1 st y b = 2 nd 1 st y b S e b = e
51 fveq2 y = d e f 2 nd y = 2 nd d e f
52 ot3rdg f V 2 nd d e f = f
53 52 elv 2 nd d e f = f
54 51 53 eqtrdi y = d e f 2 nd y = f
55 54 breq2d y = d e f c T 2 nd y c T f
56 54 eqeq2d y = d e f c = 2 nd y c = f
57 55 56 orbi12d y = d e f c T 2 nd y c = 2 nd y c T f c = f
58 43 50 57 3anbi123d y = d e f a R 1 st 1 st y a = 1 st 1 st y b S 2 nd 1 st y b = 2 nd 1 st y c T 2 nd y c = 2 nd y a R d a = d b S e b = e c T f c = f
59 neeq2 y = d e f a b c y a b c d e f
60 58 59 anbi12d y = d e f a R 1 st 1 st y a = 1 st 1 st y b S 2 nd 1 st y b = 2 nd 1 st y c T 2 nd y c = 2 nd y a b c y a R d a = d b S e b = e c T f c = f a b c d e f
61 33 60 3anbi23d y = d e f a b c A × B × C y A × B × C a R 1 st 1 st y a = 1 st 1 st y b S 2 nd 1 st y b = 2 nd 1 st y c T 2 nd y c = 2 nd y a b c y a b c A × B × C d e f A × B × C a R d a = d b S e b = e c T f c = f a b c d e f
62 2 3 32 61 1 brab a b c U d e f a b c A × B × C d e f A × B × C a R d a = d b S e b = e c T f c = f a b c d e f
63 otelxp a b c A × B × C a A b B c C
64 otelxp d e f A × B × C d A e B f C
65 6 7 8 otthne a b c d e f a d b e c f
66 65 anbi2i a R d a = d b S e b = e c T f c = f a b c d e f a R d a = d b S e b = e c T f c = f a d b e c f
67 63 64 66 3anbi123i a b c A × B × C d e f A × B × C a R d a = d b S e b = e c T f c = f a b c d e f a A b B c C d A e B f C a R d a = d b S e b = e c T f c = f a d b e c f
68 62 67 bitri a b c U d e f a A b B c C d A e B f C a R d a = d b S e b = e c T f c = f a d b e c f