Theorem xpord3lem 33722

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 5373	. . 3 ⊢ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ V
2		opex 5373	. . 3 ⊢ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ V
3		eleq1 2826	. . . 4 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶)))
4		vex 3426	. . . . . . . . 9 ⊢ 𝑎 ∈ V
5		vex 3426	. . . . . . . . 9 ⊢ 𝑏 ∈ V
6		vex 3426	. . . . . . . . 9 ⊢ 𝑐 ∈ V
7	4, 5, 6	ot21std 33583	. . . . . . . 8 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (1st ‘(1st ‘𝑥)) = 𝑎)
8	7	breq1d 5080	. . . . . . 7 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ↔ 𝑎𝑅(1st ‘(1st ‘𝑦))))
9	7	eqeq1d 2740	. . . . . . 7 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦)) ↔ 𝑎 = (1st ‘(1st ‘𝑦))))
10	8, 9	orbi12d 915	. . . . . 6 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ↔ (𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦)))))
11	4, 5, 6	ot22ndd 33584	. . . . . . . 8 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (2nd ‘(1st ‘𝑥)) = 𝑏)
12	11	breq1d 5080	. . . . . . 7 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ↔ 𝑏𝑆(2nd ‘(1st ‘𝑦))))
13	11	eqeq1d 2740	. . . . . . 7 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦)) ↔ 𝑏 = (2nd ‘(1st ‘𝑦))))
14	12, 13	orbi12d 915	. . . . . 6 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ↔ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦)))))
15		opex 5373	. . . . . . . . 9 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
16	15, 6	op2ndd 7815	. . . . . . . 8 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (2nd ‘𝑥) = 𝑐)
17	16	breq1d 5080	. . . . . . 7 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ↔ 𝑐𝑇(2nd ‘𝑦)))
18	16	eqeq1d 2740	. . . . . . 7 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → ((2nd ‘𝑥) = (2nd ‘𝑦) ↔ 𝑐 = (2nd ‘𝑦)))
19	17, 18	orbi12d 915	. . . . . 6 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ↔ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))))
20	10, 14, 19	3anbi123d 1434	. . . . 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 3005	. . . . 5 ⊢ (𝑥 = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ → (𝑥 ≠ 𝑦 ↔ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ 𝑦))
22	20, 21	anbi12d 630	. . . 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 1436	. . 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 2826	. . . 4 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶)))
25		vex 3426	. . . . . . . . 9 ⊢ 𝑑 ∈ V
26		vex 3426	. . . . . . . . 9 ⊢ 𝑒 ∈ V
27		vex 3426	. . . . . . . . 9 ⊢ 𝑓 ∈ V
28	25, 26, 27	ot21std 33583	. . . . . . . 8 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (1st ‘(1st ‘𝑦)) = 𝑑)
29	28	breq2d 5082	. . . . . . 7 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑎𝑅(1st ‘(1st ‘𝑦)) ↔ 𝑎𝑅𝑑))
30	28	eqeq2d 2749	. . . . . . 7 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑎 = (1st ‘(1st ‘𝑦)) ↔ 𝑎 = 𝑑))
31	29, 30	orbi12d 915	. . . . . 6 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ↔ (𝑎𝑅𝑑 ∨ 𝑎 = 𝑑)))
32	25, 26, 27	ot22ndd 33584	. . . . . . . 8 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (2nd ‘(1st ‘𝑦)) = 𝑒)
33	32	breq2d 5082	. . . . . . 7 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑏𝑆(2nd ‘(1st ‘𝑦)) ↔ 𝑏𝑆𝑒))
34	32	eqeq2d 2749	. . . . . . 7 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑏 = (2nd ‘(1st ‘𝑦)) ↔ 𝑏 = 𝑒))
35	33, 34	orbi12d 915	. . . . . 6 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ((𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ↔ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒)))
36		opex 5373	. . . . . . . . 9 ⊢ ⟨𝑑, 𝑒⟩ ∈ V
37	36, 27	op2ndd 7815	. . . . . . . 8 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (2nd ‘𝑦) = 𝑓)
38	37	breq2d 5082	. . . . . . 7 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑐𝑇(2nd ‘𝑦) ↔ 𝑐𝑇𝑓))
39	37	eqeq2d 2749	. . . . . . 7 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑐 = (2nd ‘𝑦) ↔ 𝑐 = 𝑓))
40	38, 39	orbi12d 915	. . . . . 6 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ((𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦)) ↔ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)))
41	31, 35, 40	3anbi123d 1434	. . . . 5 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ↔ ((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓))))
42		neeq2 3006	. . . . 5 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ 𝑦 ↔ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩))
43	41, 42	anbi12d 630	. . . 4 ⊢ (𝑦 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ((((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ 𝑦) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩)))
44	24, 43	3anbi23d 1437	. . 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 5449	. 2 ⊢ (⟨⟨𝑎, 𝑏⟩, 𝑐⟩𝑈⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ↔ (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩)))
47		ot2elxp 33582	. . 3 ⊢ (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))
48		ot2elxp 33582	. . 3 ⊢ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶))
49	4, 5, 6	otthne 33585	. . . 4 ⊢ (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ↔ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))
50	49	anbi2i 622	. . 3 ⊢ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)))
51	47, 48, 50	3anbi123i 1153	. 2 ⊢ ((⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ≠ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))
52	46, 51	bitri 274	1 ⊢ (⟨⟨𝑎, 𝑏⟩, 𝑐⟩𝑈⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))

Syntax hints:   ↔ wb 205   ∧ wa 395   ∨ wo 843   ∨ w3o 1084   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108   ≠ wne 2942  ⟨cop 4564   class class class wbr 5070  {copab 5132   × cxp 5578  ‘cfv 6418  1^st c1st 7802  2^nd c2nd 7803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-iota 6376  df-fun 6420  df-fv 6426  df-1st 7804  df-2nd 7805

This theorem is referenced by:  poxp3  33723  frxp3  33724  xpord3pred  33725