Theorem xpord3lem 33362

Description: Lemma for triple ordering. Calculate the value of the relationship. (Contributed by Scott Fenton, 21-Aug-2024.)

Hypothesis

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

Assertion

Ref	Expression
xpord3lem	⊢ (⟨⟨𝑎, 𝑏⟩, 𝑐⟩𝑈⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))

Distinct variable groups:   𝑥,𝑎   𝑥,𝐴   𝑦,𝑎   𝑦,𝐴   𝑥,𝑏   𝑥,𝐵   𝑦,𝑏   𝑦,𝐵   𝑥,𝑐   𝑥,𝐶   𝑦,𝑐   𝑦,𝐶   𝑥,𝑑,𝑦   𝑥,𝑒,𝑦   𝑥,𝑓,𝑦   𝑥,𝑅,𝑦   𝑥,𝑆,𝑦   𝑥,𝑇,𝑦

Allowed substitution hints:   𝐴(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)   𝐵(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)   𝐶(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)   𝑅(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)   𝑆(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)   𝑇(𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)   𝑈(𝑥,𝑦,𝑒,𝑓,𝑎,𝑏,𝑐,𝑑)

Proof of Theorem xpord3lem

Step	Hyp	Ref	Expression
1		opex 5328	. . 3 ⊢ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ V
2		opex 5328	. . 3 ⊢ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ V
3		eleq1 2839	. . . 4 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶)))
4		vex 3413	. . . . . . . . 9 ⊢ 𝑎 ∈ V
5		vex 3413	. . . . . . . . 9 ⊢ 𝑏 ∈ V
6		vex 3413	. . . . . . . . 9 ⊢ 𝑐 ∈ V
7	4, 5, 6	ot21std 33211	. . . . . . . 8 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (1st ‘(1st ‘𝑥)) = 𝑎)
8	7	breq1d 5046	. . . . . . 7 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ↔ 𝑎𝑅(1st ‘(1st ‘𝑦))))
9	7	eqeq1d 2760	. . . . . . 7 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦)) ↔ 𝑎 = (1st ‘(1st ‘𝑦))))
10	8, 9	orbi12d 916	. . . . . 6 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ↔ (𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦)))))
11	4, 5, 6	ot22ndd 33212	. . . . . . . 8 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (2nd ‘(1st ‘𝑥)) = 𝑏)
12	11	breq1d 5046	. . . . . . 7 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ↔ 𝑏𝑆(2nd ‘(1st ‘𝑦))))
13	11	eqeq1d 2760	. . . . . . 7 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦)) ↔ 𝑏 = (2nd ‘(1st ‘𝑦))))
14	12, 13	orbi12d 916	. . . . . 6 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ↔ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦)))))
15		opex 5328	. . . . . . . . 9 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
16	15, 6	op2ndd 7710	. . . . . . . 8 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (2nd ‘𝑥) = 𝑐)
17	16	breq1d 5046	. . . . . . 7 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ↔ 𝑐𝑇(2nd ‘𝑦)))
18	16	eqeq1d 2760	. . . . . . 7 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((2nd ‘𝑥) = (2nd ‘𝑦) ↔ 𝑐 = (2nd ‘𝑦)))
19	17, 18	orbi12d 916	. . . . . 6 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ↔ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))))
20	10, 14, 19	3anbi123d 1433	. . . . 5 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ∧ ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ∧ ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ↔ ((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦)))))
21		neeq1 3013	. . . . 5 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (𝑥 ≠ 𝑦 ↔ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ 𝑦))
22	20, 21	anbi12d 633	. . . 4 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (((((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ∧ ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ∧ ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦) ↔ (((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ 𝑦)))
23	3, 22	3anbi13d 1435	. . 3 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ∧ ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ∧ ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦)) ↔ (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ 𝑦))))
24		eleq1 2839	. . . 4 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶)))
25		vex 3413	. . . . . . . . 9 ⊢ 𝑑 ∈ V
26		vex 3413	. . . . . . . . 9 ⊢ 𝑒 ∈ V
27		vex 3413	. . . . . . . . 9 ⊢ 𝑓 ∈ V
28	25, 26, 27	ot21std 33211	. . . . . . . 8 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (1st ‘(1st ‘𝑦)) = 𝑑)
29	28	breq2d 5048	. . . . . . 7 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑎𝑅(1st ‘(1st ‘𝑦)) ↔ 𝑎𝑅𝑑))
30	28	eqeq2d 2769	. . . . . . 7 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑎 = (1st ‘(1st ‘𝑦)) ↔ 𝑎 = 𝑑))
31	29, 30	orbi12d 916	. . . . . 6 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ↔ (𝑎𝑅𝑑 ∨ 𝑎 = 𝑑)))
32	25, 26, 27	ot22ndd 33212	. . . . . . . 8 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (2nd ‘(1st ‘𝑦)) = 𝑒)
33	32	breq2d 5048	. . . . . . 7 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑏𝑆(2nd ‘(1st ‘𝑦)) ↔ 𝑏𝑆𝑒))
34	32	eqeq2d 2769	. . . . . . 7 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑏 = (2nd ‘(1st ‘𝑦)) ↔ 𝑏 = 𝑒))
35	33, 34	orbi12d 916	. . . . . 6 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ((𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ↔ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒)))
36		opex 5328	. . . . . . . . 9 ⊢ ⟨𝑑, 𝑒⟩ ∈ V
37	36, 27	op2ndd 7710	. . . . . . . 8 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (2nd ‘𝑦) = 𝑓)
38	37	breq2d 5048	. . . . . . 7 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑐𝑇(2nd ‘𝑦) ↔ 𝑐𝑇𝑓))
39	37	eqeq2d 2769	. . . . . . 7 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑐 = (2nd ‘𝑦) ↔ 𝑐 = 𝑓))
40	38, 39	orbi12d 916	. . . . . 6 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ((𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦)) ↔ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)))
41	31, 35, 40	3anbi123d 1433	. . . . 5 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ↔ ((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓))))
42		neeq2 3014	. . . . 5 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ 𝑦 ↔ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩))
43	41, 42	anbi12d 633	. . . 4 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ((((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ 𝑦) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩)))
44	24, 43	3anbi23d 1436	. . 3 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ((⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ 𝑦)) ↔ (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩))))
45		xpord3.1	. . 3 ⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ∧ ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ∧ ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}
46	1, 2, 23, 44, 45	brab 5404	. 2 ⊢ (⟨⟨𝑎, 𝑏⟩, 𝑐⟩𝑈⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ↔ (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩)))
47		ot2elxp 33210	. . 3 ⊢ (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))
48		ot2elxp 33210	. . 3 ⊢ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶))
49	4, 5, 6	otthne 33213	. . . 4 ⊢ (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ↔ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))
50	49	anbi2i 625	. . 3 ⊢ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)))
51	47, 48, 50	3anbi123i 1152	. 2 ⊢ ((⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))
52	46, 51	bitri 278	1 ⊢ (⟨⟨𝑎, 𝑏⟩, 𝑐⟩𝑈⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))

Syntax hints:   ↔ wb 209   ∧ wa 399   ∨ wo 844   ∨ w3o 1083   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  ⟨cop 4531   class class class wbr 5036  {copab 5098   × cxp 5526  ‘cfv 6340  1^st c1st 7697  2^nd c2nd 7698

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pr 5302  ax-un 7465

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5037  df-opab 5099  df-mpt 5117  df-id 5434  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-iota 6299  df-fun 6342  df-fv 6348  df-1st 7699  df-2nd 7700

This theorem is referenced by:  poxp3  33363  frxp3  33364  xpord3pred  33365