sexp3

Description: Show that the triple order is set-like. (Contributed by Scott Fenton, 21-Aug-2024)

	Ref	Expression
Hypotheses	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))\}$
	sexp3.1	$⊢ φ \to R Se A$
	sexp3.2	$⊢ φ \to S Se B$
	sexp3.3	$⊢ φ \to T Se C$
Assertion	sexp3	$⊢ φ \to U Se ((A \times B) \times C)$

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		sexp3.1	$⊢ φ \to R Se A$
3		sexp3.2	$⊢ φ \to S Se B$
4		sexp3.3	$⊢ φ \to T Se C$
5		elxpxp	$⊢ p \in ((A \times B) \times C) \leftrightarrow \exists a \in A \exists b \in B \exists c \in C p = ⟨⟨a, b⟩, c⟩$
6		df-3an	$⊢ (a \in A \land b \in B \land c \in C) \leftrightarrow ((a \in A \land b \in B) \land c \in C)$
7	1	xpord3pred	$⊢ (a \in A \land b \in B \land c \in C) \to Pred (U, ((A \times B) \times C), ⟨⟨a, b⟩, c⟩) = (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨⟨a, b⟩, c⟩\}$
8	7	adantl	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to Pred (U, ((A \times B) \times C), ⟨⟨a, b⟩, c⟩) = (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨⟨a, b⟩, c⟩\}$
9		simpr1	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to a \in A$
10	2	adantr	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to R Se A$
11		setlikespec	$⊢ (a \in A \land R Se A) \to Pred (R, A, a) \in V$
12	9 10 11	syl2anc	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to Pred (R, A, a) \in V$
13		snex	$⊢ \{a\} \in V$
14	13	a1i	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to \{a\} \in V$
15	12 14	unexd	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to Pred (R, A, a) \cup \{a\} \in V$
16		simpr2	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to b \in B$
17	3	adantr	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to S Se B$
18		setlikespec	$⊢ (b \in B \land S Se B) \to Pred (S, B, b) \in V$
19	16 17 18	syl2anc	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to Pred (S, B, b) \in V$
20		snex	$⊢ \{b\} \in V$
21	20	a1i	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to \{b\} \in V$
22	19 21	unexd	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to Pred (S, B, b) \cup \{b\} \in V$
23	15 22	xpexd	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to (Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\}) \in V$
24		simpr3	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to c \in C$
25	4	adantr	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to T Se C$
26		setlikespec	$⊢ (c \in C \land T Se C) \to Pred (T, C, c) \in V$
27	24 25 26	syl2anc	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to Pred (T, C, c) \in V$
28		snex	$⊢ \{c\} \in V$
29	28	a1i	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to \{c\} \in V$
30	27 29	unexd	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to Pred (T, C, c) \cup \{c\} \in V$
31	23 30	xpexd	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\}) \in V$
32	31	difexd	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨⟨a, b⟩, c⟩\} \in V$
33	8 32	eqeltrd	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to Pred (U, ((A \times B) \times C), ⟨⟨a, b⟩, c⟩) \in V$
34		predeq3	$⊢ p = ⟨⟨a, b⟩, c⟩ \to Pred (U, ((A \times B) \times C), p) = Pred (U, ((A \times B) \times C), ⟨⟨a, b⟩, c⟩)$
35	34	eleq1d	$⊢ p = ⟨⟨a, b⟩, c⟩ \to (Pred (U, ((A \times B) \times C), p) \in V \leftrightarrow Pred (U, ((A \times B) \times C), ⟨⟨a, b⟩, c⟩) \in V)$
36	35	biimprd	$⊢ p = ⟨⟨a, b⟩, c⟩ \to (Pred (U, ((A \times B) \times C), ⟨⟨a, b⟩, c⟩) \in V \to Pred (U, ((A \times B) \times C), p) \in V)$
37	36	com12	$⊢ Pred (U, ((A \times B) \times C), ⟨⟨a, b⟩, c⟩) \in V \to (p = ⟨⟨a, b⟩, c⟩ \to Pred (U, ((A \times B) \times C), p) \in V)$
38	33 37	syl	$⊢ (φ \land (a \in A \land b \in B \land c \in C)) \to (p = ⟨⟨a, b⟩, c⟩ \to Pred (U, ((A \times B) \times C), p) \in V)$
39	6 38	sylan2br	$⊢ (φ \land ((a \in A \land b \in B) \land c \in C)) \to (p = ⟨⟨a, b⟩, c⟩ \to Pred (U, ((A \times B) \times C), p) \in V)$
40	39	anassrs	$⊢ ((φ \land (a \in A \land b \in B)) \land c \in C) \to (p = ⟨⟨a, b⟩, c⟩ \to Pred (U, ((A \times B) \times C), p) \in V)$
41	40	rexlimdva	$⊢ (φ \land (a \in A \land b \in B)) \to (\exists c \in C p = ⟨⟨a, b⟩, c⟩ \to Pred (U, ((A \times B) \times C), p) \in V)$
42	41	rexlimdvva	$⊢ φ \to (\exists a \in A \exists b \in B \exists c \in C p = ⟨⟨a, b⟩, c⟩ \to Pred (U, ((A \times B) \times C), p) \in V)$
43	5 42	syl5bi	$⊢ φ \to (p \in ((A \times B) \times C) \to Pred (U, ((A \times B) \times C), p) \in V)$
44	43	ralrimiv	$⊢ φ \to \forall p \in ((A \times B) \times C) Pred (U, ((A \times B) \times C), p) \in V$
45		dfse3	$⊢ U Se ((A \times B) \times C) \leftrightarrow \forall p \in ((A \times B) \times C) Pred (U, ((A \times B) \times C), p) \in V$
46	44 45	sylibr	$⊢ φ \to U Se ((A \times B) \times C)$

Metamath Proof Explorer

Theorem sexp3

Proof