xpord3lem

Description: Lemma for triple ordering. Calculate the value of the relationship. (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		opex	$⊢ ⟨⟨a, b⟩, c⟩ \in V$
3		opex	$⊢ ⟨⟨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		vex	$⊢ a \in V$
6		vex	$⊢ b \in V$
7		vex	$⊢ c \in V$
8	5 6 7	ot21std	$⊢ x = ⟨⟨a, b⟩, c⟩ \to 1^{st} (1^{st} (x)) = a$
9	8	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)))$
10	8	eqeq1d	$⊢ x = ⟨⟨a, b⟩, c⟩ \to (1^{st} (1^{st} (x)) = 1^{st} (1^{st} (y)) \leftrightarrow a = 1^{st} (1^{st} (y)))$
11	9 10	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))))$
12	5 6 7	ot22ndd	$⊢ x = ⟨⟨a, b⟩, c⟩ \to 2^{nd} (1^{st} (x)) = b$
13	12	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)))$
14	12	eqeq1d	$⊢ x = ⟨⟨a, b⟩, c⟩ \to (2^{nd} (1^{st} (x)) = 2^{nd} (1^{st} (y)) \leftrightarrow b = 2^{nd} (1^{st} (y)))$
15	13 14	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))))$
16		opex	$⊢ ⟨a, b⟩ \in V$
17	16 7	op2ndd	$⊢ x = ⟨⟨a, b⟩, c⟩ \to 2^{nd} (x) = c$
18	17	breq1d	$⊢ x = ⟨⟨a, b⟩, c⟩ \to (2^{nd} (x) T 2^{nd} (y) \leftrightarrow c T 2^{nd} (y))$
19	17	eqeq1d	$⊢ x = ⟨⟨a, b⟩, c⟩ \to (2^{nd} (x) = 2^{nd} (y) \leftrightarrow c = 2^{nd} (y))$
20	18 19	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)))$
21	11 15 20	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))))$
22		neeq1	$⊢ x = ⟨⟨a, b⟩, c⟩ \to (x \neq y \leftrightarrow ⟨⟨a, b⟩, c⟩ \neq y)$
23	21 22	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))$
24	4 23	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)))$
25		eleq1	$⊢ y = ⟨⟨d, e⟩, f⟩ \to (y \in ((A \times B) \times C) \leftrightarrow ⟨⟨d, e⟩, f⟩ \in ((A \times B) \times C))$
26		vex	$⊢ d \in V$
27		vex	$⊢ e \in V$
28		vex	$⊢ f \in V$
29	26 27 28	ot21std	$⊢ y = ⟨⟨d, e⟩, f⟩ \to 1^{st} (1^{st} (y)) = d$
30	29	breq2d	$⊢ y = ⟨⟨d, e⟩, f⟩ \to (a R 1^{st} (1^{st} (y)) \leftrightarrow a R d)$
31	29	eqeq2d	$⊢ y = ⟨⟨d, e⟩, f⟩ \to (a = 1^{st} (1^{st} (y)) \leftrightarrow a = d)$
32	30 31	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))$
33	26 27 28	ot22ndd	$⊢ y = ⟨⟨d, e⟩, f⟩ \to 2^{nd} (1^{st} (y)) = e$
34	33	breq2d	$⊢ y = ⟨⟨d, e⟩, f⟩ \to (b S 2^{nd} (1^{st} (y)) \leftrightarrow b S e)$
35	33	eqeq2d	$⊢ y = ⟨⟨d, e⟩, f⟩ \to (b = 2^{nd} (1^{st} (y)) \leftrightarrow b = e)$
36	34 35	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))$
37		opex	$⊢ ⟨d, e⟩ \in V$
38	37 28	op2ndd	$⊢ y = ⟨⟨d, e⟩, f⟩ \to 2^{nd} (y) = f$
39	38	breq2d	$⊢ y = ⟨⟨d, e⟩, f⟩ \to (c T 2^{nd} (y) \leftrightarrow c T f)$
40	38	eqeq2d	$⊢ y = ⟨⟨d, e⟩, f⟩ \to (c = 2^{nd} (y) \leftrightarrow c = f)$
41	39 40	orbi12d	$⊢ y = ⟨⟨d, e⟩, f⟩ \to ((c T 2^{nd} (y) \lor c = 2^{nd} (y)) \leftrightarrow (c T f \lor c = f))$
42	32 36 41	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)))$
43		neeq2	$⊢ y = ⟨⟨d, e⟩, f⟩ \to (⟨⟨a, b⟩, c⟩ \neq y \leftrightarrow ⟨⟨a, b⟩, c⟩ \neq ⟨⟨d, e⟩, f⟩)$
44	42 43	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⟩))$
45	25 44	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⟩)))$
46	2 3 24 45 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⟩))$
47		ot2elxp	$⊢ ⟨⟨a, b⟩, c⟩ \in ((A \times B) \times C) \leftrightarrow (a \in A \land b \in B \land c \in C)$
48		ot2elxp	$⊢ ⟨⟨d, e⟩, f⟩ \in ((A \times B) \times C) \leftrightarrow (d \in A \land e \in B \land f \in C)$
49	5 6 7	otthne	$⊢ ⟨⟨a, b⟩, c⟩ \neq ⟨⟨d, e⟩, f⟩ \leftrightarrow (a \neq d \lor b \neq e \lor c \neq f)$
50	49	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))$
51	47 48 50	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)))$
52	46 51	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