xpord3pred

Description: Calculate the predecsessor class for the triple order. (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	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		opeq1	$⊢ a = X \to ⟨a, b⟩ = ⟨X, b⟩$
3	2	opeq1d	$⊢ a = X \to ⟨⟨a, b⟩, c⟩ = ⟨⟨X, b⟩, c⟩$
4		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⟩)$
5	3 4	syl	$⊢ a = X \to Pred (U, ((A \times B) \times C), ⟨⟨a, b⟩, c⟩) = Pred (U, ((A \times B) \times C), ⟨⟨X, b⟩, c⟩)$
6		predeq3	$⊢ a = X \to Pred (R, A, a) = Pred (R, A, X)$
7		sneq	$⊢ a = X \to \{a\} = \{X\}$
8	6 7	uneq12d	$⊢ a = X \to Pred (R, A, a) \cup \{a\} = Pred (R, A, X) \cup \{X\}$
9	8	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\})$
10	9	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\})$
11	3	sneqd	$⊢ a = X \to \{⟨⟨a, b⟩, c⟩\} = \{⟨⟨X, b⟩, c⟩\}$
12	10 11	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⟩\}$
13	5 12	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⟩\})$
14		opeq2	$⊢ b = Y \to ⟨X, b⟩ = ⟨X, Y⟩$
15	14	opeq1d	$⊢ b = Y \to ⟨⟨X, b⟩, c⟩ = ⟨⟨X, Y⟩, c⟩$
16		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⟩)$
17	15 16	syl	$⊢ b = Y \to Pred (U, ((A \times B) \times C), ⟨⟨X, b⟩, c⟩) = Pred (U, ((A \times B) \times C), ⟨⟨X, Y⟩, c⟩)$
18		predeq3	$⊢ b = Y \to Pred (S, B, b) = Pred (S, B, Y)$
19		sneq	$⊢ b = Y \to \{b\} = \{Y\}$
20	18 19	uneq12d	$⊢ b = Y \to Pred (S, B, b) \cup \{b\} = Pred (S, B, Y) \cup \{Y\}$
21	20	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\})$
22	21	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\})$
23	15	sneqd	$⊢ b = Y \to \{⟨⟨X, b⟩, c⟩\} = \{⟨⟨X, Y⟩, c⟩\}$
24	22 23	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⟩\}$
25	17 24	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⟩\})$
26		opeq2	$⊢ c = Z \to ⟨⟨X, Y⟩, c⟩ = ⟨⟨X, Y⟩, Z⟩$
27		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⟩)$
28	26 27	syl	$⊢ c = Z \to Pred (U, ((A \times B) \times C), ⟨⟨X, Y⟩, c⟩) = Pred (U, ((A \times B) \times C), ⟨⟨X, Y⟩, Z⟩)$
29		predeq3	$⊢ c = Z \to Pred (T, C, c) = Pred (T, C, Z)$
30		sneq	$⊢ c = Z \to \{c\} = \{Z\}$
31	29 30	uneq12d	$⊢ c = Z \to Pred (T, C, c) \cup \{c\} = Pred (T, C, Z) \cup \{Z\}$
32	31	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\})$
33	26	sneqd	$⊢ c = Z \to \{⟨⟨X, Y⟩, c⟩\} = \{⟨⟨X, Y⟩, Z⟩\}$
34	32 33	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⟩\}$
35	28 34	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⟩\})$
36		elxpxp	$⊢ q \in ((A \times B) \times C) \leftrightarrow \exists d \in A \exists e \in B \exists f \in C q = ⟨⟨d, e⟩, f⟩$
37		df-3an	$⊢ (d \in A \land e \in B \land f \in C) \leftrightarrow ((d \in A \land e \in B) \land f \in C)$
38		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)))$
39		eldif	$⊢ ⟨⟨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 \neg ⟨⟨d, e⟩, f⟩ \in \{⟨⟨a, b⟩, c⟩\})$
40		opelxp	$⊢ ⟨⟨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, e⟩ \in ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \land f \in (Pred (T, C, c) \cup \{c\}))$
41		opelxp	$⊢ ⟨d, e⟩ \in ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \leftrightarrow (d \in (Pred (R, A, a) \cup \{a\}) \land e \in (Pred (S, B, b) \cup \{b\}))$
42		elun	$⊢ d \in (Pred (R, A, a) \cup \{a\}) \leftrightarrow (d \in Pred (R, A, a) \lor d \in \{a\})$
43		vex	$⊢ d \in V$
44	43	elpred	$⊢ a \in V \to (d \in Pred (R, A, a) \leftrightarrow (d \in A \land d R a))$
45	44	elv	$⊢ d \in Pred (R, A, a) \leftrightarrow (d \in A \land d R a)$
46		velsn	$⊢ d \in \{a\} \leftrightarrow d = a$
47	45 46	orbi12i	$⊢ (d \in Pred (R, A, a) \lor d \in \{a\}) \leftrightarrow ((d \in A \land d R a) \lor d = a)$
48	42 47	bitri	$⊢ d \in (Pred (R, A, a) \cup \{a\}) \leftrightarrow ((d \in A \land d R a) \lor d = a)$
49		elun	$⊢ e \in (Pred (S, B, b) \cup \{b\}) \leftrightarrow (e \in Pred (S, B, b) \lor e \in \{b\})$
50		vex	$⊢ e \in V$
51	50	elpred	$⊢ b \in V \to (e \in Pred (S, B, b) \leftrightarrow (e \in B \land e S b))$
52	51	elv	$⊢ e \in Pred (S, B, b) \leftrightarrow (e \in B \land e S b)$
53		velsn	$⊢ e \in \{b\} \leftrightarrow e = b$
54	52 53	orbi12i	$⊢ (e \in Pred (S, B, b) \lor e \in \{b\}) \leftrightarrow ((e \in B \land e S b) \lor e = b)$
55	49 54	bitri	$⊢ e \in (Pred (S, B, b) \cup \{b\}) \leftrightarrow ((e \in B \land e S b) \lor e = b)$
56	48 55	anbi12i	$⊢ (d \in (Pred (R, A, a) \cup \{a\}) \land e \in (Pred (S, B, b) \cup \{b\})) \leftrightarrow (((d \in A \land d R a) \lor d = a) \land ((e \in B \land e S b) \lor e = b))$
57	41 56	bitri	$⊢ ⟨d, e⟩ \in ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \leftrightarrow (((d \in A \land d R a) \lor d = a) \land ((e \in B \land e S b) \lor e = b))$
58		elun	$⊢ f \in (Pred (T, C, c) \cup \{c\}) \leftrightarrow (f \in Pred (T, C, c) \lor f \in \{c\})$
59		vex	$⊢ f \in V$
60	59	elpred	$⊢ c \in V \to (f \in Pred (T, C, c) \leftrightarrow (f \in C \land f T c))$
61	60	elv	$⊢ f \in Pred (T, C, c) \leftrightarrow (f \in C \land f T c)$
62		velsn	$⊢ f \in \{c\} \leftrightarrow f = c$
63	61 62	orbi12i	$⊢ (f \in Pred (T, C, c) \lor f \in \{c\}) \leftrightarrow ((f \in C \land f T c) \lor f = c)$
64	58 63	bitri	$⊢ f \in (Pred (T, C, c) \cup \{c\}) \leftrightarrow ((f \in C \land f T c) \lor f = c)$
65	57 64	anbi12i	$⊢ (⟨d, e⟩ \in ((Pred (R, A, a) \cup \{a\}) \times (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))$
66	40 65	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))$
67		df-ne	$⊢ ⟨⟨d, e⟩, f⟩ \neq ⟨⟨a, b⟩, c⟩ \leftrightarrow \neg ⟨⟨d, e⟩, f⟩ = ⟨⟨a, b⟩, c⟩$
68	43 50 59	otthne	$⊢ ⟨⟨d, e⟩, f⟩ \neq ⟨⟨a, b⟩, c⟩ \leftrightarrow (d \neq a \lor e \neq b \lor f \neq c)$
69	67 68	bitr3i	$⊢ \neg ⟨⟨d, e⟩, f⟩ = ⟨⟨a, b⟩, c⟩ \leftrightarrow (d \neq a \lor e \neq b \lor f \neq c)$
70		opex	$⊢ ⟨⟨d, e⟩, f⟩ \in V$
71	70	elsn	$⊢ ⟨⟨d, e⟩, f⟩ \in \{⟨⟨a, b⟩, c⟩\} \leftrightarrow ⟨⟨d, e⟩, f⟩ = ⟨⟨a, b⟩, c⟩$
72	69 71	xchnxbir	$⊢ \neg ⟨⟨d, e⟩, f⟩ \in \{⟨⟨a, b⟩, c⟩\} \leftrightarrow (d \neq a \lor e \neq b \lor f \neq c)$
73	66 72	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 \neg ⟨⟨d, e⟩, f⟩ \in \{⟨⟨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))$
74	39 73	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))$
75		simpr1	$⊢ ((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$
76	75	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))$
77	76	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))$
78		simpr2	$⊢ ((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$
79	78	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))$
80	79	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))$
81		simpr3	$⊢ ((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$
82	81	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))$
83	82	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))$
84	77 80 83	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)))$
85		df-3an	$⊢ (((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)) \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))$
86	84 85	bitrdi	$⊢ ((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)))$
87	86	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)))$
88	74 87	bitr4id	$⊢ ((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, 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 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)))$
89		pm3.22	$⊢ ((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))$
90	89	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))))$
91	88 90	bitr2d	$⊢ ((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, 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⟩\}))$
92	38 91	syl5bb	$⊢ ((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, 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⟩\}))$
93		breq1	$⊢ q = ⟨⟨d, e⟩, f⟩ \to (q U ⟨⟨a, b⟩, c⟩ \leftrightarrow ⟨⟨d, e⟩, f⟩ U ⟨⟨a, b⟩, c⟩)$
94	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)))$
95	93 94	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))))$
96		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⟩\}))$
97	95 96	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, 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⟩\})))$
98	92 97	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⟩\})))$
99	37 98	sylan2br	$⊢ ((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⟩\})))$
100	99	anassrs	$⊢ (((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⟩\})))$
101	100	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⟩\})))$
102	101	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⟩\})))$
103	36 102	syl5bi	$⊢ (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⟩\})))$
104	103	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⟩\})))$
105		opex	$⊢ ⟨⟨a, b⟩, c⟩ \in V$
106		vex	$⊢ q \in V$
107	106	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⟩))$
108	105 107	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⟩)$
109		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⟩\}))$
110	104 108 109	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⟩\})))$
111	110	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⟩\})$
112		predss	$⊢ Pred (R, A, a) \subseteq A$
113	112	a1i	$⊢ a \in A \to Pred (R, A, a) \subseteq A$
114		snssi	$⊢ a \in A \to \{a\} \subseteq A$
115	113 114	unssd	$⊢ a \in A \to Pred (R, A, a) \cup \{a\} \subseteq A$
116	115	3ad2ant1	$⊢ (a \in A \land b \in B \land c \in C) \to Pred (R, A, a) \cup \{a\} \subseteq A$
117		predss	$⊢ Pred (S, B, b) \subseteq B$
118	117	a1i	$⊢ b \in B \to Pred (S, B, b) \subseteq B$
119		snssi	$⊢ b \in B \to \{b\} \subseteq B$
120	118 119	unssd	$⊢ b \in B \to Pred (S, B, b) \cup \{b\} \subseteq B$
121	120	3ad2ant2	$⊢ (a \in A \land b \in B \land c \in C) \to Pred (S, B, b) \cup \{b\} \subseteq B$
122		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$
123	116 121 122	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$
124		predss	$⊢ Pred (T, C, c) \subseteq C$
125	124	a1i	$⊢ c \in C \to Pred (T, C, c) \subseteq C$
126		snssi	$⊢ c \in C \to \{c\} \subseteq C$
127	125 126	unssd	$⊢ c \in C \to Pred (T, C, c) \cup \{c\} \subseteq C$
128	127	3ad2ant3	$⊢ (a \in A \land b \in B \land c \in C) \to Pred (T, C, c) \cup \{c\} \subseteq C$
129		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$
130	123 128 129	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$
131	130	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$
132		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⟩\}$
133	131 132	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⟩\}$
134	111 133	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⟩\}$
135	13 25 35 134	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