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 8077

Description: Calculate the predecessor class in frxp2 8076. (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 4830	. . . 4 ⊢ (𝑎 = 𝑋 → ⟨𝑎, 𝑏⟩ = ⟨𝑋, 𝑏⟩)
2		predeq3 6257	. . . 4 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝑋, 𝑏⟩ → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩))
3	1, 2	syl 17	. . 3 ⊢ (𝑎 = 𝑋 → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩))
4		predeq3 6257	. . . . . 6 ⊢ (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋))
5		sneq 4596	. . . . . 6 ⊢ (𝑎 = 𝑋 → {𝑎} = {𝑋})
6	4, 5	uneq12d 4124	. . . . 5 ⊢ (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}))
7	6	xpeq1d 5662	. . . 4 ⊢ (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
8	1	sneqd 4598	. . . 4 ⊢ (𝑎 = 𝑋 → {⟨𝑎, 𝑏⟩} = {⟨𝑋, 𝑏⟩})
9	7, 8	difeq12d 4083	. . 3 ⊢ (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}))
10	3, 9	eqeq12d 2752	. 2 ⊢ (𝑎 = 𝑋 → (Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩})))
11		opeq2 4831	. . . 4 ⊢ (𝑏 = 𝑌 → ⟨𝑋, 𝑏⟩ = ⟨𝑋, 𝑌⟩)
12		predeq3 6257	. . . 4 ⊢ (⟨𝑋, 𝑏⟩ = ⟨𝑋, 𝑌⟩ → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩))
13	11, 12	syl 17	. . 3 ⊢ (𝑏 = 𝑌 → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩))
14		predeq3 6257	. . . . . 6 ⊢ (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌))
15		sneq 4596	. . . . . 6 ⊢ (𝑏 = 𝑌 → {𝑏} = {𝑌})
16	14, 15	uneq12d 4124	. . . . 5 ⊢ (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))
17	16	xpeq2d 5663	. . . 4 ⊢ (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})))
18	11	sneqd 4598	. . . 4 ⊢ (𝑏 = 𝑌 → {⟨𝑋, 𝑏⟩} = {⟨𝑋, 𝑌⟩})
19	17, 18	difeq12d 4083	. . 3 ⊢ (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))
20	13, 19	eqeq12d 2752	. 2 ⊢ (𝑏 = 𝑌 → (Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}) ↔ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩})))
21		predel 6274	. . . . 5 ⊢ (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝑒 ∈ (𝐴 × 𝐵))
22	21	a1i 11	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝑒 ∈ (𝐴 × 𝐵)))
23		eldifi 4086	. . . . 5 ⊢ (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) → 𝑒 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
24		predss 6261	. . . . . . . . 9 ⊢ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴
25	24	a1i 11	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴)
26		snssi 4768	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐴 → {𝑎} ⊆ 𝐴)
27	25, 26	unssd 4146	. . . . . . 7 ⊢ (𝑎 ∈ 𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
28		predss 6261	. . . . . . . . 9 ⊢ Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵
29	28	a1i 11	. . . . . . . 8 ⊢ (𝑏 ∈ 𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵)
30		snssi 4768	. . . . . . . 8 ⊢ (𝑏 ∈ 𝐵 → {𝑏} ⊆ 𝐵)
31	29, 30	unssd 4146	. . . . . . 7 ⊢ (𝑏 ∈ 𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
32		xpss12 5648	. . . . . . 7 ⊢ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
33	27, 31, 32	syl2an 596	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
34	33	sseld 3943	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → 𝑒 ∈ (𝐴 × 𝐵)))
35	23, 34	syl5 34	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) → 𝑒 ∈ (𝐴 × 𝐵)))
36		elxp2 5657	. . . . 5 ⊢ (𝑒 ∈ (𝐴 × 𝐵) ↔ ∃𝑐 ∈ 𝐴 ∃𝑑 ∈ 𝐵 𝑒 = ⟨𝑐, 𝑑⟩)
37		opex 5421	. . . . . . . . 9 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
38		opex 5421	. . . . . . . . . 10 ⊢ ⟨𝑐, 𝑑⟩ ∈ V
39	38	elpred 6270	. . . . . . . . 9 ⊢ (⟨𝑎, 𝑏⟩ ∈ V → (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩)))
40	37, 39	ax-mp 5	. . . . . . . 8 ⊢ (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩))
41		opelxpi 5670	. . . . . . . . . . 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 8074	. . . . . . . . . 10 ⊢ (⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩ ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
46		eldif 3920	. . . . . . . . . . . . 13 ⊢ (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩}))
47		opelxp 5669	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
48		elun 4108	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑐 ∈ {𝑎}))
49		vex 3449	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑐 ∈ V
50	49	elpred 6270	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ V → (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎)))
51	50	elv 3451	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎))
52		velsn 4602	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 ∈ {𝑎} ↔ 𝑐 = 𝑎)
53	51, 52	orbi12i 913	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑐 ∈ {𝑎}) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎))
54	48, 53	bitri 274	. . . . . . . . . . . . . . . 16 ⊢ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎))
55		elun 4108	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑑 ∈ {𝑏}))
56		vex 3449	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑑 ∈ V
57	56	elpred 6270	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ V → (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏)))
58	57	elv 3451	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏))
59		velsn 4602	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ {𝑏} ↔ 𝑑 = 𝑏)
60	58, 59	orbi12i 913	. . . . . . . . . . . . . . . . 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 4601	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
65	64	notbii 319	. . . . . . . . . . . . . . 15 ⊢ (¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ ¬ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
66		df-ne 2944	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑐, 𝑑⟩ ≠ ⟨𝑎, 𝑏⟩ ↔ ¬ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
67	49, 56	opthne 5439	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑐, 𝑑⟩ ≠ ⟨𝑎, 𝑏⟩ ↔ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))
68	65, 66, 67	3bitr2i 298	. . . . . . . . . . . . . 14 ⊢ (¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))
69	63, 68	anbi12i 627	. . . . . . . . . . . . 13 ⊢ ((⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩}) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))
70	46, 69	bitri 274	. . . . . . . . . . . 12 ⊢ (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))
71		simprl 769	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → 𝑐 ∈ 𝐴)
72	71	biantrurd 533	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (𝑐𝑅𝑎 ↔ (𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎)))
73	72	orbi1d 915	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎)))
74		simprr 771	. . . . . . . . . . . . . . . 16 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → 𝑑 ∈ 𝐵)
75	74	biantrurd 533	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (𝑑𝑆𝑏 ↔ (𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏)))
76	75	orbi1d 915	. . . . . . . . . . . . . 14 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ↔ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
77	73, 76	3anbi12d 1437	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
78		df-3an 1089	. . . . . . . . . . . . 13 ⊢ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))
79	77, 78	bitr2di 287	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((((𝑐 ∈ 𝐴 ∧ 𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑 ∈ 𝐵 ∧ 𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
80	70, 79	bitrid 282	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
81		pm3.22 460	. . . . . . . . . . . . 13 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)))
82	81	biantrurd 533	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))))
83		df-3an 1089	. . . . . . . . . . . 12 ⊢ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) ↔ (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))))
84	82, 83	bitr4di 288	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)) ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏)))))
85	80, 84	bitr2d 279	. . . . . . . . . 10 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ ((𝑐𝑅𝑎 ∨ 𝑐 = 𝑎) ∧ (𝑑𝑆𝑏 ∨ 𝑑 = 𝑏) ∧ (𝑐 ≠ 𝑎 ∨ 𝑑 ≠ 𝑏))) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
86	45, 85	bitrid 282	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
87	43, 86	bitr3d 280	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
88	40, 87	bitrid 282	. . . . . . 7 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
89		eleq1 2825	. . . . . . . 8 ⊢ (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩)))
90		eleq1 2825	. . . . . . . 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 3205	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (∃𝑐 ∈ 𝐴 ∃𝑑 ∈ 𝐵 𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
94	36, 93	biimtrid 241	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ (𝐴 × 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
95	22, 35, 94	pm5.21ndd 380	. . 3 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
96	95	eqrdv 2734	. 2 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))
97	10, 20, 96	vtocl2ga 3535	1 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 845 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ≠ wne 2943 ∃wrex 3073 Vcvv 3445 ∖ cdif 3907 ∪ cun 3908 ⊆ wss 3910 {csn 4586 ⟨cop 4592 class class class wbr 5105 {copab 5167 × cxp 5631 Predcpred 6252 ‘cfv 6496 1^st c1st 7919 2^nd c2nd 7920

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 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 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384 ax-un 7672

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-rn 5644 df-res 5645 df-ima 5646 df-pred 6253 df-iota 6448 df-fun 6498 df-fv 6504 df-1st 7921 df-2nd 7922

This theorem is referenced by: sexp2 8078 xpord2indlem 8079 on2recsov 8614 noxpordpred 27265

W3C validator