Theorem xpord3lem 8081

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 5422	. . 3 ⊢ ⟨𝑎, 𝑏, 𝑐⟩ ∈ V
2		otex 5422	. . 3 ⊢ ⟨𝑑, 𝑒, 𝑓⟩ ∈ V
3		eleq1 2825	. . . 4 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶)))
4		2fveq3 6847	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)))
5		vex 3449	. . . . . . . . . 10 ⊢ 𝑎 ∈ V
6		vex 3449	. . . . . . . . . 10 ⊢ 𝑏 ∈ V
7		vex 3449	. . . . . . . . . 10 ⊢ 𝑐 ∈ V
8		ot1stg 7935	. . . . . . . . . 10 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) → (1st ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑎)
9	5, 6, 7, 8	mp3an 1461	. . . . . . . . 9 ⊢ (1st ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑎
10	4, 9	eqtrdi 2792	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (1st ‘(1st ‘𝑥)) = 𝑎)
11	10	breq1d 5115	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ↔ 𝑎𝑅(1st ‘(1st ‘𝑦))))
12	10	eqeq1d 2738	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦)) ↔ 𝑎 = (1st ‘(1st ‘𝑦))))
13	11, 12	orbi12d 917	. . . . . 6 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (((1st ‘(1st ‘𝑥))𝑅(1st ‘(1st ‘𝑦)) ∨ (1st ‘(1st ‘𝑥)) = (1st ‘(1st ‘𝑦))) ↔ (𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦)))))
14		2fveq3 6847	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)))
15		ot2ndg 7936	. . . . . . . . . 10 ⊢ ((𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V) → (2nd ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑏)
16	5, 6, 7, 15	mp3an 1461	. . . . . . . . 9 ⊢ (2nd ‘(1st ‘⟨𝑎, 𝑏, 𝑐⟩)) = 𝑏
17	14, 16	eqtrdi 2792	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘(1st ‘𝑥)) = 𝑏)
18	17	breq1d 5115	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ↔ 𝑏𝑆(2nd ‘(1st ‘𝑦))))
19	17	eqeq1d 2738	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦)) ↔ 𝑏 = (2nd ‘(1st ‘𝑦))))
20	18, 19	orbi12d 917	. . . . . 6 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (((2nd ‘(1st ‘𝑥))𝑆(2nd ‘(1st ‘𝑦)) ∨ (2nd ‘(1st ‘𝑥)) = (2nd ‘(1st ‘𝑦))) ↔ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦)))))
21		fveq2 6842	. . . . . . . . 9 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘𝑥) = (2nd ‘⟨𝑎, 𝑏, 𝑐⟩))
22		ot3rdg 7937	. . . . . . . . . 10 ⊢ (𝑐 ∈ V → (2nd ‘⟨𝑎, 𝑏, 𝑐⟩) = 𝑐)
23	22	elv 3451	. . . . . . . . 9 ⊢ (2nd ‘⟨𝑎, 𝑏, 𝑐⟩) = 𝑐
24	21, 23	eqtrdi 2792	. . . . . . . 8 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (2nd ‘𝑥) = 𝑐)
25	24	breq1d 5115	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘𝑥)𝑇(2nd ‘𝑦) ↔ 𝑐𝑇(2nd ‘𝑦)))
26	24	eqeq1d 2738	. . . . . . 7 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → ((2nd ‘𝑥) = (2nd ‘𝑦) ↔ 𝑐 = (2nd ‘𝑦)))
27	25, 26	orbi12d 917	. . . . . 6 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (((2nd ‘𝑥)𝑇(2nd ‘𝑦) ∨ (2nd ‘𝑥) = (2nd ‘𝑦)) ↔ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))))
28	13, 20, 27	3anbi123d 1436	. . . . 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 3006	. . . . 5 ⊢ (𝑥 = ⟨𝑎, 𝑏, 𝑐⟩ → (𝑥 ≠ 𝑦 ↔ ⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦))
30	28, 29	anbi12d 631	. . . 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 1438	. . 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 3449	. . . . . . . . . 10 ⊢ 𝑑 ∈ V
35		vex 3449	. . . . . . . . . 10 ⊢ 𝑒 ∈ V
36		vex 3449	. . . . . . . . . 10 ⊢ 𝑓 ∈ V
37		ot1stg 7935	. . . . . . . . . 10 ⊢ ((𝑑 ∈ V ∧ 𝑒 ∈ V ∧ 𝑓 ∈ V) → (1st ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑑)
38	34, 35, 36, 37	mp3an 1461	. . . . . . . . 9 ⊢ (1st ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑑
39	33, 38	eqtrdi 2792	. . . . . . . 8 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (1st ‘(1st ‘𝑦)) = 𝑑)
40	39	breq2d 5117	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑎𝑅(1st ‘(1st ‘𝑦)) ↔ 𝑎𝑅𝑑))
41	39	eqeq2d 2747	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑎 = (1st ‘(1st ‘𝑦)) ↔ 𝑎 = 𝑑))
42	40, 41	orbi12d 917	. . . . . 6 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ↔ (𝑎𝑅𝑑 ∨ 𝑎 = 𝑑)))
43		2fveq3 6847	. . . . . . . . 9 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘(1st ‘𝑦)) = (2nd ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)))
44		ot2ndg 7936	. . . . . . . . . 10 ⊢ ((𝑑 ∈ V ∧ 𝑒 ∈ V ∧ 𝑓 ∈ V) → (2nd ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑒)
45	34, 35, 36, 44	mp3an 1461	. . . . . . . . 9 ⊢ (2nd ‘(1st ‘⟨𝑑, 𝑒, 𝑓⟩)) = 𝑒
46	43, 45	eqtrdi 2792	. . . . . . . 8 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘(1st ‘𝑦)) = 𝑒)
47	46	breq2d 5117	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑏𝑆(2nd ‘(1st ‘𝑦)) ↔ 𝑏𝑆𝑒))
48	46	eqeq2d 2747	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑏 = (2nd ‘(1st ‘𝑦)) ↔ 𝑏 = 𝑒))
49	47, 48	orbi12d 917	. . . . . 6 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ↔ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒)))
50		fveq2 6842	. . . . . . . . 9 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘𝑦) = (2nd ‘⟨𝑑, 𝑒, 𝑓⟩))
51		ot3rdg 7937	. . . . . . . . . 10 ⊢ (𝑓 ∈ V → (2nd ‘⟨𝑑, 𝑒, 𝑓⟩) = 𝑓)
52	51	elv 3451	. . . . . . . . 9 ⊢ (2nd ‘⟨𝑑, 𝑒, 𝑓⟩) = 𝑓
53	50, 52	eqtrdi 2792	. . . . . . . 8 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (2nd ‘𝑦) = 𝑓)
54	53	breq2d 5117	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑐𝑇(2nd ‘𝑦) ↔ 𝑐𝑇𝑓))
55	53	eqeq2d 2747	. . . . . . 7 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑐 = (2nd ‘𝑦) ↔ 𝑐 = 𝑓))
56	54, 55	orbi12d 917	. . . . . 6 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦)) ↔ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)))
57	42, 49, 56	3anbi123d 1436	. . . . 5 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ↔ ((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓))))
58		neeq2 3007	. . . . 5 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → (⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦 ↔ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩))
59	57, 58	anbi12d 631	. . . 4 ⊢ (𝑦 = ⟨𝑑, 𝑒, 𝑓⟩ → ((((𝑎𝑅(1st ‘(1st ‘𝑦)) ∨ 𝑎 = (1st ‘(1st ‘𝑦))) ∧ (𝑏𝑆(2nd ‘(1st ‘𝑦)) ∨ 𝑏 = (2nd ‘(1st ‘𝑦))) ∧ (𝑐𝑇(2nd ‘𝑦) ∨ 𝑐 = (2nd ‘𝑦))) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ 𝑦) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩)))
60	32, 59	3anbi23d 1439	. . 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 5500	. 2 ⊢ (⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩ ↔ (⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩)))
63		otelxp 5676	. . 3 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))
64		otelxp 5676	. . 3 ⊢ (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ↔ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶))
65	5, 6, 7	otthne 5443	. . . 4 ⊢ (⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩ ↔ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))
66	65	anbi2i 623	. . 3 ⊢ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩) ↔ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)))
67	63, 64, 66	3anbi123i 1155	. 2 ⊢ ((⟨𝑎, 𝑏, 𝑐⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((𝐴 × 𝐵) × 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ ⟨𝑎, 𝑏, 𝑐⟩ ≠ ⟨𝑑, 𝑒, 𝑓⟩)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))
68	62, 67	bitri 274	1 ⊢ (⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))

Syntax hints:   ↔ wb 205   ∧ wa 396   ∨ wo 845   ∨ w3o 1086   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  Vcvv 3445  ⟨cotp 4594   class class class wbr 5105  {copab 5167   × cxp 5631  ‘cfv 6496  1^st c1st 7919  2^nd c2nd 7920

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-ot 4595  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-iota 6448  df-fun 6498  df-fv 6504  df-1st 7921  df-2nd 7922

This theorem is referenced by:  poxp3  8082  frxp3  8083  xpord3pred  8084