xpord2pred - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > xpord2pred		Structured version Visualization version GIF version

Theorem xpord2pred 8170

Description: Calculate the predecessor class in frxp2 8169. (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 4873	. . . 4 ⊢ (𝑎 = 𝑋 → ⟨𝑎, 𝑏⟩ = ⟨𝑋, 𝑏⟩)
2		predeq3 6325	. . . 4 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑋, 𝑏⟩ → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩))
3	1, 2	syl 17	. . 3 ⊢ (𝑎 = 𝑋 → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩))
4		predeq3 6325	. . . . . 6 ⊢ (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋))
5		sneq 4636	. . . . . 6 ⊢ (𝑎 = 𝑋 → {𝑎} = {𝑋})
6	4, 5	uneq12d 4169	. . . . 5 ⊢ (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}))
7	6	xpeq1d 5714	. . . 4 ⊢ (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
8	1	sneqd 4638	. . . 4 ⊢ (𝑎 = 𝑋 → {⟨𝑎, 𝑏⟩} = {⟨𝑋, 𝑏⟩})
9	7, 8	difeq12d 4127	. . 3 ⊢ (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}))
10	3, 9	eqeq12d 2753	. 2 ⊢ (𝑎 = 𝑋 → (Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩})))
11		opeq2 4874	. . . 4 ⊢ (𝑏 = 𝑌 → ⟨𝑋, 𝑏⟩ = ⟨𝑋, 𝑌⟩)
12		predeq3 6325	. . . 4 ⊢ (⟨𝑋, 𝑏⟩ = ⟨𝑋, 𝑌⟩ → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩))
13	11, 12	syl 17	. . 3 ⊢ (𝑏 = 𝑌 → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩))
14		predeq3 6325	. . . . . 6 ⊢ (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌))
15		sneq 4636	. . . . . 6 ⊢ (𝑏 = 𝑌 → {𝑏} = {𝑌})
16	14, 15	uneq12d 4169	. . . . 5 ⊢ (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))
17	16	xpeq2d 5715	. . . 4 ⊢ (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})))
18	11	sneqd 4638	. . . 4 ⊢ (𝑏 = 𝑌 → {⟨𝑋, 𝑏⟩} = {⟨𝑋, 𝑌⟩})
19	17, 18	difeq12d 4127	. . 3 ⊢ (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))
20	13, 19	eqeq12d 2753	. 2 ⊢ (𝑏 = 𝑌 → (Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}) ↔ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩})))
21		predel 6342	. . . . 5 ⊢ (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝑒 ∈ (𝐴 × 𝐵))
22	21	a1i 11	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝑒 ∈ (𝐴 × 𝐵)))
23		eldifi 4131	. . . . 5 ⊢ (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) → 𝑒 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
24		predss 6329	. . . . . . . . 9 ⊢ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴
25	24	a1i 11	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴)
26		snssi 4808	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐴 → {𝑎} ⊆ 𝐴)
27	25, 26	unssd 4192	. . . . . . 7 ⊢ (𝑎 ∈ 𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
28		predss 6329	. . . . . . . . 9 ⊢ Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵
29	28	a1i 11	. . . . . . . 8 ⊢ (𝑏 ∈ 𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵)
30		snssi 4808	. . . . . . . 8 ⊢ (𝑏 ∈ 𝐵 → {𝑏} ⊆ 𝐵)
31	29, 30	unssd 4192	. . . . . . 7 ⊢ (𝑏 ∈ 𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
32		xpss12 5700	. . . . . . 7 ⊢ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
33	27, 31, 32	syl2an 596	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
34	33	sseld 3982	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → 𝑒 ∈ (𝐴 × 𝐵)))
35	23, 34	syl5 34	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) → 𝑒 ∈ (𝐴 × 𝐵)))
36		elxp2 5709	. . . . 5 ⊢ (𝑒 ∈ (𝐴 × 𝐵) ↔ ∃𝑐 ∈ 𝐴 ∃𝑑 ∈ 𝐵 𝑒 = ⟨𝑐, 𝑑⟩)
37		opex 5469	. . . . . . . . 9 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
38		opex 5469	. . . . . . . . . 10 ⊢ ⟨𝑐, 𝑑⟩ ∈ V
39	38	elpred 6338	. . . . . . . . 9 ⊢ (⟨𝑎, 𝑏⟩ ∈ V → (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩)))
40	37, 39	ax-mp 5	. . . . . . . 8 ⊢ (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩))
41		opelxpi 5722	. . . . . . . . . . 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 8167	. . . . . . . . . 10 ⊢ (⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩ ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
46		eldif 3961	. . . . . . . . . . . . 13 ⊢ (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩}))
47		opelxp 5721	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
48		elun 4153	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑐 ∈ {𝑎}))
49		vex 3484	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑐 ∈ V
50	49	elpred 6338	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ V → (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎)))
51	50	elv 3485	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎))
52		velsn 4642	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ {𝑎} ↔ 𝑐 = 𝑎)
53	51, 52	orbi12i 915	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑐 ∈ {𝑎}) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎))
54	48, 53	bitri 275	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎))
55		elun 4153	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑑 ∈ {𝑏}))
56		vex 3484	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑑 ∈ V
57	56	elpred 6338	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ V → (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏)))
58	57	elv 3485	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏))
59		velsn 4642	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ {𝑏} ↔ 𝑑 = 𝑏)
60	58, 59	orbi12i 915	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑑 ∈ {𝑏}) ↔ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏))
61	55, 60	bitri 275	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏))
62	54, 61	anbi12i 628	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
63	47, 62	bitri 275	. . . . . . . . . . . . . 14 ⊢ (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
64	38	elsn 4641	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
65	64	notbii 320	. . . . . . . . . . . . . . 15 ⊢ (¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ ¬ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
66		df-ne 2941	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑐, 𝑑⟩ ≠ ⟨𝑎, 𝑏⟩ ↔ ¬ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
67	49, 56	opthne 5487	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑐, 𝑑⟩ ≠ ⟨𝑎, 𝑏⟩ ↔ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))
68	65, 66, 67	3bitr2i 299	. . . . . . . . . . . . . 14 ⊢ (¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))
69	63, 68	anbi12i 628	. . . . . . . . . . . . 13 ⊢ ((⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩}) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))
70	46, 69	bitri 275	. . . . . . . . . . . 12 ⊢ (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))
71		simprl 771	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → 𝑐 ∈ 𝐴)
72	71	biantrurd 532	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (𝑐𝑅𝑎 ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎)))
73	72	orbi1d 917	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎)))
74		simprr 773	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → 𝑑 ∈ 𝐵)
75	74	biantrurd 532	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (𝑑𝑆𝑏 ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏)))
76	75	orbi1d 917	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ↔ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
77	73, 76	3anbi12d 1439	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
78		df-3an 1089	. . . . . . . . . . . . 13 ⊢ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))
79	77, 78	bitr2di 288	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
80	70, 79	bitrid 283	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
81		pm3.22 459	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)))
82	81	biantrurd 532	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))))
83		df-3an 1089	. . . . . . . . . . . 12 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
84	82, 83	bitr4di 289	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))))
85	80, 84	bitr2d 280	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
86	45, 85	bitrid 283	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
87	43, 86	bitr3d 281	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
88	40, 87	bitrid 283	. . . . . . 7 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
89		eleq1 2829	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩)))
90		eleq1 2829	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
91	89, 90	bibi12d 345	. . . . . . 7 ⊢ (𝑒 = ⟨𝑐, 𝑑⟩ → ((𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})) ↔ (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
92	88, 91	syl5ibrcom 247	. . . . . 6 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
93	92	rexlimdvva 3213	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∃𝑐 ∈ 𝐴 ∃𝑑 ∈ 𝐵 𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
94	36, 93	biimtrid 242	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ (𝐴 × 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
95	22, 35, 94	pm5.21ndd 379	. . 3 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
96	95	eqrdv 2735	. 2 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))
97	10, 20, 96	vtocl2ga 3578	1 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∃wrex 3070 Vcvv 3480 ∖ cdif 3948 ∪ cun 3949 ⊆ wss 3951 {csn 4626 ⟨cop 4632 class class class wbr 5143 {copab 5205 × cxp 5683 Predcpred 6320 ‘cfv 6561 1^st c1st 8012 2^nd c2nd 8013

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 ax-un 7755

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-iota 6514 df-fun 6563 df-fv 6569 df-1st 8014 df-2nd 8015

This theorem is referenced by: sexp2 8171 xpord2indlem 8172 on2recsov 8706 noxpordpred 27986

W3C validator