xporderlem

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

		Ref	Expression
	Hypothesis	xporderlem.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))))\}$
	Assertion	xporderlem	$⊢ ⟨a, b⟩ T ⟨c, d⟩ \leftrightarrow (((a \in A \land c \in A) \land (b \in B \land d \in B)) \land (a R c \lor (a = c \land b S d)))$

Proof

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

Metamath Proof Explorer

Theorem xporderlem

Proof