xpord2lem

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

		Ref	Expression
	Hypothesis	xpord2.1	$⊢ T = \{⟨x, y⟩ \| (x \in (A \times B) \land y \in (A \times B) \land ((1^{st} (x) R 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) S 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}$
	Assertion	xpord2lem	$⊢ ⟨a, b⟩ T ⟨c, d⟩ \leftrightarrow ((a \in A \land b \in B) \land (c \in A \land d \in B) \land ((a R c \lor a = c) \land (b S d \lor b = d) \land (a \neq c \lor b \neq d)))$

Proof

Step	Hyp	Ref	Expression
1		xpord2.1	$⊢ T = \{⟨x, y⟩ \| (x \in (A \times B) \land y \in (A \times B) \land ((1^{st} (x) R 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) S 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}$
2		opex	$⊢ ⟨a, b⟩ \in V$
3		opex	$⊢ ⟨c, d⟩ \in V$
4		eleq1	$⊢ x = ⟨a, b⟩ \to (x \in (A \times B) \leftrightarrow ⟨a, b⟩ \in (A \times B))$
5		opelxp	$⊢ ⟨a, b⟩ \in (A \times B) \leftrightarrow (a \in A \land b \in B)$
6	4 5	bitrdi	$⊢ x = ⟨a, b⟩ \to (x \in (A \times B) \leftrightarrow (a \in A \land b \in B))$
7		vex	$⊢ a \in V$
8		vex	$⊢ b \in V$
9	7 8	op1std	$⊢ x = ⟨a, b⟩ \to 1^{st} (x) = a$
10	9	breq1d	$⊢ x = ⟨a, b⟩ \to (1^{st} (x) R 1^{st} (y) \leftrightarrow a R 1^{st} (y))$
11	9	eqeq1d	$⊢ x = ⟨a, b⟩ \to (1^{st} (x) = 1^{st} (y) \leftrightarrow a = 1^{st} (y))$
12	10 11	orbi12d	$⊢ x = ⟨a, b⟩ \to ((1^{st} (x) R 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \leftrightarrow (a R 1^{st} (y) \lor a = 1^{st} (y)))$
13	7 8	op2ndd	$⊢ x = ⟨a, b⟩ \to 2^{nd} (x) = b$
14	13	breq1d	$⊢ x = ⟨a, b⟩ \to (2^{nd} (x) S 2^{nd} (y) \leftrightarrow b S 2^{nd} (y))$
15	13	eqeq1d	$⊢ x = ⟨a, b⟩ \to (2^{nd} (x) = 2^{nd} (y) \leftrightarrow b = 2^{nd} (y))$
16	14 15	orbi12d	$⊢ x = ⟨a, b⟩ \to ((2^{nd} (x) S 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \leftrightarrow (b S 2^{nd} (y) \lor b = 2^{nd} (y)))$
17		neeq1	$⊢ x = ⟨a, b⟩ \to (x \neq y \leftrightarrow ⟨a, b⟩ \neq y)$
18	12 16 17	3anbi123d	$⊢ x = ⟨a, b⟩ \to (((1^{st} (x) R 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) S 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y) \leftrightarrow ((a R 1^{st} (y) \lor a = 1^{st} (y)) \land (b S 2^{nd} (y) \lor b = 2^{nd} (y)) \land ⟨a, b⟩ \neq y))$
19	6 18	3anbi13d	$⊢ x = ⟨a, b⟩ \to ((x \in (A \times B) \land y \in (A \times B) \land ((1^{st} (x) R 1^{st} (y) \lor 1^{st} (x) = 1^{st} (y)) \land (2^{nd} (x) S 2^{nd} (y) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y)) \leftrightarrow ((a \in A \land b \in B) \land y \in (A \times B) \land ((a R 1^{st} (y) \lor a = 1^{st} (y)) \land (b S 2^{nd} (y) \lor b = 2^{nd} (y)) \land ⟨a, b⟩ \neq y)))$
20		eleq1	$⊢ y = ⟨c, d⟩ \to (y \in (A \times B) \leftrightarrow ⟨c, d⟩ \in (A \times B))$
21		opelxp	$⊢ ⟨c, d⟩ \in (A \times B) \leftrightarrow (c \in A \land d \in B)$
22	20 21	bitrdi	$⊢ y = ⟨c, d⟩ \to (y \in (A \times B) \leftrightarrow (c \in A \land d \in B))$
23		vex	$⊢ c \in V$
24		vex	$⊢ d \in V$
25	23 24	op1std	$⊢ y = ⟨c, d⟩ \to 1^{st} (y) = c$
26	25	breq2d	$⊢ y = ⟨c, d⟩ \to (a R 1^{st} (y) \leftrightarrow a R c)$
27	25	eqeq2d	$⊢ y = ⟨c, d⟩ \to (a = 1^{st} (y) \leftrightarrow a = c)$
28	26 27	orbi12d	$⊢ y = ⟨c, d⟩ \to ((a R 1^{st} (y) \lor a = 1^{st} (y)) \leftrightarrow (a R c \lor a = c))$
29	23 24	op2ndd	$⊢ y = ⟨c, d⟩ \to 2^{nd} (y) = d$
30	29	breq2d	$⊢ y = ⟨c, d⟩ \to (b S 2^{nd} (y) \leftrightarrow b S d)$
31	29	eqeq2d	$⊢ y = ⟨c, d⟩ \to (b = 2^{nd} (y) \leftrightarrow b = d)$
32	30 31	orbi12d	$⊢ y = ⟨c, d⟩ \to ((b S 2^{nd} (y) \lor b = 2^{nd} (y)) \leftrightarrow (b S d \lor b = d))$
33		neeq2	$⊢ y = ⟨c, d⟩ \to (⟨a, b⟩ \neq y \leftrightarrow ⟨a, b⟩ \neq ⟨c, d⟩)$
34	7 8	opthne	$⊢ ⟨a, b⟩ \neq ⟨c, d⟩ \leftrightarrow (a \neq c \lor b \neq d)$
35	33 34	bitrdi	$⊢ y = ⟨c, d⟩ \to (⟨a, b⟩ \neq y \leftrightarrow (a \neq c \lor b \neq d))$
36	28 32 35	3anbi123d	$⊢ y = ⟨c, d⟩ \to (((a R 1^{st} (y) \lor a = 1^{st} (y)) \land (b S 2^{nd} (y) \lor b = 2^{nd} (y)) \land ⟨a, b⟩ \neq y) \leftrightarrow ((a R c \lor a = c) \land (b S d \lor b = d) \land (a \neq c \lor b \neq d)))$
37	22 36	3anbi23d	$⊢ y = ⟨c, d⟩ \to (((a \in A \land b \in B) \land y \in (A \times B) \land ((a R 1^{st} (y) \lor a = 1^{st} (y)) \land (b S 2^{nd} (y) \lor b = 2^{nd} (y)) \land ⟨a, b⟩ \neq y)) \leftrightarrow ((a \in A \land b \in B) \land (c \in A \land d \in B) \land ((a R c \lor a = c) \land (b S d \lor b = d) \land (a \neq c \lor b \neq d))))$
38	2 3 19 37 1	brab	$⊢ ⟨a, b⟩ T ⟨c, d⟩ \leftrightarrow ((a \in A \land b \in B) \land (c \in A \land d \in B) \land ((a R c \lor a = c) \land (b S d \lor b = d) \land (a \neq c \lor b \neq d)))$

Metamath Proof Explorer

Theorem xpord2lem

Proof