xpord3pred

Description: Calculate the predecsessor class for the triple order. (Contributed by Scott Fenton, 31-Jan-2025)

		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	xpord3pred	$⊢ (X \in A \land Y \in B \land Z \in C) \to Pred (U, ((A \times B) \times C), ⟨X, Y, Z⟩) = (((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, Y) \cup \{Y\})) \times (Pred (T, C, Z) \cup \{Z\})) ∖ \{⟨X, Y, Z⟩\}$

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		oteq1	$⊢ a = X \to ⟨a, b, c⟩ = ⟨X, b, c⟩$
3		predeq3	$⊢ ⟨a, b, c⟩ = ⟨X, b, c⟩ \to Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) = Pred (U, ((A \times B) \times C), ⟨X, b, c⟩)$
4	2 3	syl	$⊢ a = X \to Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) = Pred (U, ((A \times B) \times C), ⟨X, b, c⟩)$
5		predeq3	$⊢ a = X \to Pred (R, A, a) = Pred (R, A, X)$
6		sneq	$⊢ a = X \to \{a\} = \{X\}$
7	5 6	uneq12d	$⊢ a = X \to Pred (R, A, a) \cup \{a\} = Pred (R, A, X) \cup \{X\}$
8	7	xpeq1d	$⊢ a = X \to (Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\}) = (Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, b) \cup \{b\})$
9	8	xpeq1d	$⊢ a = X \to ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\}) = ((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})$
10	2	sneqd	$⊢ a = X \to \{⟨a, b, c⟩\} = \{⟨X, b, c⟩\}$
11	9 10	difeq12d	$⊢ a = X \to (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\} = (((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨X, b, c⟩\}$
12	4 11	eqeq12d	$⊢ a = X \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⟩\} \leftrightarrow Pred (U, ((A \times B) \times C), ⟨X, b, c⟩) = (((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨X, b, c⟩\})$
13		oteq2	$⊢ b = Y \to ⟨X, b, c⟩ = ⟨X, Y, c⟩$
14		predeq3	$⊢ ⟨X, b, c⟩ = ⟨X, Y, c⟩ \to Pred (U, ((A \times B) \times C), ⟨X, b, c⟩) = Pred (U, ((A \times B) \times C), ⟨X, Y, c⟩)$
15	13 14	syl	$⊢ b = Y \to Pred (U, ((A \times B) \times C), ⟨X, b, c⟩) = Pred (U, ((A \times B) \times C), ⟨X, Y, c⟩)$
16		predeq3	$⊢ b = Y \to Pred (S, B, b) = Pred (S, B, Y)$
17		sneq	$⊢ b = Y \to \{b\} = \{Y\}$
18	16 17	uneq12d	$⊢ b = Y \to Pred (S, B, b) \cup \{b\} = Pred (S, B, Y) \cup \{Y\}$
19	18	xpeq2d	$⊢ b = Y \to (Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, b) \cup \{b\}) = (Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, Y) \cup \{Y\})$
20	19	xpeq1d	$⊢ b = Y \to ((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\}) = ((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, Y) \cup \{Y\})) \times (Pred (T, C, c) \cup \{c\})$
21	13	sneqd	$⊢ b = Y \to \{⟨X, b, c⟩\} = \{⟨X, Y, c⟩\}$
22	20 21	difeq12d	$⊢ b = Y \to (((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨X, b, c⟩\} = (((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, Y) \cup \{Y\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨X, Y, c⟩\}$
23	15 22	eqeq12d	$⊢ b = Y \to (Pred (U, ((A \times B) \times C), ⟨X, b, c⟩) = (((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨X, b, c⟩\} \leftrightarrow Pred (U, ((A \times B) \times C), ⟨X, Y, c⟩) = (((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, Y) \cup \{Y\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨X, Y, c⟩\})$
24		oteq3	$⊢ c = Z \to ⟨X, Y, c⟩ = ⟨X, Y, Z⟩$
25		predeq3	$⊢ ⟨X, Y, c⟩ = ⟨X, Y, Z⟩ \to Pred (U, ((A \times B) \times C), ⟨X, Y, c⟩) = Pred (U, ((A \times B) \times C), ⟨X, Y, Z⟩)$
26	24 25	syl	$⊢ c = Z \to Pred (U, ((A \times B) \times C), ⟨X, Y, c⟩) = Pred (U, ((A \times B) \times C), ⟨X, Y, Z⟩)$
27		predeq3	$⊢ c = Z \to Pred (T, C, c) = Pred (T, C, Z)$
28		sneq	$⊢ c = Z \to \{c\} = \{Z\}$
29	27 28	uneq12d	$⊢ c = Z \to Pred (T, C, c) \cup \{c\} = Pred (T, C, Z) \cup \{Z\}$
30	29	xpeq2d	$⊢ c = Z \to ((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, Y) \cup \{Y\})) \times (Pred (T, C, c) \cup \{c\}) = ((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, Y) \cup \{Y\})) \times (Pred (T, C, Z) \cup \{Z\})$
31	24	sneqd	$⊢ c = Z \to \{⟨X, Y, c⟩\} = \{⟨X, Y, Z⟩\}$
32	30 31	difeq12d	$⊢ c = Z \to (((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, Y) \cup \{Y\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨X, Y, c⟩\} = (((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, Y) \cup \{Y\})) \times (Pred (T, C, Z) \cup \{Z\})) ∖ \{⟨X, Y, Z⟩\}$
33	26 32	eqeq12d	$⊢ c = Z \to (Pred (U, ((A \times B) \times C), ⟨X, Y, c⟩) = (((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, Y) \cup \{Y\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨X, Y, c⟩\} \leftrightarrow Pred (U, ((A \times B) \times C), ⟨X, Y, Z⟩) = (((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, Y) \cup \{Y\})) \times (Pred (T, C, Z) \cup \{Z\})) ∖ \{⟨X, Y, Z⟩\})$
34		el2xptp	$⊢ q \in ((A \times B) \times C) \leftrightarrow \exists d \in A \exists e \in B \exists f \in C q = ⟨d, e, f⟩$
35		df-3an	$⊢ ((d \in A \land e \in B \land f \in C) \land (a \in A \land b \in B \land c \in C) \land (((d R a \lor d = a) \land (e S b \lor e = b) \land (f T c \lor f = c)) \land (d \neq a \lor e \neq b \lor f \neq c))) \leftrightarrow (((d \in A \land e \in B \land f \in C) \land (a \in A \land b \in B \land c \in C)) \land (((d R a \lor d = a) \land (e S b \lor e = b) \land (f T c \lor f = c)) \land (d \neq a \lor e \neq b \lor f \neq c)))$
36		simplrl	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to d \in A$
37		simplrr	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to e \in B$
38		simpr	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to f \in C$
39	36 37 38	3jca	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to (d \in A \land e \in B \land f \in C)$
40		simpll	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to (a \in A \land b \in B \land c \in C)$
41	39 40	jca	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to ((d \in A \land e \in B \land f \in C) \land (a \in A \land b \in B \land c \in C))$
42	41	biantrurd	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to ((((d R a \lor d = a) \land (e S b \lor e = b) \land (f T c \lor f = c)) \land (d \neq a \lor e \neq b \lor f \neq c)) \leftrightarrow (((d \in A \land e \in B \land f \in C) \land (a \in A \land b \in B \land c \in C)) \land (((d R a \lor d = a) \land (e S b \lor e = b) \land (f T c \lor f = c)) \land (d \neq a \lor e \neq b \lor f \neq c))))$
43	36	biantrurd	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to (d R a \leftrightarrow (d \in A \land d R a))$
44	43	orbi1d	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to ((d R a \lor d = a) \leftrightarrow ((d \in A \land d R a) \lor d = a))$
45	37	biantrurd	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to (e S b \leftrightarrow (e \in B \land e S b))$
46	45	orbi1d	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to ((e S b \lor e = b) \leftrightarrow ((e \in B \land e S b) \lor e = b))$
47	38	biantrurd	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to (f T c \leftrightarrow (f \in C \land f T c))$
48	47	orbi1d	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to ((f T c \lor f = c) \leftrightarrow ((f \in C \land f T c) \lor f = c))$
49	44 46 48	3anbi123d	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to (((d R a \lor d = a) \land (e S b \lor e = b) \land (f T c \lor f = c)) \leftrightarrow (((d \in A \land d R a) \lor d = a) \land ((e \in B \land e S b) \lor e = b) \land ((f \in C \land f T c) \lor f = c)))$
50	49	anbi1d	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to ((((d R a \lor d = a) \land (e S b \lor e = b) \land (f T c \lor f = c)) \land (d \neq a \lor e \neq b \lor f \neq c)) \leftrightarrow ((((d \in A \land d R a) \lor d = a) \land ((e \in B \land e S b) \lor e = b) \land ((f \in C \land f T c) \lor f = c)) \land (d \neq a \lor e \neq b \lor f \neq c)))$
51	42 50	bitr3d	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to ((((d \in A \land e \in B \land f \in C) \land (a \in A \land b \in B \land c \in C)) \land (((d R a \lor d = a) \land (e S b \lor e = b) \land (f T c \lor f = c)) \land (d \neq a \lor e \neq b \lor f \neq c))) \leftrightarrow ((((d \in A \land d R a) \lor d = a) \land ((e \in B \land e S b) \lor e = b) \land ((f \in C \land f T c) \lor f = c)) \land (d \neq a \lor e \neq b \lor f \neq c)))$
52	35 51	bitrid	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to (((d \in A \land e \in B \land f \in C) \land (a \in A \land b \in B \land c \in C) \land (((d R a \lor d = a) \land (e S b \lor e = b) \land (f T c \lor f = c)) \land (d \neq a \lor e \neq b \lor f \neq c))) \leftrightarrow ((((d \in A \land d R a) \lor d = a) \land ((e \in B \land e S b) \lor e = b) \land ((f \in C \land f T c) \lor f = c)) \land (d \neq a \lor e \neq b \lor f \neq c)))$
53		breq1	$⊢ q = ⟨d, e, f⟩ \to (q U ⟨a, b, c⟩ \leftrightarrow ⟨d, e, f⟩ U ⟨a, b, c⟩)$
54	1	xpord3lem	$⊢ ⟨d, e, f⟩ U ⟨a, b, c⟩ \leftrightarrow ((d \in A \land e \in B \land f \in C) \land (a \in A \land b \in B \land c \in C) \land (((d R a \lor d = a) \land (e S b \lor e = b) \land (f T c \lor f = c)) \land (d \neq a \lor e \neq b \lor f \neq c)))$
55	53 54	bitrdi	$⊢ q = ⟨d, e, f⟩ \to (q U ⟨a, b, c⟩ \leftrightarrow ((d \in A \land e \in B \land f \in C) \land (a \in A \land b \in B \land c \in C) \land (((d R a \lor d = a) \land (e S b \lor e = b) \land (f T c \lor f = c)) \land (d \neq a \lor e \neq b \lor f \neq c))))$
56		eleq1	$⊢ q = ⟨d, e, f⟩ \to (q \in ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\}) \leftrightarrow ⟨d, e, f⟩ \in ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\}))$
57		eldifsn	$⊢ ⟨d, e, f⟩ \in ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\}) \leftrightarrow (⟨d, e, f⟩ \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) \land ⟨d, e, f⟩ \neq ⟨a, b, c⟩)$
58		otelxp	$⊢ ⟨d, e, f⟩ \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) \leftrightarrow (d \in (Pred (R, A, a) \cup \{a\}) \land e \in (Pred (S, B, b) \cup \{b\}) \land f \in (Pred (T, C, c) \cup \{c\}))$
59		elun	$⊢ d \in (Pred (R, A, a) \cup \{a\}) \leftrightarrow (d \in Pred (R, A, a) \lor d \in \{a\})$
60		vex	$⊢ d \in V$
61	60	elpred	$⊢ a \in V \to (d \in Pred (R, A, a) \leftrightarrow (d \in A \land d R a))$
62	61	elv	$⊢ d \in Pred (R, A, a) \leftrightarrow (d \in A \land d R a)$
63		velsn	$⊢ d \in \{a\} \leftrightarrow d = a$
64	62 63	orbi12i	$⊢ (d \in Pred (R, A, a) \lor d \in \{a\}) \leftrightarrow ((d \in A \land d R a) \lor d = a)$
65	59 64	bitri	$⊢ d \in (Pred (R, A, a) \cup \{a\}) \leftrightarrow ((d \in A \land d R a) \lor d = a)$
66		elun	$⊢ e \in (Pred (S, B, b) \cup \{b\}) \leftrightarrow (e \in Pred (S, B, b) \lor e \in \{b\})$
67		vex	$⊢ e \in V$
68	67	elpred	$⊢ b \in V \to (e \in Pred (S, B, b) \leftrightarrow (e \in B \land e S b))$
69	68	elv	$⊢ e \in Pred (S, B, b) \leftrightarrow (e \in B \land e S b)$
70		velsn	$⊢ e \in \{b\} \leftrightarrow e = b$
71	69 70	orbi12i	$⊢ (e \in Pred (S, B, b) \lor e \in \{b\}) \leftrightarrow ((e \in B \land e S b) \lor e = b)$
72	66 71	bitri	$⊢ e \in (Pred (S, B, b) \cup \{b\}) \leftrightarrow ((e \in B \land e S b) \lor e = b)$
73		elun	$⊢ f \in (Pred (T, C, c) \cup \{c\}) \leftrightarrow (f \in Pred (T, C, c) \lor f \in \{c\})$
74		vex	$⊢ f \in V$
75	74	elpred	$⊢ c \in V \to (f \in Pred (T, C, c) \leftrightarrow (f \in C \land f T c))$
76	75	elv	$⊢ f \in Pred (T, C, c) \leftrightarrow (f \in C \land f T c)$
77		velsn	$⊢ f \in \{c\} \leftrightarrow f = c$
78	76 77	orbi12i	$⊢ (f \in Pred (T, C, c) \lor f \in \{c\}) \leftrightarrow ((f \in C \land f T c) \lor f = c)$
79	73 78	bitri	$⊢ f \in (Pred (T, C, c) \cup \{c\}) \leftrightarrow ((f \in C \land f T c) \lor f = c)$
80	65 72 79	3anbi123i	$⊢ (d \in (Pred (R, A, a) \cup \{a\}) \land e \in (Pred (S, B, b) \cup \{b\}) \land f \in (Pred (T, C, c) \cup \{c\})) \leftrightarrow (((d \in A \land d R a) \lor d = a) \land ((e \in B \land e S b) \lor e = b) \land ((f \in C \land f T c) \lor f = c))$
81	58 80	bitri	$⊢ ⟨d, e, f⟩ \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) \leftrightarrow (((d \in A \land d R a) \lor d = a) \land ((e \in B \land e S b) \lor e = b) \land ((f \in C \land f T c) \lor f = c))$
82	60 67 74	otthne	$⊢ ⟨d, e, f⟩ \neq ⟨a, b, c⟩ \leftrightarrow (d \neq a \lor e \neq b \lor f \neq c)$
83	81 82	anbi12i	$⊢ (⟨d, e, f⟩ \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) \land ⟨d, e, f⟩ \neq ⟨a, b, c⟩) \leftrightarrow ((((d \in A \land d R a) \lor d = a) \land ((e \in B \land e S b) \lor e = b) \land ((f \in C \land f T c) \lor f = c)) \land (d \neq a \lor e \neq b \lor f \neq c))$
84	57 83	bitri	$⊢ ⟨d, e, f⟩ \in ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\}) \leftrightarrow ((((d \in A \land d R a) \lor d = a) \land ((e \in B \land e S b) \lor e = b) \land ((f \in C \land f T c) \lor f = c)) \land (d \neq a \lor e \neq b \lor f \neq c))$
85	56 84	bitrdi	$⊢ q = ⟨d, e, f⟩ \to (q \in ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\}) \leftrightarrow ((((d \in A \land d R a) \lor d = a) \land ((e \in B \land e S b) \lor e = b) \land ((f \in C \land f T c) \lor f = c)) \land (d \neq a \lor e \neq b \lor f \neq c)))$
86	55 85	bibi12d	$⊢ q = ⟨d, e, f⟩ \to ((q U ⟨a, b, c⟩ \leftrightarrow q \in ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\})) \leftrightarrow (((d \in A \land e \in B \land f \in C) \land (a \in A \land b \in B \land c \in C) \land (((d R a \lor d = a) \land (e S b \lor e = b) \land (f T c \lor f = c)) \land (d \neq a \lor e \neq b \lor f \neq c))) \leftrightarrow ((((d \in A \land d R a) \lor d = a) \land ((e \in B \land e S b) \lor e = b) \land ((f \in C \land f T c) \lor f = c)) \land (d \neq a \lor e \neq b \lor f \neq c))))$
87	52 86	syl5ibrcom	$⊢ (((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \land f \in C) \to (q = ⟨d, e, f⟩ \to (q U ⟨a, b, c⟩ \leftrightarrow q \in ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\})))$
88	87	rexlimdva	$⊢ ((a \in A \land b \in B \land c \in C) \land (d \in A \land e \in B)) \to (\exists f \in C q = ⟨d, e, f⟩ \to (q U ⟨a, b, c⟩ \leftrightarrow q \in ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\})))$
89	88	rexlimdvva	$⊢ (a \in A \land b \in B \land c \in C) \to (\exists d \in A \exists e \in B \exists f \in C q = ⟨d, e, f⟩ \to (q U ⟨a, b, c⟩ \leftrightarrow q \in ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\})))$
90	34 89	biimtrid	$⊢ (a \in A \land b \in B \land c \in C) \to (q \in ((A \times B) \times C) \to (q U ⟨a, b, c⟩ \leftrightarrow q \in ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\})))$
91	90	pm5.32d	$⊢ (a \in A \land b \in B \land c \in C) \to ((q \in ((A \times B) \times C) \land q U ⟨a, b, c⟩) \leftrightarrow (q \in ((A \times B) \times C) \land q \in ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\})))$
92		otex	$⊢ ⟨a, b, c⟩ \in V$
93		vex	$⊢ q \in V$
94	93	elpred	$⊢ ⟨a, b, c⟩ \in V \to (q \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \leftrightarrow (q \in ((A \times B) \times C) \land q U ⟨a, b, c⟩))$
95	92 94	ax-mp	$⊢ q \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \leftrightarrow (q \in ((A \times B) \times C) \land q U ⟨a, b, c⟩)$
96		elin	$⊢ q \in (((A \times B) \times C) \cap ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\})) \leftrightarrow (q \in ((A \times B) \times C) \land q \in ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\}))$
97	91 95 96	3bitr4g	$⊢ (a \in A \land b \in B \land c \in C) \to (q \in Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) \leftrightarrow q \in (((A \times B) \times C) \cap ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\})))$
98	97	eqrdv	$⊢ (a \in A \land b \in B \land c \in C) \to Pred (U, ((A \times B) \times C), ⟨a, b, c⟩) = ((A \times B) \times C) \cap ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\})$
99		predss	$⊢ Pred (R, A, a) \subseteq A$
100	99	a1i	$⊢ a \in A \to Pred (R, A, a) \subseteq A$
101		snssi	$⊢ a \in A \to \{a\} \subseteq A$
102	100 101	unssd	$⊢ a \in A \to Pred (R, A, a) \cup \{a\} \subseteq A$
103	102	3ad2ant1	$⊢ (a \in A \land b \in B \land c \in C) \to Pred (R, A, a) \cup \{a\} \subseteq A$
104		predss	$⊢ Pred (S, B, b) \subseteq B$
105	104	a1i	$⊢ b \in B \to Pred (S, B, b) \subseteq B$
106		snssi	$⊢ b \in B \to \{b\} \subseteq B$
107	105 106	unssd	$⊢ b \in B \to Pred (S, B, b) \cup \{b\} \subseteq B$
108	107	3ad2ant2	$⊢ (a \in A \land b \in B \land c \in C) \to Pred (S, B, b) \cup \{b\} \subseteq B$
109		xpss12	$⊢ (Pred (R, A, a) \cup \{a\} \subseteq A \land Pred (S, B, b) \cup \{b\} \subseteq B) \to (Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\}) \subseteq A \times B$
110	103 108 109	syl2anc	$⊢ (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\}) \subseteq A \times B$
111		predss	$⊢ Pred (T, C, c) \subseteq C$
112	111	a1i	$⊢ c \in C \to Pred (T, C, c) \subseteq C$
113		snssi	$⊢ c \in C \to \{c\} \subseteq C$
114	112 113	unssd	$⊢ c \in C \to Pred (T, C, c) \cup \{c\} \subseteq C$
115	114	3ad2ant3	$⊢ (a \in A \land b \in B \land c \in C) \to Pred (T, C, c) \cup \{c\} \subseteq C$
116		xpss12	$⊢ ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\}) \subseteq A \times B \land Pred (T, C, c) \cup \{c\} \subseteq C) \to ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\}) \subseteq (A \times B) \times C$
117	110 115 116	syl2anc	$⊢ (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\}) \subseteq (A \times B) \times C$
118	117	ssdifssd	$⊢ (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⟩\} \subseteq (A \times B) \times C$
119		sseqin2	$⊢ (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{c\})) ∖ \{⟨a, b, c⟩\} \subseteq (A \times B) \times C \leftrightarrow ((A \times B) \times C) \cap ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{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⟩\}$
120	118 119	sylib	$⊢ (a \in A \land b \in B \land c \in C) \to ((A \times B) \times C) \cap ((((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \times (Pred (T, C, c) \cup \{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⟩\}$
121	98 120	eqtrd	$⊢ (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⟩\}$
122	12 23 33 121	vtocl3ga	$⊢ (X \in A \land Y \in B \land Z \in C) \to Pred (U, ((A \times B) \times C), ⟨X, Y, Z⟩) = (((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, Y) \cup \{Y\})) \times (Pred (T, C, Z) \cup \{Z\})) ∖ \{⟨X, Y, Z⟩\}$

Metamath Proof Explorer

Theorem xpord3pred

Proof