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 8126

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 4837	. . . 4 ⊢ (𝑎 = 𝑋 → ⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑏, 𝑐⟩)
2		predeq3 6287	. . . 4 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑏, 𝑐⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩))
3	1, 2	syl 17	. . 3 ⊢ (𝑎 = 𝑋 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩))
4		predeq3 6287	. . . . . . 7 ⊢ (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋))
5		sneq 4589	. . . . . . 7 ⊢ (𝑎 = 𝑋 → {𝑎} = {𝑋})
6	4, 5	uneq12d 4120	. . . . . 6 ⊢ (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}))
7	6	xpeq1d 5672	. . . . 5 ⊢ (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
8	7	xpeq1d 5672	. . . 4 ⊢ (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
9	1	sneqd 4591	. . . 4 ⊢ (𝑎 = 𝑋 → {⟨𝑎, 𝑏, 𝑐⟩} = {⟨𝑋, 𝑏, 𝑐⟩})
10	8, 9	difeq12d 4079	. . 3 ⊢ (𝑎 = 𝑋 → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}))
11	3, 10	eqeq12d 2777	. 2 ⊢ (𝑎 = 𝑋 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩})))
12		oteq2 4838	. . . 4 ⊢ (𝑏 = 𝑌 → ⟨𝑋, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑐⟩)
13		predeq3 6287	. . . 4 ⊢ (⟨𝑋, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑐⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩))
14	12, 13	syl 17	. . 3 ⊢ (𝑏 = 𝑌 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩))
15		predeq3 6287	. . . . . . 7 ⊢ (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌))
16		sneq 4589	. . . . . . 7 ⊢ (𝑏 = 𝑌 → {𝑏} = {𝑌})
17	15, 16	uneq12d 4120	. . . . . 6 ⊢ (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))
18	17	xpeq2d 5673	. . . . 5 ⊢ (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})))
19	18	xpeq1d 5672	. . . 4 ⊢ (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
20	12	sneqd 4591	. . . 4 ⊢ (𝑏 = 𝑌 → {⟨𝑋, 𝑏, 𝑐⟩} = {⟨𝑋, 𝑌, 𝑐⟩})
21	19, 20	difeq12d 4079	. . 3 ⊢ (𝑏 = 𝑌 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}))
22	14, 21	eqeq12d 2777	. 2 ⊢ (𝑏 = 𝑌 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩})))
23		oteq3 4839	. . . 4 ⊢ (𝑐 = 𝑍 → ⟨𝑋, 𝑌, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑍⟩)
24		predeq3 6287	. . . 4 ⊢ (⟨𝑋, 𝑌, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑍⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩))
25	23, 24	syl 17	. . 3 ⊢ (𝑐 = 𝑍 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩))
26		predeq3 6287	. . . . . 6 ⊢ (𝑐 = 𝑍 → Pred(𝑇, 𝐶, 𝑐) = Pred(𝑇, 𝐶, 𝑍))
27		sneq 4589	. . . . . 6 ⊢ (𝑐 = 𝑍 → {𝑐} = {𝑍})
28	26, 27	uneq12d 4120	. . . . 5 ⊢ (𝑐 = 𝑍 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) = (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍}))
29	28	xpeq2d 5673	. . . 4 ⊢ (𝑐 = 𝑍 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})))
30	23	sneqd 4591	. . . 4 ⊢ (𝑐 = 𝑍 → {⟨𝑋, 𝑌, 𝑐⟩} = {⟨𝑋, 𝑌, 𝑍⟩})
31	29, 30	difeq12d 4079	. . 3 ⊢ (𝑐 = 𝑍 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩}))
32	25, 31	eqeq12d 2777	. 2 ⊢ (𝑐 = 𝑍 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩})))
33		el2xptp 8011	. . . . . . 7 ⊢ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩)
34		df-3an 1099	. . . . . . . . . . 11 ⊢ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
35		simplrl 786	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → 𝑑 ∈ 𝐴)
36		simplrr 787	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → 𝑒 ∈ 𝐵)
37		simpr 488	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → 𝑓 ∈ 𝐶)
38	35, 36, 37	3jca 1140	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶))
39		simpll 776	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))
40	38, 39	jca 519	. . . . . . . . . . . . 13 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)))
41	40	biantrurd 540	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))))
42	35	biantrurd 540	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑑𝑅𝑎 ↔ (𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎)))
43	42	orbi1d 927	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ↔ ((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎)))
44	36	biantrurd 540	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑒𝑆𝑏 ↔ (𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏)))
45	44	orbi1d 927	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ↔ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)))
46	37	biantrurd 540	. . . . . . . . . . . . . . 15 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑓𝑇𝑐 ↔ (𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐)))
47	46	orbi1d 927	. . . . . . . . . . . . . 14 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((𝑓𝑇𝑐 ∨ 𝑓 = 𝑐) ↔ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
48	43, 45, 47	3anbi123d 1456	. . . . . . . . . . . . 13 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))))
49	48	anbi1d 640	. . . . . . . . . . . 12 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
50	41, 49	bitr3d 283	. . . . . . . . . . 11 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶)) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
51	34, 50	bitrid 285	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
52		breq1 5100	. . . . . . . . . . . 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 8123	. . . . . . . . . . . 12 ⊢ (⟨𝑑, 𝑒, 𝑓⟩𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
55	52, 54	bitrdi 289	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))))
56		eleq1 2849	. . . . . . . . . . . 12 ⊢ (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
57		eldifsn 4743	. . . . . . . . . . . . 13 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩))
58		otelxp 5687	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
59		elun 4104	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}))
60		vex 3457	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑑 ∈ V
61	60	elpred 6300	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 ∈ V → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎)))
62	61	elv 3458	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎))
63		velsn 4595	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ {𝑎} ↔ 𝑑 = 𝑎)
64	62, 63	orbi12i 925	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}) ↔ ((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))
65	59, 64	bitri 277	. . . . . . . . . . . . . . . 16 ⊢ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))
66		elun 4104	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}))
67		vex 3457	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑒 ∈ V
68	67	elpred 6300	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑏 ∈ V → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏)))
69	68	elv 3458	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏))
70		velsn 4595	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑒 ∈ {𝑏} ↔ 𝑒 = 𝑏)
71	69, 70	orbi12i 925	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}) ↔ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))
72	66, 71	bitri 277	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))
73		elun 4104	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐}))
74		vex 3457	. . . . . . . . . . . . . . . . . . . 20 ⊢ 𝑓 ∈ V
75	74	elpred 6300	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 ∈ V → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐)))
76	75	elv 3458	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐))
77		velsn 4595	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑓 ∈ {𝑐} ↔ 𝑓 = 𝑐)
78	76, 77	orbi12i 925	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐}) ↔ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))
79	73, 78	bitri 277	. . . . . . . . . . . . . . . 16 ⊢ (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))
80	65, 72, 79	3anbi123i 1167	. . . . . . . . . . . . . . 15 ⊢ ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
81	58, 80	bitri 277	. . . . . . . . . . . . . 14 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
82	60, 67, 74	otthne 5451	. . . . . . . . . . . . . 14 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩ ↔ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))
83	81, 82	anbi12i 637	. . . . . . . . . . . . 13 ⊢ ((⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
84	57, 83	bitri 277	. . . . . . . . . . . 12 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))
85	56, 84	bitrdi 289	. . . . . . . . . . 11 ⊢ (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))))
86	55, 85	bibi12d 347	. . . . . . . . . 10 ⊢ (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑑𝑅𝑎 ∨ 𝑑 = 𝑎) ∧ (𝑒𝑆𝑏 ∨ 𝑒 = 𝑏) ∧ (𝑓𝑇𝑐 ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐))) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒 ∈ 𝐵 ∧ 𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓 ∈ 𝐶 ∧ 𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐)))))
87	51, 86	syl5ibrcom 249	. . . . . . . . 9 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) ∧ 𝑓 ∈ 𝐶) → (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
88	87	rexlimdva 3162	. . . . . . . 8 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵)) → (∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
89	88	rexlimdvva 3218	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
90	33, 89	biimtrid 244	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
91	90	pm5.32d 585	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
92		otex 5430	. . . . . 6 ⊢ ⟨𝑎, 𝑏, 𝑐⟩ ∈ V
93		vex 3457	. . . . . . 7 ⊢ 𝑞 ∈ V
94	93	elpred 6300	. . . . . 6 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ ∈ V → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩)))
95	92, 94	ax-mp 5	. . . . 5 ⊢ (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈⟨𝑎, 𝑏, 𝑐⟩))
96		elin 3918	. . . . 5 ⊢ (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
97	91, 95, 96	3bitr4g 316	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
98	97	eqrdv 2759	. . 3 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
99		predss 6291	. . . . . . . . . 10 ⊢ Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴
100	99	a1i 11	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴)
101		snssi 4741	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐴 → {𝑎} ⊆ 𝐴)
102	100, 101	unssd 4142	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
103	102	3ad2ant1 1145	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
104		predss 6291	. . . . . . . . . 10 ⊢ Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵
105	104	a1i 11	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵)
106		snssi 4741	. . . . . . . . 9 ⊢ (𝑏 ∈ 𝐵 → {𝑏} ⊆ 𝐵)
107	105, 106	unssd 4142	. . . . . . . 8 ⊢ (𝑏 ∈ 𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
108	107	3ad2ant2 1146	. . . . . . 7 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
109		xpss12 5658	. . . . . . 7 ⊢ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
110	103, 108, 109	syl2anc 593	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
111		predss 6291	. . . . . . . . 9 ⊢ Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶
112	111	a1i 11	. . . . . . . 8 ⊢ (𝑐 ∈ 𝐶 → Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶)
113		snssi 4741	. . . . . . . 8 ⊢ (𝑐 ∈ 𝐶 → {𝑐} ⊆ 𝐶)
114	112, 113	unssd 4142	. . . . . . 7 ⊢ (𝑐 ∈ 𝐶 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶)
115	114	3ad2ant3 1147	. . . . . 6 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶)
116		xpss12 5658	. . . . . 6 ⊢ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵) ∧ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶))
117	110, 115, 116	syl2anc 593	. . . . 5 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶))
118	117	ssdifssd 4098	. . . 4 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ⊆ ((𝐴 × 𝐵) × 𝐶))
119		sseqin2 4173	. . . 4 ⊢ (((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
120	118, 119	sylib 220	. . 3 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
121	98, 120	eqtrd 2796	. 2 ⊢ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
122	11, 22, 32, 121	vtocl3ga 3544	1 ⊢ ((𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩}))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 ∨ w3o 1096 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 ∃wrex 3085 Vcvv 3453 ∖ cdif 3899 ∪ cun 3900 ∩ cin 3901 ⊆ wss 3902 {csn 4579 ⟨cotp 4587 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-3or 1098 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-sbc 3743 df-csb 3851 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-ot 4588 df-uni 4863 df-iun 4948 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: sexp3 8127 xpord3inddlem 8128

W3C validator