xpord2pred

Description: Calculate the predecessor class in frxp2 . (Contributed by Scott Fenton, 22-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	xpord2pred	$⊢ (X \in A \land Y \in B) \to Pred (T, (A \times B), ⟨X, Y⟩) = ((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, Y) \cup \{Y\})) ∖ \{⟨X, Y⟩\}$

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		opeq1	$⊢ a = X \to ⟨a, b⟩ = ⟨X, b⟩$
3		predeq3	$⊢ ⟨a, b⟩ = ⟨X, b⟩ \to Pred (T, (A \times B), ⟨a, b⟩) = Pred (T, (A \times B), ⟨X, b⟩)$
4	2 3	syl	$⊢ a = X \to Pred (T, (A \times B), ⟨a, b⟩) = Pred (T, (A \times B), ⟨X, b⟩)$
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	2	sneqd	$⊢ a = X \to \{⟨a, b⟩\} = \{⟨X, b⟩\}$
10	8 9	difeq12d	$⊢ a = X \to ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\} = ((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨X, b⟩\}$
11	4 10	eqeq12d	$⊢ a = X \to (Pred (T, (A \times B), ⟨a, b⟩) = ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\} \leftrightarrow Pred (T, (A \times B), ⟨X, b⟩) = ((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨X, b⟩\})$
12		opeq2	$⊢ b = Y \to ⟨X, b⟩ = ⟨X, Y⟩$
13		predeq3	$⊢ ⟨X, b⟩ = ⟨X, Y⟩ \to Pred (T, (A \times B), ⟨X, b⟩) = Pred (T, (A \times B), ⟨X, Y⟩)$
14	12 13	syl	$⊢ b = Y \to Pred (T, (A \times B), ⟨X, b⟩) = Pred (T, (A \times B), ⟨X, Y⟩)$
15		predeq3	$⊢ b = Y \to Pred (S, B, b) = Pred (S, B, Y)$
16		sneq	$⊢ b = Y \to \{b\} = \{Y\}$
17	15 16	uneq12d	$⊢ b = Y \to Pred (S, B, b) \cup \{b\} = Pred (S, B, Y) \cup \{Y\}$
18	17	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\})$
19	12	sneqd	$⊢ b = Y \to \{⟨X, b⟩\} = \{⟨X, Y⟩\}$
20	18 19	difeq12d	$⊢ b = Y \to ((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨X, b⟩\} = ((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, Y) \cup \{Y\})) ∖ \{⟨X, Y⟩\}$
21	14 20	eqeq12d	$⊢ b = Y \to (Pred (T, (A \times B), ⟨X, b⟩) = ((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨X, b⟩\} \leftrightarrow Pred (T, (A \times B), ⟨X, Y⟩) = ((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, Y) \cup \{Y\})) ∖ \{⟨X, Y⟩\})$
22		predel	$⊢ e \in Pred (T, (A \times B), ⟨a, b⟩) \to e \in (A \times B)$
23	22	a1i	$⊢ (a \in A \land b \in B) \to (e \in Pred (T, (A \times B), ⟨a, b⟩) \to e \in (A \times B))$
24		eldifi	$⊢ e \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\}) \to e \in ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\}))$
25		predss	$⊢ Pred (R, A, a) \subseteq A$
26	25	a1i	$⊢ a \in A \to Pred (R, A, a) \subseteq A$
27		snssi	$⊢ a \in A \to \{a\} \subseteq A$
28	26 27	unssd	$⊢ a \in A \to Pred (R, A, a) \cup \{a\} \subseteq A$
29		predss	$⊢ Pred (S, B, b) \subseteq B$
30	29	a1i	$⊢ b \in B \to Pred (S, B, b) \subseteq B$
31		snssi	$⊢ b \in B \to \{b\} \subseteq B$
32	30 31	unssd	$⊢ b \in B \to Pred (S, B, b) \cup \{b\} \subseteq B$
33		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$
34	28 32 33	syl2an	$⊢ (a \in A \land b \in B) \to (Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\}) \subseteq A \times B$
35	34	sseld	$⊢ (a \in A \land b \in B) \to (e \in ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \to e \in (A \times B))$
36	24 35	syl5	$⊢ (a \in A \land b \in B) \to (e \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\}) \to e \in (A \times B))$
37		elxp2	$⊢ e \in (A \times B) \leftrightarrow \exists c \in A \exists d \in B e = ⟨c, d⟩$
38		opex	$⊢ ⟨a, b⟩ \in V$
39		opex	$⊢ ⟨c, d⟩ \in V$
40	39	elpred	$⊢ ⟨a, b⟩ \in V \to (⟨c, d⟩ \in Pred (T, (A \times B), ⟨a, b⟩) \leftrightarrow (⟨c, d⟩ \in (A \times B) \land ⟨c, d⟩ T ⟨a, b⟩))$
41	38 40	ax-mp	$⊢ ⟨c, d⟩ \in Pred (T, (A \times B), ⟨a, b⟩) \leftrightarrow (⟨c, d⟩ \in (A \times B) \land ⟨c, d⟩ T ⟨a, b⟩)$
42		opelxpi	$⊢ (c \in A \land d \in B) \to ⟨c, d⟩ \in (A \times B)$
43	42	adantl	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to ⟨c, d⟩ \in (A \times B)$
44	43	biantrurd	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to (⟨c, d⟩ T ⟨a, b⟩ \leftrightarrow (⟨c, d⟩ \in (A \times B) \land ⟨c, d⟩ T ⟨a, b⟩))$
45	1	xpord2lem	$⊢ ⟨c, d⟩ T ⟨a, b⟩ \leftrightarrow ((c \in A \land d \in B) \land (a \in A \land b \in B) \land ((c R a \lor c = a) \land (d S b \lor d = b) \land (c \neq a \lor d \neq b)))$
46		eldif	$⊢ ⟨c, d⟩ \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\}) \leftrightarrow (⟨c, d⟩ \in ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \land \neg ⟨c, d⟩ \in \{⟨a, b⟩\})$
47		opelxp	$⊢ ⟨c, d⟩ \in ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \leftrightarrow (c \in (Pred (R, A, a) \cup \{a\}) \land d \in (Pred (S, B, b) \cup \{b\}))$
48		elun	$⊢ c \in (Pred (R, A, a) \cup \{a\}) \leftrightarrow (c \in Pred (R, A, a) \lor c \in \{a\})$
49		vex	$⊢ c \in V$
50	49	elpred	$⊢ a \in V \to (c \in Pred (R, A, a) \leftrightarrow (c \in A \land c R a))$
51	50	elv	$⊢ c \in Pred (R, A, a) \leftrightarrow (c \in A \land c R a)$
52		velsn	$⊢ c \in \{a\} \leftrightarrow c = a$
53	51 52	orbi12i	$⊢ (c \in Pred (R, A, a) \lor c \in \{a\}) \leftrightarrow ((c \in A \land c R a) \lor c = a)$
54	48 53	bitri	$⊢ c \in (Pred (R, A, a) \cup \{a\}) \leftrightarrow ((c \in A \land c R a) \lor c = a)$
55		elun	$⊢ d \in (Pred (S, B, b) \cup \{b\}) \leftrightarrow (d \in Pred (S, B, b) \lor d \in \{b\})$
56		vex	$⊢ d \in V$
57	56	elpred	$⊢ b \in V \to (d \in Pred (S, B, b) \leftrightarrow (d \in B \land d S b))$
58	57	elv	$⊢ d \in Pred (S, B, b) \leftrightarrow (d \in B \land d S b)$
59		velsn	$⊢ d \in \{b\} \leftrightarrow d = b$
60	58 59	orbi12i	$⊢ (d \in Pred (S, B, b) \lor d \in \{b\}) \leftrightarrow ((d \in B \land d S b) \lor d = b)$
61	55 60	bitri	$⊢ d \in (Pred (S, B, b) \cup \{b\}) \leftrightarrow ((d \in B \land d S b) \lor d = b)$
62	54 61	anbi12i	$⊢ (c \in (Pred (R, A, a) \cup \{a\}) \land d \in (Pred (S, B, b) \cup \{b\})) \leftrightarrow (((c \in A \land c R a) \lor c = a) \land ((d \in B \land d S b) \lor d = b))$
63	47 62	bitri	$⊢ ⟨c, d⟩ \in ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \leftrightarrow (((c \in A \land c R a) \lor c = a) \land ((d \in B \land d S b) \lor d = b))$
64	39	elsn	$⊢ ⟨c, d⟩ \in \{⟨a, b⟩\} \leftrightarrow ⟨c, d⟩ = ⟨a, b⟩$
65	64	notbii	$⊢ \neg ⟨c, d⟩ \in \{⟨a, b⟩\} \leftrightarrow \neg ⟨c, d⟩ = ⟨a, b⟩$
66		df-ne	$⊢ ⟨c, d⟩ \neq ⟨a, b⟩ \leftrightarrow \neg ⟨c, d⟩ = ⟨a, b⟩$
67	49 56	opthne	$⊢ ⟨c, d⟩ \neq ⟨a, b⟩ \leftrightarrow (c \neq a \lor d \neq b)$
68	65 66 67	3bitr2i	$⊢ \neg ⟨c, d⟩ \in \{⟨a, b⟩\} \leftrightarrow (c \neq a \lor d \neq b)$
69	63 68	anbi12i	$⊢ (⟨c, d⟩ \in ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) \land \neg ⟨c, d⟩ \in \{⟨a, b⟩\}) \leftrightarrow ((((c \in A \land c R a) \lor c = a) \land ((d \in B \land d S b) \lor d = b)) \land (c \neq a \lor d \neq b))$
70	46 69	bitri	$⊢ ⟨c, d⟩ \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\}) \leftrightarrow ((((c \in A \land c R a) \lor c = a) \land ((d \in B \land d S b) \lor d = b)) \land (c \neq a \lor d \neq b))$
71		simprl	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to c \in A$
72	71	biantrurd	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to (c R a \leftrightarrow (c \in A \land c R a))$
73	72	orbi1d	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to ((c R a \lor c = a) \leftrightarrow ((c \in A \land c R a) \lor c = a))$
74		simprr	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to d \in B$
75	74	biantrurd	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to (d S b \leftrightarrow (d \in B \land d S b))$
76	75	orbi1d	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to ((d S b \lor d = b) \leftrightarrow ((d \in B \land d S b) \lor d = b))$
77	73 76	3anbi12d	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to (((c R a \lor c = a) \land (d S b \lor d = b) \land (c \neq a \lor d \neq b)) \leftrightarrow (((c \in A \land c R a) \lor c = a) \land ((d \in B \land d S b) \lor d = b) \land (c \neq a \lor d \neq b)))$
78		df-3an	$⊢ (((c \in A \land c R a) \lor c = a) \land ((d \in B \land d S b) \lor d = b) \land (c \neq a \lor d \neq b)) \leftrightarrow ((((c \in A \land c R a) \lor c = a) \land ((d \in B \land d S b) \lor d = b)) \land (c \neq a \lor d \neq b))$
79	77 78	bitr2di	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to (((((c \in A \land c R a) \lor c = a) \land ((d \in B \land d S b) \lor d = b)) \land (c \neq a \lor d \neq b)) \leftrightarrow ((c R a \lor c = a) \land (d S b \lor d = b) \land (c \neq a \lor d \neq b)))$
80	70 79	syl5bb	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to (⟨c, d⟩ \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\}) \leftrightarrow ((c R a \lor c = a) \land (d S b \lor d = b) \land (c \neq a \lor d \neq b)))$
81		pm3.22	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to ((c \in A \land d \in B) \land (a \in A \land b \in B))$
82	81	biantrurd	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to (((c R a \lor c = a) \land (d S b \lor d = b) \land (c \neq a \lor d \neq b)) \leftrightarrow (((c \in A \land d \in B) \land (a \in A \land b \in B)) \land ((c R a \lor c = a) \land (d S b \lor d = b) \land (c \neq a \lor d \neq b))))$
83		df-3an	$⊢ ((c \in A \land d \in B) \land (a \in A \land b \in B) \land ((c R a \lor c = a) \land (d S b \lor d = b) \land (c \neq a \lor d \neq b))) \leftrightarrow (((c \in A \land d \in B) \land (a \in A \land b \in B)) \land ((c R a \lor c = a) \land (d S b \lor d = b) \land (c \neq a \lor d \neq b)))$
84	82 83	bitr4di	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to (((c R a \lor c = a) \land (d S b \lor d = b) \land (c \neq a \lor d \neq b)) \leftrightarrow ((c \in A \land d \in B) \land (a \in A \land b \in B) \land ((c R a \lor c = a) \land (d S b \lor d = b) \land (c \neq a \lor d \neq b))))$
85	80 84	bitr2d	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to (((c \in A \land d \in B) \land (a \in A \land b \in B) \land ((c R a \lor c = a) \land (d S b \lor d = b) \land (c \neq a \lor d \neq b))) \leftrightarrow ⟨c, d⟩ \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\}))$
86	45 85	syl5bb	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to (⟨c, d⟩ T ⟨a, b⟩ \leftrightarrow ⟨c, d⟩ \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\}))$
87	44 86	bitr3d	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to ((⟨c, d⟩ \in (A \times B) \land ⟨c, d⟩ T ⟨a, b⟩) \leftrightarrow ⟨c, d⟩ \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\}))$
88	41 87	syl5bb	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to (⟨c, d⟩ \in Pred (T, (A \times B), ⟨a, b⟩) \leftrightarrow ⟨c, d⟩ \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\}))$
89		eleq1	$⊢ e = ⟨c, d⟩ \to (e \in Pred (T, (A \times B), ⟨a, b⟩) \leftrightarrow ⟨c, d⟩ \in Pred (T, (A \times B), ⟨a, b⟩))$
90		eleq1	$⊢ e = ⟨c, d⟩ \to (e \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\}) \leftrightarrow ⟨c, d⟩ \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\}))$
91	89 90	bibi12d	$⊢ e = ⟨c, d⟩ \to ((e \in Pred (T, (A \times B), ⟨a, b⟩) \leftrightarrow e \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\})) \leftrightarrow (⟨c, d⟩ \in Pred (T, (A \times B), ⟨a, b⟩) \leftrightarrow ⟨c, d⟩ \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\})))$
92	88 91	syl5ibrcom	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B)) \to (e = ⟨c, d⟩ \to (e \in Pred (T, (A \times B), ⟨a, b⟩) \leftrightarrow e \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\})))$
93	92	rexlimdvva	$⊢ (a \in A \land b \in B) \to (\exists c \in A \exists d \in B e = ⟨c, d⟩ \to (e \in Pred (T, (A \times B), ⟨a, b⟩) \leftrightarrow e \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\})))$
94	37 93	syl5bi	$⊢ (a \in A \land b \in B) \to (e \in (A \times B) \to (e \in Pred (T, (A \times B), ⟨a, b⟩) \leftrightarrow e \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\})))$
95	23 36 94	pm5.21ndd	$⊢ (a \in A \land b \in B) \to (e \in Pred (T, (A \times B), ⟨a, b⟩) \leftrightarrow e \in (((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\}))$
96	95	eqrdv	$⊢ (a \in A \land b \in B) \to Pred (T, (A \times B), ⟨a, b⟩) = ((Pred (R, A, a) \cup \{a\}) \times (Pred (S, B, b) \cup \{b\})) ∖ \{⟨a, b⟩\}$
97	11 21 96	vtocl2ga	$⊢ (X \in A \land Y \in B) \to Pred (T, (A \times B), ⟨X, Y⟩) = ((Pred (R, A, X) \cup \{X\}) \times (Pred (S, B, Y) \cup \{Y\})) ∖ \{⟨X, Y⟩\}$

Metamath Proof Explorer

Theorem xpord2pred

Proof