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 33719

Description: Calculate the predecessor class in frxp2 33718. (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 4801	. . . 4 ⊢ (𝑎 = 𝑋 → ⟨𝑎, 𝑏⟩ = ⟨𝑋, 𝑏⟩)
2		predeq3 6195	. . . 4 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑋, 𝑏⟩ → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩))
3	1, 2	syl 17	. . 3 ⊢ (𝑎 = 𝑋 → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩))
4		predeq3 6195	. . . . . 6 ⊢ (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋))
5		sneq 4568	. . . . . 6 ⊢ (𝑎 = 𝑋 → {𝑎} = {𝑋})
6	4, 5	uneq12d 4094	. . . . 5 ⊢ (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}))
7	6	xpeq1d 5609	. . . 4 ⊢ (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
8	1	sneqd 4570	. . . 4 ⊢ (𝑎 = 𝑋 → {⟨𝑎, 𝑏⟩} = {⟨𝑋, 𝑏⟩})
9	7, 8	difeq12d 4054	. . 3 ⊢ (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}))
10	3, 9	eqeq12d 2754	. 2 ⊢ (𝑎 = 𝑋 → (Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩})))
11		opeq2 4802	. . . 4 ⊢ (𝑏 = 𝑌 → ⟨𝑋, 𝑏⟩ = ⟨𝑋, 𝑌⟩)
12		predeq3 6195	. . . 4 ⊢ (⟨𝑋, 𝑏⟩ = ⟨𝑋, 𝑌⟩ → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩))
13	11, 12	syl 17	. . 3 ⊢ (𝑏 = 𝑌 → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩))
14		predeq3 6195	. . . . . 6 ⊢ (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌))
15		sneq 4568	. . . . . 6 ⊢ (𝑏 = 𝑌 → {𝑏} = {𝑌})
16	14, 15	uneq12d 4094	. . . . 5 ⊢ (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))
17	16	xpeq2d 5610	. . . 4 ⊢ (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})))
18	11	sneqd 4570	. . . 4 ⊢ (𝑏 = 𝑌 → {⟨𝑋, 𝑏⟩} = {⟨𝑋, 𝑌⟩})
19	17, 18	difeq12d 4054	. . 3 ⊢ (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))
20	13, 19	eqeq12d 2754	. 2 ⊢ (𝑏 = 𝑌 → (Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}) ↔ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩})))
21		predel 6212	. . . . 5 ⊢ (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝑒 ∈ (𝐴 × 𝐵))
22	21	a1i 11	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝑒 ∈ (𝐴 × 𝐵)))
23		eldifi 4057	. . . . 5 ⊢ (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) → 𝑒 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
24		predss 6199	. . . . . . . . 9 ⊢ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴
25	24	a1i 11	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴)
26		snssi 4738	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐴 → {𝑎} ⊆ 𝐴)
27	25, 26	unssd 4116	. . . . . . 7 ⊢ (𝑎 ∈ 𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
28		predss 6199	. . . . . . . . 9 ⊢ Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵
29	28	a1i 11	. . . . . . . 8 ⊢ (𝑏 ∈ 𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵)
30		snssi 4738	. . . . . . . 8 ⊢ (𝑏 ∈ 𝐵 → {𝑏} ⊆ 𝐵)
31	29, 30	unssd 4116	. . . . . . 7 ⊢ (𝑏 ∈ 𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
32		xpss12 5595	. . . . . . 7 ⊢ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
33	27, 31, 32	syl2an 595	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
34	33	sseld 3916	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → 𝑒 ∈ (𝐴 × 𝐵)))
35	23, 34	syl5 34	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) → 𝑒 ∈ (𝐴 × 𝐵)))
36		elxp2 5604	. . . . 5 ⊢ (𝑒 ∈ (𝐴 × 𝐵) ↔ ∃𝑐 ∈ 𝐴 ∃𝑑 ∈ 𝐵 𝑒 = ⟨𝑐, 𝑑⟩)
37		opex 5373	. . . . . . . . 9 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
38		opex 5373	. . . . . . . . . 10 ⊢ ⟨𝑐, 𝑑⟩ ∈ V
39	38	elpred 6208	. . . . . . . . 9 ⊢ (⟨𝑎, 𝑏⟩ ∈ V → (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩)))
40	37, 39	ax-mp 5	. . . . . . . 8 ⊢ (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩))
41		opelxpi 5617	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) → ⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵))
42	41	adantl 481	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵))
43	42	biantrurd 532	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩ ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩)))
44		xpord2.1	. . . . . . . . . . 11 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥)𝑆(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}
45	44	xpord2lem 33716	. . . . . . . . . 10 ⊢ (⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩ ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
46		eldif 3893	. . . . . . . . . . . . 13 ⊢ (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩}))
47		opelxp 5616	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
48		elun 4079	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑐 ∈ {𝑎}))
49		vex 3426	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑐 ∈ V
50	49	elpred 6208	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ V → (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎)))
51	50	elv 3428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎))
52		velsn 4574	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ {𝑎} ↔ 𝑐 = 𝑎)
53	51, 52	orbi12i 911	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑐 ∈ {𝑎}) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎))
54	48, 53	bitri 274	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎))
55		elun 4079	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑑 ∈ {𝑏}))
56		vex 3426	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑑 ∈ V
57	56	elpred 6208	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ V → (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏)))
58	57	elv 3428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏))
59		velsn 4574	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ {𝑏} ↔ 𝑑 = 𝑏)
60	58, 59	orbi12i 911	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑑 ∈ {𝑏}) ↔ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏))
61	55, 60	bitri 274	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏))
62	54, 61	anbi12i 626	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
63	47, 62	bitri 274	. . . . . . . . . . . . . 14 ⊢ (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
64	38	elsn 4573	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
65	64	notbii 319	. . . . . . . . . . . . . . 15 ⊢ (¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ ¬ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
66		df-ne 2943	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑐, 𝑑⟩ ≠ ⟨𝑎, 𝑏⟩ ↔ ¬ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
67	49, 56	opthne 5391	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑐, 𝑑⟩ ≠ ⟨𝑎, 𝑏⟩ ↔ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))
68	65, 66, 67	3bitr2i 298	. . . . . . . . . . . . . 14 ⊢ (¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))
69	63, 68	anbi12i 626	. . . . . . . . . . . . 13 ⊢ ((⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩}) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))
70	46, 69	bitri 274	. . . . . . . . . . . 12 ⊢ (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))
71		simprl 767	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → 𝑐 ∈ 𝐴)
72	71	biantrurd 532	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (𝑐𝑅𝑎 ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎)))
73	72	orbi1d 913	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎)))
74		simprr 769	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → 𝑑 ∈ 𝐵)
75	74	biantrurd 532	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (𝑑𝑆𝑏 ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏)))
76	75	orbi1d 913	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ↔ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
77	73, 76	3anbi12d 1435	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
78		df-3an 1087	. . . . . . . . . . . . 13 ⊢ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))
79	77, 78	bitr2di 287	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
80	70, 79	syl5bb 282	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
81		pm3.22 459	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)))
82	81	biantrurd 532	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))))
83		df-3an 1087	. . . . . . . . . . . 12 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
84	82, 83	bitr4di 288	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))))
85	80, 84	bitr2d 279	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
86	45, 85	syl5bb 282	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
87	43, 86	bitr3d 280	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
88	40, 87	syl5bb 282	. . . . . . 7 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
89		eleq1 2826	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩)))
90		eleq1 2826	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
91	89, 90	bibi12d 345	. . . . . . 7 ⊢ (𝑒 = ⟨𝑐, 𝑑⟩ → ((𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})) ↔ (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
92	88, 91	syl5ibrcom 246	. . . . . 6 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
93	92	rexlimdvva 3222	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∃𝑐 ∈ 𝐴 ∃𝑑 ∈ 𝐵 𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
94	36, 93	syl5bi 241	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ (𝐴 × 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
95	22, 35, 94	pm5.21ndd 380	. . 3 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
96	95	eqrdv 2736	. 2 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))
97	10, 20, 96	vtocl2ga 3504	1 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 ∧ w3a 1085 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∃wrex 3064 Vcvv 3422 ∖ cdif 3880 ∪ cun 3881 ⊆ wss 3883 {csn 4558 ⟨cop 4564 class class class wbr 5070 {copab 5132 × cxp 5578 Predcpred 6190 ‘cfv 6418 1^st c1st 7802 2^nd c2nd 7803

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-iota 6376 df-fun 6420 df-fv 6426 df-1st 7804 df-2nd 7805

This theorem is referenced by: sexp2 33720 xpord2ind 33721 on2recsov 33754 noxpordpred 34037

W3C validator