xpord2pred - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > xpord2pred		Structured version Visualization version GIF version

Theorem xpord2pred 33792

Description: Calculate the predecessor class in frxp2 33791. (Contributed by Scott Fenton, 22-Aug-2024.)

**Hypothesis**
Ref	Expression
xpord2.1	⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥)𝑆(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}

**Assertion**
Ref	Expression
xpord2pred	⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))

Distinct variable groups: 𝑥,𝐴,𝑦 𝑥,𝐵,𝑦 𝑥,𝑅,𝑦 𝑥,𝑆,𝑦 Allowed substitution hints: 𝑇(𝑥,𝑦) 𝑋(𝑥,𝑦) 𝑌(𝑥,𝑦)

Proof of Theorem xpord2pred Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		opeq1 4804	. . . 4 ⊢ (𝑎 = 𝑋 → ⟨𝑎, 𝑏⟩ = ⟨𝑋, 𝑏⟩)
2		predeq3 6206	. . . 4 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑋, 𝑏⟩ → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩))
3	1, 2	syl 17	. . 3 ⊢ (𝑎 = 𝑋 → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩))
4		predeq3 6206	. . . . . 6 ⊢ (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋))
5		sneq 4571	. . . . . 6 ⊢ (𝑎 = 𝑋 → {𝑎} = {𝑋})
6	4, 5	uneq12d 4098	. . . . 5 ⊢ (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}))
7	6	xpeq1d 5618	. . . 4 ⊢ (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
8	1	sneqd 4573	. . . 4 ⊢ (𝑎 = 𝑋 → {⟨𝑎, 𝑏⟩} = {⟨𝑋, 𝑏⟩})
9	7, 8	difeq12d 4058	. . 3 ⊢ (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}))
10	3, 9	eqeq12d 2754	. 2 ⊢ (𝑎 = 𝑋 → (Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩})))
11		opeq2 4805	. . . 4 ⊢ (𝑏 = 𝑌 → ⟨𝑋, 𝑏⟩ = ⟨𝑋, 𝑌⟩)
12		predeq3 6206	. . . 4 ⊢ (⟨𝑋, 𝑏⟩ = ⟨𝑋, 𝑌⟩ → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩))
13	11, 12	syl 17	. . 3 ⊢ (𝑏 = 𝑌 → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩))
14		predeq3 6206	. . . . . 6 ⊢ (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌))
15		sneq 4571	. . . . . 6 ⊢ (𝑏 = 𝑌 → {𝑏} = {𝑌})
16	14, 15	uneq12d 4098	. . . . 5 ⊢ (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))
17	16	xpeq2d 5619	. . . 4 ⊢ (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})))
18	11	sneqd 4573	. . . 4 ⊢ (𝑏 = 𝑌 → {⟨𝑋, 𝑏⟩} = {⟨𝑋, 𝑌⟩})
19	17, 18	difeq12d 4058	. . 3 ⊢ (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))
20	13, 19	eqeq12d 2754	. 2 ⊢ (𝑏 = 𝑌 → (Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}) ↔ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩})))
21		predel 6223	. . . . 5 ⊢ (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝑒 ∈ (𝐴 × 𝐵))
22	21	a1i 11	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝑒 ∈ (𝐴 × 𝐵)))
23		eldifi 4061	. . . . 5 ⊢ (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) → 𝑒 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
24		predss 6210	. . . . . . . . 9 ⊢ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴
25	24	a1i 11	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴)
26		snssi 4741	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐴 → {𝑎} ⊆ 𝐴)
27	25, 26	unssd 4120	. . . . . . 7 ⊢ (𝑎 ∈ 𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
28		predss 6210	. . . . . . . . 9 ⊢ Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵
29	28	a1i 11	. . . . . . . 8 ⊢ (𝑏 ∈ 𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵)
30		snssi 4741	. . . . . . . 8 ⊢ (𝑏 ∈ 𝐵 → {𝑏} ⊆ 𝐵)
31	29, 30	unssd 4120	. . . . . . 7 ⊢ (𝑏 ∈ 𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
32		xpss12 5604	. . . . . . 7 ⊢ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
33	27, 31, 32	syl2an 596	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
34	33	sseld 3920	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → 𝑒 ∈ (𝐴 × 𝐵)))
35	23, 34	syl5 34	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) → 𝑒 ∈ (𝐴 × 𝐵)))
36		elxp2 5613	. . . . 5 ⊢ (𝑒 ∈ (𝐴 × 𝐵) ↔ ∃𝑐 ∈ 𝐴 ∃𝑑 ∈ 𝐵 𝑒 = ⟨𝑐, 𝑑⟩)
37		opex 5379	. . . . . . . . 9 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
38		opex 5379	. . . . . . . . . 10 ⊢ ⟨𝑐, 𝑑⟩ ∈ V
39	38	elpred 6219	. . . . . . . . 9 ⊢ (⟨𝑎, 𝑏⟩ ∈ V → (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩)))
40	37, 39	ax-mp 5	. . . . . . . 8 ⊢ (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩))
41		opelxpi 5626	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) → ⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵))
42	41	adantl 482	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵))
43	42	biantrurd 533	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩ ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩)))
44		xpord2.1	. . . . . . . . . . 11 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥)𝑆(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}
45	44	xpord2lem 33789	. . . . . . . . . 10 ⊢ (⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩ ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
46		eldif 3897	. . . . . . . . . . . . 13 ⊢ (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩}))
47		opelxp 5625	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
48		elun 4083	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑐 ∈ {𝑎}))
49		vex 3436	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑐 ∈ V
50	49	elpred 6219	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ V → (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎)))
51	50	elv 3438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎))
52		velsn 4577	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ {𝑎} ↔ 𝑐 = 𝑎)
53	51, 52	orbi12i 912	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑐 ∈ {𝑎}) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎))
54	48, 53	bitri 274	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎))
55		elun 4083	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑑 ∈ {𝑏}))
56		vex 3436	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑑 ∈ V
57	56	elpred 6219	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ V → (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏)))
58	57	elv 3438	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏))
59		velsn 4577	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ {𝑏} ↔ 𝑑 = 𝑏)
60	58, 59	orbi12i 912	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑑 ∈ {𝑏}) ↔ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏))
61	55, 60	bitri 274	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏))
62	54, 61	anbi12i 627	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
63	47, 62	bitri 274	. . . . . . . . . . . . . 14 ⊢ (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
64	38	elsn 4576	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
65	64	notbii 320	. . . . . . . . . . . . . . 15 ⊢ (¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ ¬ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
66		df-ne 2944	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑐, 𝑑⟩ ≠ ⟨𝑎, 𝑏⟩ ↔ ¬ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
67	49, 56	opthne 5397	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑐, 𝑑⟩ ≠ ⟨𝑎, 𝑏⟩ ↔ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))
68	65, 66, 67	3bitr2i 299	. . . . . . . . . . . . . 14 ⊢ (¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))
69	63, 68	anbi12i 627	. . . . . . . . . . . . 13 ⊢ ((⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩}) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))
70	46, 69	bitri 274	. . . . . . . . . . . 12 ⊢ (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))
71		simprl 768	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → 𝑐 ∈ 𝐴)
72	71	biantrurd 533	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (𝑐𝑅𝑎 ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎)))
73	72	orbi1d 914	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎)))
74		simprr 770	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → 𝑑 ∈ 𝐵)
75	74	biantrurd 533	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (𝑑𝑆𝑏 ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏)))
76	75	orbi1d 914	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ↔ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
77	73, 76	3anbi12d 1436	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
78		df-3an 1088	. . . . . . . . . . . . 13 ⊢ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))
79	77, 78	bitr2di 288	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
80	70, 79	syl5bb 283	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
81		pm3.22 460	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)))
82	81	biantrurd 533	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))))
83		df-3an 1088	. . . . . . . . . . . 12 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
84	82, 83	bitr4di 289	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))))
85	80, 84	bitr2d 279	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
86	45, 85	syl5bb 283	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
87	43, 86	bitr3d 280	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
88	40, 87	syl5bb 283	. . . . . . 7 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
89		eleq1 2826	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩)))
90		eleq1 2826	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
91	89, 90	bibi12d 346	. . . . . . 7 ⊢ (𝑒 = ⟨𝑐, 𝑑⟩ → ((𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})) ↔ (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
92	88, 91	syl5ibrcom 246	. . . . . 6 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
93	92	rexlimdvva 3223	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∃𝑐 ∈ 𝐴 ∃𝑑 ∈ 𝐵 𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
94	36, 93	syl5bi 241	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ (𝐴 × 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
95	22, 35, 94	pm5.21ndd 381	. . 3 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
96	95	eqrdv 2736	. 2 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))
97	10, 20, 96	vtocl2ga 3514	1 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∃wrex 3065 Vcvv 3432 ∖ cdif 3884 ∪ cun 3885 ⊆ wss 3887 {csn 4561 ⟨cop 4567 class class class wbr 5074 {copab 5136 × cxp 5587 Predcpred 6201 ‘cfv 6433 1^st c1st 7829 2^nd c2nd 7830

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 ax-un 7588

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5489 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-pred 6202 df-iota 6391 df-fun 6435 df-fv 6441 df-1st 7831 df-2nd 7832

This theorem is referenced by: sexp2 33793 xpord2ind 33794 on2recsov 33827 noxpordpred 34110

W3C validator