xpord3pred - Metamath Proof Explorer

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

Theorem xpord3pred 8178

Description: Calculate the predecsessor class for the triple order. (Contributed by Scott Fenton, 31-Jan-2025.)

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

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

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

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

Step	Hyp	Ref	Expression
1		oteq1 4881	. . . 4 ⊢ (𝑎 = 𝑋 → ⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑏, 𝑐⟩)
2		predeq3 6324	. . . 4 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑏, 𝑐⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩))
3	1, 2	syl 17	. . 3 ⊢ (𝑎 = 𝑋 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩))
4		predeq3 6324	. . . . . . 7 ⊢ (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋))
5		sneq 4635	. . . . . . 7 ⊢ (𝑎 = 𝑋 → {𝑎} = {𝑋})
6	4, 5	uneq12d 4168	. . . . . 6 ⊢ (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}))
7	6	xpeq1d 5713	. . . . 5 ⊢ (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
8	7	xpeq1d 5713	. . . 4 ⊢ (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
9	1	sneqd 4637	. . . 4 ⊢ (𝑎 = 𝑋 → {⟨𝑎, 𝑏, 𝑐⟩} = {⟨𝑋, 𝑏, 𝑐⟩})
10	8, 9	difeq12d 4126	. . 3 ⊢ (𝑎 = 𝑋 → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}))
11	3, 10	eqeq12d 2752	. 2 ⊢ (𝑎 = 𝑋 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩})))
12		oteq2 4882	. . . 4 ⊢ (𝑏 = 𝑌 → ⟨𝑋, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑐⟩)
13		predeq3 6324	. . . 4 ⊢ (⟨𝑋, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑐⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩))
14	12, 13	syl 17	. . 3 ⊢ (𝑏 = 𝑌 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩))
15		predeq3 6324	. . . . . . 7 ⊢ (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌))
16		sneq 4635	. . . . . . 7 ⊢ (𝑏 = 𝑌 → {𝑏} = {𝑌})
17	15, 16	uneq12d 4168	. . . . . 6 ⊢ (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))
18	17	xpeq2d 5714	. . . . 5 ⊢ (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})))
19	18	xpeq1d 5713	. . . 4 ⊢ (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
20	12	sneqd 4637	. . . 4 ⊢ (𝑏 = 𝑌 → {⟨𝑋, 𝑏, 𝑐⟩} = {⟨𝑋, 𝑌, 𝑐⟩})
21	19, 20	difeq12d 4126	. . 3 ⊢ (𝑏 = 𝑌 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}))
22	14, 21	eqeq12d 2752	. 2 ⊢ (𝑏 = 𝑌 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩})))
23		oteq3 4883	. . . 4 ⊢ (𝑐 = 𝑍 → ⟨𝑋, 𝑌, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑍⟩)
24		predeq3 6324	. . . 4 ⊢ (⟨𝑋, 𝑌, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑍⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩))
25	23, 24	syl 17	. . 3 ⊢ (𝑐 = 𝑍 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩))
26		predeq3 6324	. . . . . 6 ⊢ (𝑐 = 𝑍 → Pred(𝑇, 𝐶, 𝑐) = Pred(𝑇, 𝐶, 𝑍))
27		sneq 4635	. . . . . 6 ⊢ (𝑐 = 𝑍 → {𝑐} = {𝑍})
28	26, 27	uneq12d 4168	. . . . 5 ⊢ (𝑐 = 𝑍 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) = (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍}))
29	28	xpeq2d 5714	. . . 4 ⊢ (𝑐 = 𝑍 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})))
30	23	sneqd 4637	. . . 4 ⊢ (𝑐 = 𝑍 → {⟨𝑋, 𝑌, 𝑐⟩} = {⟨𝑋, 𝑌, 𝑍⟩})
31	29, 30	difeq12d 4126	. . 3 ⊢ (𝑐 = 𝑍 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩}))
32	25, 31	eqeq12d 2752	. 2 ⊢ (𝑐 = 𝑍 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩})))
33		el2xptp 8061	. . . . . . 7 ⊢ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩)
34		df-3an 1088	. . . . . . . . . . 11 ⊢ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
35		simplrl 776	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → 𝑑 ∈ 𝐴)
36		simplrr 777	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → 𝑒 ∈ 𝐵)
37		simpr 484	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → 𝑓 ∈ 𝐶)
38	35, 36, 37	3jca 1128	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶))
39		simpll 766	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))
40	38, 39	jca 511	. . . . . . . . . . . . 13 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
41	40	biantrurd 532	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))))
42	35	biantrurd 532	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑑𝑅𝑎 ↔ (𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎)))
43	42	orbi1d 916	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ↔ ((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎)))
44	36	biantrurd 532	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑒𝑆𝑏 ↔ (𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏)))
45	44	orbi1d 916	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ↔ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)))
46	37	biantrurd 532	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑓𝑇𝑐 ↔ (𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐)))
47	46	orbi1d 916	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((𝑓𝑇𝑐 ∨ 𝑓 = 𝑐) ↔ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
48	43, 45, 47	3anbi123d 1437	. . . . . . . . . . . . 13 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))))
49	48	anbi1d 631	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
50	41, 49	bitr3d 281	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
51	34, 50	bitrid 283	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
52		breq1 5145	. . . . . . . . . . . 12 ⊢ (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ ⟨𝑑, 𝑒, 𝑓⟩𝑈⟨𝑎, 𝑏, 𝑐⟩))
53		xpord3.1	. . . . . . . . . . . . 13 ⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1^st ‘(1^st ‘𝑥))𝑅(1^st ‘(1^st ‘𝑦)) ∨ (1^st ‘(1^st ‘𝑥)) = (1^st ‘(1^st ‘𝑦))) ∧ ((2^nd ‘(1^st ‘𝑥))𝑆(2^nd ‘(1^st ‘𝑦)) ∨ (2^nd ‘(1^st ‘𝑥)) = (2^nd ‘(1^st ‘𝑦))) ∧ ((2^nd ‘𝑥)𝑇(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}
54	53	xpord3lem 8175	. . . . . . . . . . . 12 ⊢ (⟨𝑑, 𝑒, 𝑓⟩𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
55	52, 54	bitrdi 287	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))))
56		eleq1 2828	. . . . . . . . . . . 12 ⊢ (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
57		eldifsn 4785	. . . . . . . . . . . . 13 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩))
58		otelxp 5728	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
59		elun 4152	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}))
60		vex 3483	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑑 ∈ V
61	60	elpred 6337	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ V → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎)))
62	61	elv 3484	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎))
63		velsn 4641	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ {𝑎} ↔ 𝑑 = 𝑎)
64	62, 63	orbi12i 914	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}) ↔ ((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))
65	59, 64	bitri 275	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))
66		elun 4152	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}))
67		vex 3483	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑒 ∈ V
68	67	elpred 6337	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ V → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏)))
69	68	elv 3484	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏))
70		velsn 4641	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 ∈ {𝑏} ↔ 𝑒 = 𝑏)
71	69, 70	orbi12i 914	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}) ↔ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))
72	66, 71	bitri 275	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))
73		elun 4152	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐}))
74		vex 3483	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑓 ∈ V
75	74	elpred 6337	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ V → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐)))
76	75	elv 3484	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐))
77		velsn 4641	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ {𝑐} ↔ 𝑓 = 𝑐)
78	76, 77	orbi12i 914	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐}) ↔ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))
79	73, 78	bitri 275	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))
80	65, 72, 79	3anbi123i 1155	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
81	58, 80	bitri 275	. . . . . . . . . . . . . 14 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
82	60, 67, 74	otthne 5490	. . . . . . . . . . . . . 14 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩ ↔ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
83	81, 82	anbi12i 628	. . . . . . . . . . . . 13 ⊢ ((⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
84	57, 83	bitri 275	. . . . . . . . . . . 12 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
85	56, 84	bitrdi 287	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
86	55, 85	bibi12d 345	. . . . . . . . . 10 ⊢ (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))))
87	51, 86	syl5ibrcom 247	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
88	87	rexlimdva 3154	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) → (∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
89	88	rexlimdvva 3212	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
90	33, 89	biimtrid 242	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
91	90	pm5.32d 577	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
92		otex 5469	. . . . . 6 ⊢ ⟨𝑎, 𝑏, 𝑐⟩ ∈ V
93		vex 3483	. . . . . . 7 ⊢ 𝑞 ∈ V
94	93	elpred 6337	. . . . . 6 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ ∈ V → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩)))
95	92, 94	ax-mp 5	. . . . 5 ⊢ (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩))
96		elin 3966	. . . . 5 ⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
97	91, 95, 96	3bitr4g 314	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
98	97	eqrdv 2734	. . 3 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
99		predss 6328	. . . . . . . . . 10 ⊢ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴
100	99	a1i 11	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴)
101		snssi 4807	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐴 → {𝑎} ⊆ 𝐴)
102	100, 101	unssd 4191	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
103	102	3ad2ant1 1133	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
104		predss 6328	. . . . . . . . . 10 ⊢ Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵
105	104	a1i 11	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵)
106		snssi 4807	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝐵 → {𝑏} ⊆ 𝐵)
107	105, 106	unssd 4191	. . . . . . . 8 ⊢ (𝑏 ∈ 𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
108	107	3ad2ant2 1134	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
109		xpss12 5699	. . . . . . 7 ⊢ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
110	103, 108, 109	syl2anc 584	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
111		predss 6328	. . . . . . . . 9 ⊢ Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶
112	111	a1i 11	. . . . . . . 8 ⊢ (𝑐 ∈ 𝐶 → Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶)
113		snssi 4807	. . . . . . . 8 ⊢ (𝑐 ∈ 𝐶 → {𝑐} ⊆ 𝐶)
114	112, 113	unssd 4191	. . . . . . 7 ⊢ (𝑐 ∈ 𝐶 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶)
115	114	3ad2ant3 1135	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶)
116		xpss12 5699	. . . . . 6 ⊢ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵) ∧ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶))
117	110, 115, 116	syl2anc 584	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶))
118	117	ssdifssd 4146	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ⊆ ((𝐴 × 𝐵) × 𝐶))
119		sseqin2 4222	. . . 4 ⊢ (((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
120	118, 119	sylib 218	. . 3 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
121	98, 120	eqtrd 2776	. 2 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
122	11, 22, 32, 121	vtocl3ga 3582	1 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩}))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 ∨ w3o 1085 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ≠ wne 2939 ∃wrex 3069 Vcvv 3479 ∖ cdif 3947 ∪ cun 3948 ∩ cin 3949 ⊆ wss 3950 {csn 4625 ⟨cotp 4633 class class class wbr 5142 {copab 5204 × cxp 5682 Predcpred 6319 ‘cfv 6560 1^st c1st 8013 2^nd c2nd 8014

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2707 ax-sep 5295 ax-nul 5305 ax-pr 5431 ax-un 7756

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2728 df-clel 2815 df-nfc 2891 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3436 df-v 3481 df-sbc 3788 df-csb 3899 df-dif 3953 df-un 3955 df-in 3957 df-ss 3967 df-nul 4333 df-if 4525 df-sn 4626 df-pr 4628 df-op 4632 df-ot 4634 df-uni 4907 df-iun 4992 df-br 5143 df-opab 5205 df-mpt 5225 df-id 5577 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6320 df-iota 6513 df-fun 6562 df-fv 6568 df-1st 8015 df-2nd 8016

This theorem is referenced by: sexp3 8179 xpord3inddlem 8180

W3C validator