xpord3lem

Description: Lemma for triple ordering. Calculate the value of the relation. (Contributed by Scott Fenton, 21-Aug-2024)

		Ref	Expression
	Hypothesis	xpord3.1	⊢ 𝑈 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( ( 2^nd ‘ 𝑥 ) 𝑇 ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
	Assertion	xpord3lem	⊢ ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ 𝑈 ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		xpord3.1	⊢ 𝑈 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( ( 2^nd ‘ 𝑥 ) 𝑇 ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
2		otex	⊢ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∈ V
3		otex	⊢ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ V
4		eleq1	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) )
5		2fveq3	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( 1^st ‘ ( 1^st ‘ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) ) )
6		vex	⊢ 𝑎 ∈ V
7		vex	⊢ 𝑏 ∈ V
8		vex	⊢ 𝑐 ∈ V
9		ot1stg	⊢ ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V ) → ( 1^st ‘ ( 1^st ‘ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) ) = 𝑎 )
10	6 7 8 9	mp3an	⊢ ( 1^st ‘ ( 1^st ‘ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) ) = 𝑎
11	5 10	eqtrdi	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = 𝑎 )
12	11	breq1d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ↔ 𝑎 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) )
13	11	eqeq1d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ↔ 𝑎 = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) )
14	12 13	orbi12d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ↔ ( 𝑎 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑎 = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ) )
15		2fveq3	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) = ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) ) )
16		ot2ndg	⊢ ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ∧ 𝑐 ∈ V ) → ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) ) = 𝑏 )
17	6 7 8 16	mp3an	⊢ ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) ) = 𝑏
18	15 17	eqtrdi	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) = 𝑏 )
19	18	breq1d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ↔ 𝑏 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) )
20	18	eqeq1d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ↔ 𝑏 = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) )
21	19 20	orbi12d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ↔ ( 𝑏 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑏 = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ) )
22		fveq2	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) )
23		ot3rdg	⊢ ( 𝑐 ∈ V → ( 2^nd ‘ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) = 𝑐 )
24	23	elv	⊢ ( 2^nd ‘ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) = 𝑐
25	22 24	eqtrdi	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( 2^nd ‘ 𝑥 ) = 𝑐 )
26	25	breq1d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( ( 2^nd ‘ 𝑥 ) 𝑇 ( 2^nd ‘ 𝑦 ) ↔ 𝑐 𝑇 ( 2^nd ‘ 𝑦 ) ) )
27	25	eqeq1d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ↔ 𝑐 = ( 2^nd ‘ 𝑦 ) ) )
28	26 27	orbi12d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( ( ( 2^nd ‘ 𝑥 ) 𝑇 ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ↔ ( 𝑐 𝑇 ( 2^nd ‘ 𝑦 ) ∨ 𝑐 = ( 2^nd ‘ 𝑦 ) ) ) )
29	14 21 28	3anbi123d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( ( 2^nd ‘ 𝑥 ) 𝑇 ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ) ↔ ( ( 𝑎 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑎 = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑏 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑏 = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑐 𝑇 ( 2^nd ‘ 𝑦 ) ∨ 𝑐 = ( 2^nd ‘ 𝑦 ) ) ) ) )
30		neeq1	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( 𝑥 ≠ 𝑦 ↔ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ≠ 𝑦 ) )
31	29 30	anbi12d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( ( 2^nd ‘ 𝑥 ) 𝑇 ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ↔ ( ( ( 𝑎 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑎 = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑏 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑏 = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑐 𝑇 ( 2^nd ‘ 𝑦 ) ∨ 𝑐 = ( 2^nd ‘ 𝑦 ) ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ≠ 𝑦 ) ) )
32	4 31	3anbi13d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( ( 2^nd ‘ 𝑥 ) 𝑇 ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ) ↔ ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( 𝑎 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑎 = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑏 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑏 = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑐 𝑇 ( 2^nd ‘ 𝑦 ) ∨ 𝑐 = ( 2^nd ‘ 𝑦 ) ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ≠ 𝑦 ) ) ) )
33		eleq1	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) )
34		2fveq3	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) = ( 1^st ‘ ( 1^st ‘ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) ) )
35		vex	⊢ 𝑑 ∈ V
36		vex	⊢ 𝑒 ∈ V
37		vex	⊢ 𝑓 ∈ V
38		ot1stg	⊢ ( ( 𝑑 ∈ V ∧ 𝑒 ∈ V ∧ 𝑓 ∈ V ) → ( 1^st ‘ ( 1^st ‘ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) ) = 𝑑 )
39	35 36 37 38	mp3an	⊢ ( 1^st ‘ ( 1^st ‘ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) ) = 𝑑
40	34 39	eqtrdi	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) = 𝑑 )
41	40	breq2d	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 𝑎 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ↔ 𝑎 𝑅 𝑑 ) )
42	40	eqeq2d	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 𝑎 = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ↔ 𝑎 = 𝑑 ) )
43	41 42	orbi12d	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( ( 𝑎 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑎 = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ↔ ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ) )
44		2fveq3	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) = ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) ) )
45		ot2ndg	⊢ ( ( 𝑑 ∈ V ∧ 𝑒 ∈ V ∧ 𝑓 ∈ V ) → ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) ) = 𝑒 )
46	35 36 37 45	mp3an	⊢ ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) ) = 𝑒
47	44 46	eqtrdi	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) = 𝑒 )
48	47	breq2d	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 𝑏 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ↔ 𝑏 𝑆 𝑒 ) )
49	47	eqeq2d	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 𝑏 = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ↔ 𝑏 = 𝑒 ) )
50	48 49	orbi12d	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( ( 𝑏 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑏 = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ↔ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ) )
51		fveq2	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 2^nd ‘ 𝑦 ) = ( 2^nd ‘ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) )
52		ot3rdg	⊢ ( 𝑓 ∈ V → ( 2^nd ‘ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) = 𝑓 )
53	52	elv	⊢ ( 2^nd ‘ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) = 𝑓
54	51 53	eqtrdi	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 2^nd ‘ 𝑦 ) = 𝑓 )
55	54	breq2d	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 𝑐 𝑇 ( 2^nd ‘ 𝑦 ) ↔ 𝑐 𝑇 𝑓 ) )
56	54	eqeq2d	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 𝑐 = ( 2^nd ‘ 𝑦 ) ↔ 𝑐 = 𝑓 ) )
57	55 56	orbi12d	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( ( 𝑐 𝑇 ( 2^nd ‘ 𝑦 ) ∨ 𝑐 = ( 2^nd ‘ 𝑦 ) ) ↔ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) )
58	43 50 57	3anbi123d	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( ( ( 𝑎 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑎 = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑏 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑏 = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑐 𝑇 ( 2^nd ‘ 𝑦 ) ∨ 𝑐 = ( 2^nd ‘ 𝑦 ) ) ) ↔ ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ) )
59		neeq2	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ≠ 𝑦 ↔ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ≠ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) )
60	58 59	anbi12d	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( ( ( ( 𝑎 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑎 = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑏 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑏 = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑐 𝑇 ( 2^nd ‘ 𝑦 ) ∨ 𝑐 = ( 2^nd ‘ 𝑦 ) ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ≠ 𝑦 ) ↔ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ≠ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) ) )
61	33 60	3anbi23d	⊢ ( 𝑦 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( 𝑎 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑎 = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑏 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑏 = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑐 𝑇 ( 2^nd ‘ 𝑦 ) ∨ 𝑐 = ( 2^nd ‘ 𝑦 ) ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ≠ 𝑦 ) ) ↔ ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ≠ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) ) ) )
62	2 3 32 61 1	brab	⊢ ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ 𝑈 ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ↔ ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ≠ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) ) )
63		otelxp	⊢ ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) )
64		otelxp	⊢ ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) )
65	6 7 8	otthne	⊢ ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ≠ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ↔ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) )
66	65	anbi2i	⊢ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ≠ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) ↔ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) )
67	63 64 66	3anbi123i	⊢ ( ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ≠ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ) )
68	62 67	bitri	⊢ ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ 𝑈 ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ) )

Metamath Proof Explorer

Theorem xpord3lem

Proof