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 8119

Description: Calculate the predecessor class in frxp2 8118. (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 4828	. . . 4 ⊢ (𝑎 = 𝑋 → ⟨𝑎, 𝑏⟩ = ⟨𝑋, 𝑏⟩)
2		predeq3 6287	. . . 4 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑋, 𝑏⟩ → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩))
3	1, 2	syl 17	. . 3 ⊢ (𝑎 = 𝑋 → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩))
4		predeq3 6287	. . . . . 6 ⊢ (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋))
5		sneq 4589	. . . . . 6 ⊢ (𝑎 = 𝑋 → {𝑎} = {𝑋})
6	4, 5	uneq12d 4120	. . . . 5 ⊢ (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}))
7	6	xpeq1d 5672	. . . 4 ⊢ (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
8	1	sneqd 4591	. . . 4 ⊢ (𝑎 = 𝑋 → {⟨𝑎, 𝑏⟩} = {⟨𝑋, 𝑏⟩})
9	7, 8	difeq12d 4079	. . 3 ⊢ (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}))
10	3, 9	eqeq12d 2777	. 2 ⊢ (𝑎 = 𝑋 → (Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩})))
11		opeq2 4829	. . . 4 ⊢ (𝑏 = 𝑌 → ⟨𝑋, 𝑏⟩ = ⟨𝑋, 𝑌⟩)
12		predeq3 6287	. . . 4 ⊢ (⟨𝑋, 𝑏⟩ = ⟨𝑋, 𝑌⟩ → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩))
13	11, 12	syl 17	. . 3 ⊢ (𝑏 = 𝑌 → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩))
14		predeq3 6287	. . . . . 6 ⊢ (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌))
15		sneq 4589	. . . . . 6 ⊢ (𝑏 = 𝑌 → {𝑏} = {𝑌})
16	14, 15	uneq12d 4120	. . . . 5 ⊢ (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))
17	16	xpeq2d 5673	. . . 4 ⊢ (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})))
18	11	sneqd 4591	. . . 4 ⊢ (𝑏 = 𝑌 → {⟨𝑋, 𝑏⟩} = {⟨𝑋, 𝑌⟩})
19	17, 18	difeq12d 4079	. . 3 ⊢ (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))
20	13, 19	eqeq12d 2777	. 2 ⊢ (𝑏 = 𝑌 → (Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}) ↔ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩})))
21		predel 6303	. . . . 5 ⊢ (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝑒 ∈ (𝐴 × 𝐵))
22	21	a1i 11	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝑒 ∈ (𝐴 × 𝐵)))
23		eldifi 4082	. . . . 5 ⊢ (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) → 𝑒 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
24		predss 6291	. . . . . . . . 9 ⊢ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴
25	24	a1i 11	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴)
26		snssi 4741	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐴 → {𝑎} ⊆ 𝐴)
27	25, 26	unssd 4142	. . . . . . 7 ⊢ (𝑎 ∈ 𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
28		predss 6291	. . . . . . . . 9 ⊢ Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵
29	28	a1i 11	. . . . . . . 8 ⊢ (𝑏 ∈ 𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵)
30		snssi 4741	. . . . . . . 8 ⊢ (𝑏 ∈ 𝐵 → {𝑏} ⊆ 𝐵)
31	29, 30	unssd 4142	. . . . . . 7 ⊢ (𝑏 ∈ 𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
32		xpss12 5658	. . . . . . 7 ⊢ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
33	27, 31, 32	syl2an 605	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
34	33	sseld 3933	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → 𝑒 ∈ (𝐴 × 𝐵)))
35	23, 34	syl5 34	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) → 𝑒 ∈ (𝐴 × 𝐵)))
36		elxp2 5667	. . . . 5 ⊢ (𝑒 ∈ (𝐴 × 𝐵) ↔ ∃𝑐 ∈ 𝐴 ∃𝑑 ∈ 𝐵 𝑒 = ⟨𝑐, 𝑑⟩)
37		opex 5428	. . . . . . . . 9 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
38		opex 5428	. . . . . . . . . 10 ⊢ ⟨𝑐, 𝑑⟩ ∈ V
39	38	elpred 6300	. . . . . . . . 9 ⊢ (⟨𝑎, 𝑏⟩ ∈ V → (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩)))
40	37, 39	ax-mp 5	. . . . . . . 8 ⊢ (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩))
41		opelxpi 5680	. . . . . . . . . . 11 ⊢ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) → ⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵))
42	41	adantl 485	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵))
43	42	biantrurd 540	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩ ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩)))
44		xpord2.1	. . . . . . . . . . 11 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥)𝑆(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}
45	44	xpord2lem 8116	. . . . . . . . . 10 ⊢ (⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩ ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
46		eldif 3912	. . . . . . . . . . . . 13 ⊢ (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩}))
47		opelxp 5679	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
48		elun 4104	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑐 ∈ {𝑎}))
49		vex 3457	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑐 ∈ V
50	49	elpred 6300	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ V → (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎)))
51	50	elv 3458	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎))
52		velsn 4595	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ {𝑎} ↔ 𝑐 = 𝑎)
53	51, 52	orbi12i 925	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑐 ∈ {𝑎}) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎))
54	48, 53	bitri 277	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎))
55		elun 4104	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑑 ∈ {𝑏}))
56		vex 3457	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑑 ∈ V
57	56	elpred 6300	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ V → (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏)))
58	57	elv 3458	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏))
59		velsn 4595	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ {𝑏} ↔ 𝑑 = 𝑏)
60	58, 59	orbi12i 925	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑑 ∈ {𝑏}) ↔ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏))
61	55, 60	bitri 277	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏))
62	54, 61	anbi12i 637	. . . . . . . . . . . . . . 15 ⊢ ((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
63	47, 62	bitri 277	. . . . . . . . . . . . . 14 ⊢ (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
64	38	elsn 4594	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
65	64	notbii 322	. . . . . . . . . . . . . . 15 ⊢ (¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ ¬ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
66		df-ne 2957	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑐, 𝑑⟩ ≠ ⟨𝑎, 𝑏⟩ ↔ ¬ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
67	49, 56	opthne 5447	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑐, 𝑑⟩ ≠ ⟨𝑎, 𝑏⟩ ↔ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))
68	65, 66, 67	3bitr2i 301	. . . . . . . . . . . . . 14 ⊢ (¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))
69	63, 68	anbi12i 637	. . . . . . . . . . . . 13 ⊢ ((⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩}) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))
70	46, 69	bitri 277	. . . . . . . . . . . 12 ⊢ (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))
71		simprl 780	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → 𝑐 ∈ 𝐴)
72	71	biantrurd 540	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (𝑐𝑅𝑎 ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎)))
73	72	orbi1d 927	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎)))
74		simprr 782	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → 𝑑 ∈ 𝐵)
75	74	biantrurd 540	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (𝑑𝑆𝑏 ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏)))
76	75	orbi1d 927	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ↔ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
77	73, 76	3anbi12d 1457	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
78		df-3an 1099	. . . . . . . . . . . . 13 ⊢ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))
79	77, 78	bitr2di 290	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
80	70, 79	bitrid 285	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
81		pm3.22 463	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)))
82	81	biantrurd 540	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))))
83		df-3an 1099	. . . . . . . . . . . 12 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
84	82, 83	bitr4di 291	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))))
85	80, 84	bitr2d 282	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
86	45, 85	bitrid 285	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
87	43, 86	bitr3d 283	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
88	40, 87	bitrid 285	. . . . . . 7 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
89		eleq1 2849	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩)))
90		eleq1 2849	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
91	89, 90	bibi12d 347	. . . . . . 7 ⊢ (𝑒 = ⟨𝑐, 𝑑⟩ → ((𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})) ↔ (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
92	88, 91	syl5ibrcom 249	. . . . . 6 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
93	92	rexlimdvva 3218	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∃𝑐 ∈ 𝐴 ∃𝑑 ∈ 𝐵 𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
94	36, 93	biimtrid 244	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ (𝐴 × 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
95	22, 35, 94	pm5.21ndd 381	. . 3 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
96	95	eqrdv 2759	. 2 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))
97	10, 20, 96	vtocl2ga 3541	1 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 ∃wrex 3085 Vcvv 3453 ∖ cdif 3899 ∪ cun 3900 ⊆ wss 3902 {csn 4579 ⟨cop 4585 class class class wbr 5097 {copab 5159 × cxp 5641 Predcpred 6282 ‘cfv 6516 1^st c1st 7963 2^nd c2nd 7964

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5243 ax-nul 5253 ax-pr 5387 ax-un 7713

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3076 df-rex 3086 df-rab 3414 df-v 3455 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-nul 4284 df-if 4478 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-br 5098 df-opab 5160 df-mpt 5179 df-id 5538 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-iota 6472 df-fun 6518 df-fv 6524 df-1st 7965 df-2nd 7966

This theorem is referenced by: sexp2 8120 xpord2indlem 8121 on2recsov 8632 noxpordpred 28034

W3C validator