Theorem xpord3lem 8101

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 5421	. . 3 ⊢ ⟨𝑎, 𝑏, 𝑐⟩ ∈ V
2		otex 5421	. . 3 ⊢ ⟨𝑑, 𝑒, 𝑓⟩ ∈ V
3		eleq1 2825	. . . 4 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶)))
4		2fveq3 6847	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)))
5		vex 3446	. . . . . . . . . 10 ⊢ 𝑎 ∈ V
6		vex 3446	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
7		vex 3446	. . . . . . . . . 10 ⊢ 𝑐 ∈ V
8		ot1stg 7957	. . . . . . . . . 10 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) → (1st ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑎)
9	5, 6, 7, 8	mp3an 1464	. . . . . . . . 9 ⊢ (1st ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑎
10	4, 9	eqtrdi 2788	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (1st ‘(1st ‘𝑥)) = 𝑎)
11	10	breq1d 5110	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ↔ 𝑎𝑅(1st ‘(1st ‘𝑦))))
12	10	eqeq1d 2739	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦)) ↔ 𝑎 = (1st ‘(1st ‘𝑦))))
13	11, 12	orbi12d 919	. . . . . 6 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ↔ (𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦)))))
14		2fveq3 6847	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)))
15		ot2ndg 7958	. . . . . . . . . 10 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) → (2nd ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑏)
16	5, 6, 7, 15	mp3an 1464	. . . . . . . . 9 ⊢ (2nd ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑏
17	14, 16	eqtrdi 2788	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘(1st ‘𝑥)) = 𝑏)
18	17	breq1d 5110	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ↔ 𝑏𝑆(2nd ‘(1st ‘𝑦))))
19	17	eqeq1d 2739	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦)) ↔ 𝑏 = (2nd ‘(1st ‘𝑦))))
20	18, 19	orbi12d 919	. . . . . 6 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ↔ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦)))))
21		fveq2 6842	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘𝑥) = (2nd ‘⟨𝑎, 𝑏, 𝑐⟩))
22		ot3rdg 7959	. . . . . . . . . 10 ⊢ (𝑐 ∈ V → (2nd ‘⟨𝑎, 𝑏, 𝑐⟩) = 𝑐)
23	22	elv 3447	. . . . . . . . 9 ⊢ (2nd ‘⟨𝑎, 𝑏, 𝑐⟩) = 𝑐
24	21, 23	eqtrdi 2788	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘𝑥) = 𝑐)
25	24	breq1d 5110	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ↔ 𝑐𝑇(2nd ‘𝑦)))
26	24	eqeq1d 2739	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘𝑥) = (2nd ‘𝑦) ↔ 𝑐 = (2nd ‘𝑦)))
27	25, 26	orbi12d 919	. . . . . 6 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ↔ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))))
28	13, 20, 27	3anbi123d 1439	. . . . 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 2995	. . . . 5 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (𝑥 ≠ 𝑦 ↔ ⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦))
30	28, 29	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 ‘𝑦))) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦)))
31	3, 30	3anbi13d 1441	. . 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 2825	. . . 4 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶)))
33		2fveq3 6847	. . . . . . . . 9 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (1st ‘(1st ‘𝑦)) = (1st ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)))
34		vex 3446	. . . . . . . . . 10 ⊢ 𝑑 ∈ V
35		vex 3446	. . . . . . . . . 10 ⊢ 𝑒 ∈ V
36		vex 3446	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
37		ot1stg 7957	. . . . . . . . . 10 ⊢ ((𝑑 ∈ V ∧ 𝑒 ∈ V ∧ 𝑓 ∈ V) → (1st ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑑)
38	34, 35, 36, 37	mp3an 1464	. . . . . . . . 9 ⊢ (1st ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑑
39	33, 38	eqtrdi 2788	. . . . . . . 8 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (1st ‘(1st ‘𝑦)) = 𝑑)
40	39	breq2d 5112	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑎𝑅(1st ‘(1st ‘𝑦)) ↔ 𝑎𝑅𝑑))
41	39	eqeq2d 2748	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑎 = (1st ‘(1st ‘𝑦)) ↔ 𝑎 = 𝑑))
42	40, 41	orbi12d 919	. . . . . 6 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ↔ (𝑎𝑅𝑑 ∨ 𝑎 = 𝑑)))
43		2fveq3 6847	. . . . . . . . 9 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘(1st ‘𝑦)) = (2nd ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)))
44		ot2ndg 7958	. . . . . . . . . 10 ⊢ ((𝑑 ∈ V ∧ 𝑒 ∈ V ∧ 𝑓 ∈ V) → (2nd ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑒)
45	34, 35, 36, 44	mp3an 1464	. . . . . . . . 9 ⊢ (2nd ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑒
46	43, 45	eqtrdi 2788	. . . . . . . 8 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘(1st ‘𝑦)) = 𝑒)
47	46	breq2d 5112	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑏𝑆(2nd ‘(1st ‘𝑦)) ↔ 𝑏𝑆𝑒))
48	46	eqeq2d 2748	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑏 = (2nd ‘(1st ‘𝑦)) ↔ 𝑏 = 𝑒))
49	47, 48	orbi12d 919	. . . . . 6 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ↔ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒)))
50		fveq2 6842	. . . . . . . . 9 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘𝑦) = (2nd ‘⟨𝑑, 𝑒, 𝑓⟩))
51		ot3rdg 7959	. . . . . . . . . 10 ⊢ (𝑓 ∈ V → (2nd ‘⟨𝑑, 𝑒, 𝑓⟩) = 𝑓)
52	51	elv 3447	. . . . . . . . 9 ⊢ (2nd ‘⟨𝑑, 𝑒, 𝑓⟩) = 𝑓
53	50, 52	eqtrdi 2788	. . . . . . . 8 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘𝑦) = 𝑓)
54	53	breq2d 5112	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑐𝑇(2nd ‘𝑦) ↔ 𝑐𝑇𝑓))
55	53	eqeq2d 2748	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑐 = (2nd ‘𝑦) ↔ 𝑐 = 𝑓))
56	54, 55	orbi12d 919	. . . . . 6 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦)) ↔ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)))
57	42, 49, 56	3anbi123d 1439	. . . . 5 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ↔ ((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓))))
58		neeq2 2996	. . . . 5 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦 ↔ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩))
59	57, 58	anbi12d 633	. . . 4 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩)))
60	32, 59	3anbi23d 1442	. . 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 5499	. 2 ⊢ (⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩ ↔ (⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩)))
63		otelxp 5676	. . 3 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))
64		otelxp 5676	. . 3 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶))
65	5, 6, 7	otthne 5442	. . . 4 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩ ↔ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))
66	65	anbi2i 624	. . 3 ⊢ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)))
67	63, 64, 66	3anbi123i 1156	. 2 ⊢ ((⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))
68	62, 67	bitri 275	1 ⊢ (⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∨ w3o 1086   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2933  Vcvv 3442  ⟨cotp 4590   class class class wbr 5100  {copab 5162   × cxp 5630  ‘cfv 6500  1^st c1st 7941  2^nd c2nd 7942

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-ot 4591  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-iota 6456  df-fun 6502  df-fv 6508  df-1st 7943  df-2nd 7944

This theorem is referenced by:  poxp3  8102  frxp3  8103  xpord3pred  8104