Theorem xpord3lem 8166

Description: Lemma for triple ordering. Calculate the value of the relation. (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		otex 5434	. . 3 ⊢ ⟨𝑎, 𝑏, 𝑐⟩ ∈ V
2		otex 5434	. . 3 ⊢ ⟨𝑑, 𝑒, 𝑓⟩ ∈ V
3		eleq1 2849	. . . 4 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶)))
4		2fveq3 6890	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)))
5		vex 3455	. . . . . . . . . 10 ⊢ 𝑎 ∈ V
6		vex 3455	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
7		vex 3455	. . . . . . . . . 10 ⊢ 𝑐 ∈ V
8		ot1stg 8015	. . . . . . . . . 10 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) → (1st ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑎)
9	5, 6, 7, 8	mp3an 1490	. . . . . . . . 9 ⊢ (1st ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑎
10	4, 9	eqtrdi 2812	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (1st ‘(1st ‘𝑥)) = 𝑎)
11	10	breq1d 5113	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ↔ 𝑎𝑅(1st ‘(1st ‘𝑦))))
12	10	eqeq1d 2763	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦)) ↔ 𝑎 = (1st ‘(1st ‘𝑦))))
13	11, 12	orbi12d 932	. . . . . 6 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ↔ (𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦)))))
14		2fveq3 6890	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)))
15		ot2ndg 8016	. . . . . . . . . 10 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) → (2nd ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑏)
16	5, 6, 7, 15	mp3an 1490	. . . . . . . . 9 ⊢ (2nd ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑏
17	14, 16	eqtrdi 2812	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘(1st ‘𝑥)) = 𝑏)
18	17	breq1d 5113	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ↔ 𝑏𝑆(2nd ‘(1st ‘𝑦))))
19	17	eqeq1d 2763	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦)) ↔ 𝑏 = (2nd ‘(1st ‘𝑦))))
20	18, 19	orbi12d 932	. . . . . 6 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ↔ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦)))))
21		fveq2 6885	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘𝑥) = (2nd ‘⟨𝑎, 𝑏, 𝑐⟩))
22		ot3rdg 8017	. . . . . . . . . 10 ⊢ (𝑐 ∈ V → (2nd ‘⟨𝑎, 𝑏, 𝑐⟩) = 𝑐)
23	22	elv 3456	. . . . . . . . 9 ⊢ (2nd ‘⟨𝑎, 𝑏, 𝑐⟩) = 𝑐
24	21, 23	eqtrdi 2812	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘𝑥) = 𝑐)
25	24	breq1d 5113	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ↔ 𝑐𝑇(2nd ‘𝑦)))
26	24	eqeq1d 2763	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘𝑥) = (2nd ‘𝑦) ↔ 𝑐 = (2nd ‘𝑦)))
27	25, 26	orbi12d 932	. . . . . 6 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ↔ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))))
28	13, 20, 27	3anbi123d 1464	. . . . 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 ‘𝑦)))))
29		neeq1 3018	. . . . 5 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (𝑥 ≠ 𝑦 ↔ ⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦))
30	28, 29	anbi12d 644	. . . 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 ‘𝑦))) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦)))
31	3, 30	3anbi13d 1466	. . 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 ‘𝑦))) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦))))
32		eleq1 2849	. . . 4 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶)))
33		2fveq3 6890	. . . . . . . . 9 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (1st ‘(1st ‘𝑦)) = (1st ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)))
34		vex 3455	. . . . . . . . . 10 ⊢ 𝑑 ∈ V
35		vex 3455	. . . . . . . . . 10 ⊢ 𝑒 ∈ V
36		vex 3455	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
37		ot1stg 8015	. . . . . . . . . 10 ⊢ ((𝑑 ∈ V ∧ 𝑒 ∈ V ∧ 𝑓 ∈ V) → (1st ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑑)
38	34, 35, 36, 37	mp3an 1490	. . . . . . . . 9 ⊢ (1st ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑑
39	33, 38	eqtrdi 2812	. . . . . . . 8 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (1st ‘(1st ‘𝑦)) = 𝑑)
40	39	breq2d 5115	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑎𝑅(1st ‘(1st ‘𝑦)) ↔ 𝑎𝑅𝑑))
41	39	eqeq2d 2772	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑎 = (1st ‘(1st ‘𝑦)) ↔ 𝑎 = 𝑑))
42	40, 41	orbi12d 932	. . . . . 6 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ↔ (𝑎𝑅𝑑 ∨ 𝑎 = 𝑑)))
43		2fveq3 6890	. . . . . . . . 9 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘(1st ‘𝑦)) = (2nd ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)))
44		ot2ndg 8016	. . . . . . . . . 10 ⊢ ((𝑑 ∈ V ∧ 𝑒 ∈ V ∧ 𝑓 ∈ V) → (2nd ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑒)
45	34, 35, 36, 44	mp3an 1490	. . . . . . . . 9 ⊢ (2nd ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑒
46	43, 45	eqtrdi 2812	. . . . . . . 8 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘(1st ‘𝑦)) = 𝑒)
47	46	breq2d 5115	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑏𝑆(2nd ‘(1st ‘𝑦)) ↔ 𝑏𝑆𝑒))
48	46	eqeq2d 2772	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑏 = (2nd ‘(1st ‘𝑦)) ↔ 𝑏 = 𝑒))
49	47, 48	orbi12d 932	. . . . . 6 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ↔ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒)))
50		fveq2 6885	. . . . . . . . 9 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘𝑦) = (2nd ‘⟨𝑑, 𝑒, 𝑓⟩))
51		ot3rdg 8017	. . . . . . . . . 10 ⊢ (𝑓 ∈ V → (2nd ‘⟨𝑑, 𝑒, 𝑓⟩) = 𝑓)
52	51	elv 3456	. . . . . . . . 9 ⊢ (2nd ‘⟨𝑑, 𝑒, 𝑓⟩) = 𝑓
53	50, 52	eqtrdi 2812	. . . . . . . 8 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘𝑦) = 𝑓)
54	53	breq2d 5115	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑐𝑇(2nd ‘𝑦) ↔ 𝑐𝑇𝑓))
55	53	eqeq2d 2772	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑐 = (2nd ‘𝑦) ↔ 𝑐 = 𝑓))
56	54, 55	orbi12d 932	. . . . . 6 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦)) ↔ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)))
57	42, 49, 56	3anbi123d 1464	. . . . 5 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ↔ ((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓))))
58		neeq2 3019	. . . . 5 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦 ↔ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩))
59	57, 58	anbi12d 644	. . . 4 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩)))
60	32, 59	3anbi23d 1467	. . 3 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦)) ↔ (⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩))))
61		xpord3.1	. . 3 ⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ∧ ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ∧ ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}
62	1, 2, 31, 60, 61	brab 5518	. 2 ⊢ (⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩ ↔ (⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩)))
63		otelxp 5695	. . 3 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))
64		otelxp 5695	. . 3 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶))
65	5, 6, 7	otthne 5455	. . . 4 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩ ↔ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))
66	65	anbi2i 635	. . 3 ⊢ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)))
67	63, 64, 66	3anbi123i 1173	. 2 ⊢ ((⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))
68	62, 67	bitri 278	1 ⊢ (⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∨ w3o 1102   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2956  Vcvv 3451  ⟨cotp 4592   class class class wbr 5103  {copab 5167   × cxp 5649  ‘cfv 6538  1^st c1st 7999  2^nd c2nd 8000

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-ot 4593  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6494  df-fun 6540  df-fv 6546  df-1st 8001  df-2nd 8002

This theorem is used by:  poxp3  8167  frxp3  8168  xpord3pred  8169