Theorem xpord3lem 8153

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 5445	. . 3 ⊢ ⟨𝑎, 𝑏, 𝑐⟩ ∈ V
2		otex 5445	. . 3 ⊢ ⟨𝑑, 𝑒, 𝑓⟩ ∈ V
3		eleq1 2823	. . . 4 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶)))
4		2fveq3 6886	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)))
5		vex 3468	. . . . . . . . . 10 ⊢ 𝑎 ∈ V
6		vex 3468	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
7		vex 3468	. . . . . . . . . 10 ⊢ 𝑐 ∈ V
8		ot1stg 8007	. . . . . . . . . 10 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) → (1st ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑎)
9	5, 6, 7, 8	mp3an 1463	. . . . . . . . 9 ⊢ (1st ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑎
10	4, 9	eqtrdi 2787	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (1st ‘(1st ‘𝑥)) = 𝑎)
11	10	breq1d 5134	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ↔ 𝑎𝑅(1st ‘(1st ‘𝑦))))
12	10	eqeq1d 2738	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦)) ↔ 𝑎 = (1st ‘(1st ‘𝑦))))
13	11, 12	orbi12d 918	. . . . . 6 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ↔ (𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦)))))
14		2fveq3 6886	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)))
15		ot2ndg 8008	. . . . . . . . . 10 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) → (2nd ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑏)
16	5, 6, 7, 15	mp3an 1463	. . . . . . . . 9 ⊢ (2nd ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑏
17	14, 16	eqtrdi 2787	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘(1st ‘𝑥)) = 𝑏)
18	17	breq1d 5134	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ↔ 𝑏𝑆(2nd ‘(1st ‘𝑦))))
19	17	eqeq1d 2738	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦)) ↔ 𝑏 = (2nd ‘(1st ‘𝑦))))
20	18, 19	orbi12d 918	. . . . . 6 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ↔ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦)))))
21		fveq2 6881	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘𝑥) = (2nd ‘⟨𝑎, 𝑏, 𝑐⟩))
22		ot3rdg 8009	. . . . . . . . . 10 ⊢ (𝑐 ∈ V → (2nd ‘⟨𝑎, 𝑏, 𝑐⟩) = 𝑐)
23	22	elv 3469	. . . . . . . . 9 ⊢ (2nd ‘⟨𝑎, 𝑏, 𝑐⟩) = 𝑐
24	21, 23	eqtrdi 2787	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘𝑥) = 𝑐)
25	24	breq1d 5134	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ↔ 𝑐𝑇(2nd ‘𝑦)))
26	24	eqeq1d 2738	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘𝑥) = (2nd ‘𝑦) ↔ 𝑐 = (2nd ‘𝑦)))
27	25, 26	orbi12d 918	. . . . . 6 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ↔ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))))
28	13, 20, 27	3anbi123d 1438	. . . . 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 632	. . . 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 1440	. . 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 2823	. . . 4 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶)))
33		2fveq3 6886	. . . . . . . . 9 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (1st ‘(1st ‘𝑦)) = (1st ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)))
34		vex 3468	. . . . . . . . . 10 ⊢ 𝑑 ∈ V
35		vex 3468	. . . . . . . . . 10 ⊢ 𝑒 ∈ V
36		vex 3468	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
37		ot1stg 8007	. . . . . . . . . 10 ⊢ ((𝑑 ∈ V ∧ 𝑒 ∈ V ∧ 𝑓 ∈ V) → (1st ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑑)
38	34, 35, 36, 37	mp3an 1463	. . . . . . . . 9 ⊢ (1st ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑑
39	33, 38	eqtrdi 2787	. . . . . . . 8 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (1st ‘(1st ‘𝑦)) = 𝑑)
40	39	breq2d 5136	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑎𝑅(1st ‘(1st ‘𝑦)) ↔ 𝑎𝑅𝑑))
41	39	eqeq2d 2747	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑎 = (1st ‘(1st ‘𝑦)) ↔ 𝑎 = 𝑑))
42	40, 41	orbi12d 918	. . . . . 6 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ↔ (𝑎𝑅𝑑 ∨ 𝑎 = 𝑑)))
43		2fveq3 6886	. . . . . . . . 9 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘(1st ‘𝑦)) = (2nd ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)))
44		ot2ndg 8008	. . . . . . . . . 10 ⊢ ((𝑑 ∈ V ∧ 𝑒 ∈ V ∧ 𝑓 ∈ V) → (2nd ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑒)
45	34, 35, 36, 44	mp3an 1463	. . . . . . . . 9 ⊢ (2nd ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑒
46	43, 45	eqtrdi 2787	. . . . . . . 8 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘(1st ‘𝑦)) = 𝑒)
47	46	breq2d 5136	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑏𝑆(2nd ‘(1st ‘𝑦)) ↔ 𝑏𝑆𝑒))
48	46	eqeq2d 2747	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑏 = (2nd ‘(1st ‘𝑦)) ↔ 𝑏 = 𝑒))
49	47, 48	orbi12d 918	. . . . . 6 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ↔ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒)))
50		fveq2 6881	. . . . . . . . 9 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘𝑦) = (2nd ‘⟨𝑑, 𝑒, 𝑓⟩))
51		ot3rdg 8009	. . . . . . . . . 10 ⊢ (𝑓 ∈ V → (2nd ‘⟨𝑑, 𝑒, 𝑓⟩) = 𝑓)
52	51	elv 3469	. . . . . . . . 9 ⊢ (2nd ‘⟨𝑑, 𝑒, 𝑓⟩) = 𝑓
53	50, 52	eqtrdi 2787	. . . . . . . 8 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘𝑦) = 𝑓)
54	53	breq2d 5136	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑐𝑇(2nd ‘𝑦) ↔ 𝑐𝑇𝑓))
55	53	eqeq2d 2747	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑐 = (2nd ‘𝑦) ↔ 𝑐 = 𝑓))
56	54, 55	orbi12d 918	. . . . . 6 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦)) ↔ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)))
57	42, 49, 56	3anbi123d 1438	. . . . 5 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ↔ ((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓))))
58		neeq2 2996	. . . . 5 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦 ↔ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩))
59	57, 58	anbi12d 632	. . . 4 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩)))
60	32, 59	3anbi23d 1441	. . 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 5523	. 2 ⊢ (⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩ ↔ (⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩)))
63		otelxp 5703	. . 3 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))
64		otelxp 5703	. . 3 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶))
65	5, 6, 7	otthne 5466	. . . 4 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩ ↔ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))
66	65	anbi2i 623	. . 3 ⊢ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)))
67	63, 64, 66	3anbi123i 1155	. 2 ⊢ ((⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))
68	62, 67	bitri 275	1 ⊢ (⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∨ w3o 1085   ∧ w3a 1086   = wceq 1540   ∈ wcel 2109   ≠ wne 2933  Vcvv 3464  ⟨cotp 4614   class class class wbr 5124  {copab 5186   × cxp 5657  ‘cfv 6536  1^st c1st 7991  2^nd c2nd 7992

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-ot 4615  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-iota 6489  df-fun 6538  df-fv 6544  df-1st 7993  df-2nd 7994

This theorem is referenced by:  poxp3  8154  frxp3  8155  xpord3pred  8156