Theorem xpord3lem 8141

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 5447	. . 3 ⊢ ⟨𝑎, 𝑏, 𝑐⟩ ∈ V
2		otex 5447	. . 3 ⊢ ⟨𝑑, 𝑒, 𝑓⟩ ∈ V
3		eleq1 2851	. . . 4 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶)))
4		2fveq3 6886	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)))
5		vex 3459	. . . . . . . . . 10 ⊢ 𝑎 ∈ V
6		vex 3459	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
7		vex 3459	. . . . . . . . . 10 ⊢ 𝑐 ∈ V
8		ot1stg 7996	. . . . . . . . . 10 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) → (1st ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑎)
9	5, 6, 7, 8	mp3an 1490	. . . . . . . . 9 ⊢ (1st ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑎
10	4, 9	eqtrdi 2814	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (1st ‘(1st ‘𝑥)) = 𝑎)
11	10	breq1d 5119	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ↔ 𝑎𝑅(1st ‘(1st ‘𝑦))))
12	10	eqeq1d 2765	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦)) ↔ 𝑎 = (1st ‘(1st ‘𝑦))))
13	11, 12	orbi12d 931	. . . . . 6 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ↔ (𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦)))))
14		2fveq3 6886	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)))
15		ot2ndg 7997	. . . . . . . . . 10 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) → (2nd ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑏)
16	5, 6, 7, 15	mp3an 1490	. . . . . . . . 9 ⊢ (2nd ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑏
17	14, 16	eqtrdi 2814	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘(1st ‘𝑥)) = 𝑏)
18	17	breq1d 5119	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ↔ 𝑏𝑆(2nd ‘(1st ‘𝑦))))
19	17	eqeq1d 2765	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦)) ↔ 𝑏 = (2nd ‘(1st ‘𝑦))))
20	18, 19	orbi12d 931	. . . . . 6 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ↔ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦)))))
21		fveq2 6881	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘𝑥) = (2nd ‘⟨𝑎, 𝑏, 𝑐⟩))
22		ot3rdg 7998	. . . . . . . . . 10 ⊢ (𝑐 ∈ V → (2nd ‘⟨𝑎, 𝑏, 𝑐⟩) = 𝑐)
23	22	elv 3460	. . . . . . . . 9 ⊢ (2nd ‘⟨𝑎, 𝑏, 𝑐⟩) = 𝑐
24	21, 23	eqtrdi 2814	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘𝑥) = 𝑐)
25	24	breq1d 5119	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ↔ 𝑐𝑇(2nd ‘𝑦)))
26	24	eqeq1d 2765	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘𝑥) = (2nd ‘𝑦) ↔ 𝑐 = (2nd ‘𝑦)))
27	25, 26	orbi12d 931	. . . . . 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 3020	. . . . 5 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (𝑥 ≠ 𝑦 ↔ ⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦))
30	28, 29	anbi12d 643	. . . 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 2851	. . . 4 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶)))
33		2fveq3 6886	. . . . . . . . 9 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (1st ‘(1st ‘𝑦)) = (1st ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)))
34		vex 3459	. . . . . . . . . 10 ⊢ 𝑑 ∈ V
35		vex 3459	. . . . . . . . . 10 ⊢ 𝑒 ∈ V
36		vex 3459	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
37		ot1stg 7996	. . . . . . . . . 10 ⊢ ((𝑑 ∈ V ∧ 𝑒 ∈ V ∧ 𝑓 ∈ V) → (1st ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑑)
38	34, 35, 36, 37	mp3an 1490	. . . . . . . . 9 ⊢ (1st ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑑
39	33, 38	eqtrdi 2814	. . . . . . . 8 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (1st ‘(1st ‘𝑦)) = 𝑑)
40	39	breq2d 5121	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑎𝑅(1st ‘(1st ‘𝑦)) ↔ 𝑎𝑅𝑑))
41	39	eqeq2d 2774	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑎 = (1st ‘(1st ‘𝑦)) ↔ 𝑎 = 𝑑))
42	40, 41	orbi12d 931	. . . . . 6 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ↔ (𝑎𝑅𝑑 ∨ 𝑎 = 𝑑)))
43		2fveq3 6886	. . . . . . . . 9 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘(1st ‘𝑦)) = (2nd ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)))
44		ot2ndg 7997	. . . . . . . . . 10 ⊢ ((𝑑 ∈ V ∧ 𝑒 ∈ V ∧ 𝑓 ∈ V) → (2nd ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑒)
45	34, 35, 36, 44	mp3an 1490	. . . . . . . . 9 ⊢ (2nd ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑒
46	43, 45	eqtrdi 2814	. . . . . . . 8 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘(1st ‘𝑦)) = 𝑒)
47	46	breq2d 5121	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑏𝑆(2nd ‘(1st ‘𝑦)) ↔ 𝑏𝑆𝑒))
48	46	eqeq2d 2774	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑏 = (2nd ‘(1st ‘𝑦)) ↔ 𝑏 = 𝑒))
49	47, 48	orbi12d 931	. . . . . 6 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ↔ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒)))
50		fveq2 6881	. . . . . . . . 9 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘𝑦) = (2nd ‘⟨𝑑, 𝑒, 𝑓⟩))
51		ot3rdg 7998	. . . . . . . . . 10 ⊢ (𝑓 ∈ V → (2nd ‘⟨𝑑, 𝑒, 𝑓⟩) = 𝑓)
52	51	elv 3460	. . . . . . . . 9 ⊢ (2nd ‘⟨𝑑, 𝑒, 𝑓⟩) = 𝑓
53	50, 52	eqtrdi 2814	. . . . . . . 8 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘𝑦) = 𝑓)
54	53	breq2d 5121	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑐𝑇(2nd ‘𝑦) ↔ 𝑐𝑇𝑓))
55	53	eqeq2d 2774	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑐 = (2nd ‘𝑦) ↔ 𝑐 = 𝑓))
56	54, 55	orbi12d 931	. . . . . 6 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦)) ↔ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)))
57	42, 49, 56	3anbi123d 1464	. . . . 5 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ↔ ((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓))))
58		neeq2 3021	. . . . 5 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦 ↔ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩))
59	57, 58	anbi12d 643	. . . 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 5528	. 2 ⊢ (⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩ ↔ (⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩)))
63		otelxp 5705	. . 3 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))
64		otelxp 5705	. . 3 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶))
65	5, 6, 7	otthne 5468	. . . 4 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩ ↔ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))
66	65	anbi2i 634	. . 3 ⊢ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)))
67	63, 64, 66	3anbi123i 1173	. 2 ⊢ ((⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))
68	62, 67	bitri 278	1 ⊢ (⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))

Syntax hints:   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∨ w3o 1102   ∧ w3a 1103   = wceq 1570   ∈ wcel 2143   ≠ wne 2958  Vcvv 3455  ⟨cotp 4597   class class class wbr 5109  {copab 5173   × cxp 5659  ‘cfv 6536  1^st c1st 7980  2^nd c2nd 7981

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-ot 4598  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-iota 6492  df-fun 6538  df-fv 6544  df-1st 7982  df-2nd 7983

This theorem is referenced by:  poxp3  8142  frxp3  8143  xpord3pred  8144