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 \in ((A \times B) \times C) \land y \in ((A \times B) \times C) \land (((1^{st} (1^{st} (x)) R 1^{st} (1^{st} (y)) \lor 1^{st} (1^{st} (x)) = 1^{st} (1^{st} (y))) \land (2^{nd} (1^{st} (x)) S 2^{nd} (1^{st} (y)) \lor 2^{nd} (1^{st} (x)) = 2^{nd} (1^{st} (y))) \land (2^{nd} (x) T 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y))) \land x \neq y))\}$
	Assertion	xpord3lem	$⊢ ⟨a, b, c⟩ U ⟨d, e, f⟩ \leftrightarrow ((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C) \land (((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)))$

Proof

Step	Hyp	Ref	Expression
1		xpord3.1	$⊢ U = \{⟨x, y⟩ \| (x \in ((A \times B) \times C) \land y \in ((A \times B) \times C) \land (((1^{st} (1^{st} (x)) R 1^{st} (1^{st} (y)) \lor 1^{st} (1^{st} (x)) = 1^{st} (1^{st} (y))) \land (2^{nd} (1^{st} (x)) S 2^{nd} (1^{st} (y)) \lor 2^{nd} (1^{st} (x)) = 2^{nd} (1^{st} (y))) \land (2^{nd} (x) T 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y))) \land x \neq y))\}$
2		otex	$⊢ ⟨a, b, c⟩ \in V$
3		otex	$⊢ ⟨d, e, f⟩ \in V$
4		eleq1	$⊢ x = ⟨a, b, c⟩ \to (x \in ((A \times B) \times C) \leftrightarrow ⟨a, b, c⟩ \in ((A \times B) \times C))$
5		2fveq3	$⊢ x = ⟨a, b, c⟩ \to 1^{st} (1^{st} (x)) = 1^{st} (1^{st} (⟨a, b, c⟩))$
6		vex	$⊢ a \in V$
7		vex	$⊢ b \in V$
8		vex	$⊢ c \in V$
9		ot1stg	$⊢ (a \in V \land b \in V \land c \in V) \to 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⟩ \to 1^{st} (1^{st} (x)) = a$
12	11	breq1d	$⊢ x = ⟨a, b, c⟩ \to (1^{st} (1^{st} (x)) R 1^{st} (1^{st} (y)) \leftrightarrow a R 1^{st} (1^{st} (y)))$
13	11	eqeq1d	$⊢ x = ⟨a, b, c⟩ \to (1^{st} (1^{st} (x)) = 1^{st} (1^{st} (y)) \leftrightarrow a = 1^{st} (1^{st} (y)))$
14	12 13	orbi12d	$⊢ x = ⟨a, b, c⟩ \to ((1^{st} (1^{st} (x)) R 1^{st} (1^{st} (y)) \lor 1^{st} (1^{st} (x)) = 1^{st} (1^{st} (y))) \leftrightarrow (a R 1^{st} (1^{st} (y)) \lor a = 1^{st} (1^{st} (y))))$
15		2fveq3	$⊢ x = ⟨a, b, c⟩ \to 2^{nd} (1^{st} (x)) = 2^{nd} (1^{st} (⟨a, b, c⟩))$
16		ot2ndg	$⊢ (a \in V \land b \in V \land c \in V) \to 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⟩ \to 2^{nd} (1^{st} (x)) = b$
19	18	breq1d	$⊢ x = ⟨a, b, c⟩ \to (2^{nd} (1^{st} (x)) S 2^{nd} (1^{st} (y)) \leftrightarrow b S 2^{nd} (1^{st} (y)))$
20	18	eqeq1d	$⊢ x = ⟨a, b, c⟩ \to (2^{nd} (1^{st} (x)) = 2^{nd} (1^{st} (y)) \leftrightarrow b = 2^{nd} (1^{st} (y)))$
21	19 20	orbi12d	$⊢ x = ⟨a, b, c⟩ \to ((2^{nd} (1^{st} (x)) S 2^{nd} (1^{st} (y)) \lor 2^{nd} (1^{st} (x)) = 2^{nd} (1^{st} (y))) \leftrightarrow (b S 2^{nd} (1^{st} (y)) \lor b = 2^{nd} (1^{st} (y))))$
22		fveq2	$⊢ x = ⟨a, b, c⟩ \to 2^{nd} (x) = 2^{nd} (⟨a, b, c⟩)$
23		ot3rdg	$⊢ c \in V \to 2^{nd} (⟨a, b, c⟩) = c$
24	23	elv	$⊢ 2^{nd} (⟨a, b, c⟩) = c$
25	22 24	eqtrdi	$⊢ x = ⟨a, b, c⟩ \to 2^{nd} (x) = c$
26	25	breq1d	$⊢ x = ⟨a, b, c⟩ \to (2^{nd} (x) T 2^{nd} (y) \leftrightarrow c T 2^{nd} (y))$
27	25	eqeq1d	$⊢ x = ⟨a, b, c⟩ \to (2^{nd} (x) = 2^{nd} (y) \leftrightarrow c = 2^{nd} (y))$
28	26 27	orbi12d	$⊢ x = ⟨a, b, c⟩ \to ((2^{nd} (x) T 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \leftrightarrow (c T 2^{nd} (y) \lor c = 2^{nd} (y)))$
29	14 21 28	3anbi123d	$⊢ x = ⟨a, b, c⟩ \to (((1^{st} (1^{st} (x)) R 1^{st} (1^{st} (y)) \lor 1^{st} (1^{st} (x)) = 1^{st} (1^{st} (y))) \land (2^{nd} (1^{st} (x)) S 2^{nd} (1^{st} (y)) \lor 2^{nd} (1^{st} (x)) = 2^{nd} (1^{st} (y))) \land (2^{nd} (x) T 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y))) \leftrightarrow ((a R 1^{st} (1^{st} (y)) \lor a = 1^{st} (1^{st} (y))) \land (b S 2^{nd} (1^{st} (y)) \lor b = 2^{nd} (1^{st} (y))) \land (c T 2^{nd} (y) \lor c = 2^{nd} (y))))$
30		neeq1	$⊢ x = ⟨a, b, c⟩ \to (x \neq y \leftrightarrow ⟨a, b, c⟩ \neq y)$
31	29 30	anbi12d	$⊢ x = ⟨a, b, c⟩ \to ((((1^{st} (1^{st} (x)) R 1^{st} (1^{st} (y)) \lor 1^{st} (1^{st} (x)) = 1^{st} (1^{st} (y))) \land (2^{nd} (1^{st} (x)) S 2^{nd} (1^{st} (y)) \lor 2^{nd} (1^{st} (x)) = 2^{nd} (1^{st} (y))) \land (2^{nd} (x) T 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y))) \land x \neq y) \leftrightarrow (((a R 1^{st} (1^{st} (y)) \lor a = 1^{st} (1^{st} (y))) \land (b S 2^{nd} (1^{st} (y)) \lor b = 2^{nd} (1^{st} (y))) \land (c T 2^{nd} (y) \lor c = 2^{nd} (y))) \land ⟨a, b, c⟩ \neq y))$
32	4 31	3anbi13d	$⊢ x = ⟨a, b, c⟩ \to ((x \in ((A \times B) \times C) \land y \in ((A \times B) \times C) \land (((1^{st} (1^{st} (x)) R 1^{st} (1^{st} (y)) \lor 1^{st} (1^{st} (x)) = 1^{st} (1^{st} (y))) \land (2^{nd} (1^{st} (x)) S 2^{nd} (1^{st} (y)) \lor 2^{nd} (1^{st} (x)) = 2^{nd} (1^{st} (y))) \land (2^{nd} (x) T 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y))) \land x \neq y)) \leftrightarrow (⟨a, b, c⟩ \in ((A \times B) \times C) \land y \in ((A \times B) \times C) \land (((a R 1^{st} (1^{st} (y)) \lor a = 1^{st} (1^{st} (y))) \land (b S 2^{nd} (1^{st} (y)) \lor b = 2^{nd} (1^{st} (y))) \land (c T 2^{nd} (y) \lor c = 2^{nd} (y))) \land ⟨a, b, c⟩ \neq y)))$
33		eleq1	$⊢ y = ⟨d, e, f⟩ \to (y \in ((A \times B) \times C) \leftrightarrow ⟨d, e, f⟩ \in ((A \times B) \times C))$
34		2fveq3	$⊢ y = ⟨d, e, f⟩ \to 1^{st} (1^{st} (y)) = 1^{st} (1^{st} (⟨d, e, f⟩))$
35		vex	$⊢ d \in V$
36		vex	$⊢ e \in V$
37		vex	$⊢ f \in V$
38		ot1stg	$⊢ (d \in V \land e \in V \land f \in V) \to 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⟩ \to 1^{st} (1^{st} (y)) = d$
41	40	breq2d	$⊢ y = ⟨d, e, f⟩ \to (a R 1^{st} (1^{st} (y)) \leftrightarrow a R d)$
42	40	eqeq2d	$⊢ y = ⟨d, e, f⟩ \to (a = 1^{st} (1^{st} (y)) \leftrightarrow a = d)$
43	41 42	orbi12d	$⊢ y = ⟨d, e, f⟩ \to ((a R 1^{st} (1^{st} (y)) \lor a = 1^{st} (1^{st} (y))) \leftrightarrow (a R d \lor a = d))$
44		2fveq3	$⊢ y = ⟨d, e, f⟩ \to 2^{nd} (1^{st} (y)) = 2^{nd} (1^{st} (⟨d, e, f⟩))$
45		ot2ndg	$⊢ (d \in V \land e \in V \land f \in V) \to 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⟩ \to 2^{nd} (1^{st} (y)) = e$
48	47	breq2d	$⊢ y = ⟨d, e, f⟩ \to (b S 2^{nd} (1^{st} (y)) \leftrightarrow b S e)$
49	47	eqeq2d	$⊢ y = ⟨d, e, f⟩ \to (b = 2^{nd} (1^{st} (y)) \leftrightarrow b = e)$
50	48 49	orbi12d	$⊢ y = ⟨d, e, f⟩ \to ((b S 2^{nd} (1^{st} (y)) \lor b = 2^{nd} (1^{st} (y))) \leftrightarrow (b S e \lor b = e))$
51		fveq2	$⊢ y = ⟨d, e, f⟩ \to 2^{nd} (y) = 2^{nd} (⟨d, e, f⟩)$
52		ot3rdg	$⊢ f \in V \to 2^{nd} (⟨d, e, f⟩) = f$
53	52	elv	$⊢ 2^{nd} (⟨d, e, f⟩) = f$
54	51 53	eqtrdi	$⊢ y = ⟨d, e, f⟩ \to 2^{nd} (y) = f$
55	54	breq2d	$⊢ y = ⟨d, e, f⟩ \to (c T 2^{nd} (y) \leftrightarrow c T f)$
56	54	eqeq2d	$⊢ y = ⟨d, e, f⟩ \to (c = 2^{nd} (y) \leftrightarrow c = f)$
57	55 56	orbi12d	$⊢ y = ⟨d, e, f⟩ \to ((c T 2^{nd} (y) \lor c = 2^{nd} (y)) \leftrightarrow (c T f \lor c = f))$
58	43 50 57	3anbi123d	$⊢ y = ⟨d, e, f⟩ \to (((a R 1^{st} (1^{st} (y)) \lor a = 1^{st} (1^{st} (y))) \land (b S 2^{nd} (1^{st} (y)) \lor b = 2^{nd} (1^{st} (y))) \land (c T 2^{nd} (y) \lor c = 2^{nd} (y))) \leftrightarrow ((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)))$
59		neeq2	$⊢ y = ⟨d, e, f⟩ \to (⟨a, b, c⟩ \neq y \leftrightarrow ⟨a, b, c⟩ \neq ⟨d, e, f⟩)$
60	58 59	anbi12d	$⊢ y = ⟨d, e, f⟩ \to ((((a R 1^{st} (1^{st} (y)) \lor a = 1^{st} (1^{st} (y))) \land (b S 2^{nd} (1^{st} (y)) \lor b = 2^{nd} (1^{st} (y))) \land (c T 2^{nd} (y) \lor c = 2^{nd} (y))) \land ⟨a, b, c⟩ \neq y) \leftrightarrow (((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land ⟨a, b, c⟩ \neq ⟨d, e, f⟩))$
61	33 60	3anbi23d	$⊢ y = ⟨d, e, f⟩ \to ((⟨a, b, c⟩ \in ((A \times B) \times C) \land y \in ((A \times B) \times C) \land (((a R 1^{st} (1^{st} (y)) \lor a = 1^{st} (1^{st} (y))) \land (b S 2^{nd} (1^{st} (y)) \lor b = 2^{nd} (1^{st} (y))) \land (c T 2^{nd} (y) \lor c = 2^{nd} (y))) \land ⟨a, b, c⟩ \neq y)) \leftrightarrow (⟨a, b, c⟩ \in ((A \times B) \times C) \land ⟨d, e, f⟩ \in ((A \times B) \times C) \land (((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land ⟨a, b, c⟩ \neq ⟨d, e, f⟩)))$
62	2 3 32 61 1	brab	$⊢ ⟨a, b, c⟩ U ⟨d, e, f⟩ \leftrightarrow (⟨a, b, c⟩ \in ((A \times B) \times C) \land ⟨d, e, f⟩ \in ((A \times B) \times C) \land (((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land ⟨a, b, c⟩ \neq ⟨d, e, f⟩))$
63		otelxp	$⊢ ⟨a, b, c⟩ \in ((A \times B) \times C) \leftrightarrow (a \in A \land b \in B \land c \in C)$
64		otelxp	$⊢ ⟨d, e, f⟩ \in ((A \times B) \times C) \leftrightarrow (d \in A \land e \in B \land f \in C)$
65	6 7 8	otthne	$⊢ ⟨a, b, c⟩ \neq ⟨d, e, f⟩ \leftrightarrow (a \neq d \lor b \neq e \lor c \neq f)$
66	65	anbi2i	$⊢ (((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land ⟨a, b, c⟩ \neq ⟨d, e, f⟩) \leftrightarrow (((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f))$
67	63 64 66	3anbi123i	$⊢ (⟨a, b, c⟩ \in ((A \times B) \times C) \land ⟨d, e, f⟩ \in ((A \times B) \times C) \land (((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land ⟨a, b, c⟩ \neq ⟨d, e, f⟩)) \leftrightarrow ((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C) \land (((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)))$
68	62 67	bitri	$⊢ ⟨a, b, c⟩ U ⟨d, e, f⟩ \leftrightarrow ((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B \land f \in C) \land (((a R d \lor a = d) \land (b S e \lor b = e) \land (c T f \lor c = f)) \land (a \neq d \lor b \neq e \lor c \neq f)))$

Metamath Proof Explorer

Theorem xpord3lem

Proof