xpord3lem

Description: Lemma for triple ordering. Calculate the value of the relationship. (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		opex	⊢ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∈ V
3		opex	⊢ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ V
4		eleq1	⊢ ( 𝑥 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) )
5		vex	⊢ 𝑎 ∈ V
6		vex	⊢ 𝑏 ∈ V
7		vex	⊢ 𝑐 ∈ V
8	5 6 7	ot21std	⊢ ( 𝑥 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = 𝑎 )
9	8	breq1d	⊢ ( 𝑥 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ↔ 𝑎 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) )
10	8	eqeq1d	⊢ ( 𝑥 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ↔ 𝑎 = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) )
11	9 10	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 ‘ 𝑦 ) ) ) ) )
12	5 6 7	ot22ndd	⊢ ( 𝑥 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) = 𝑏 )
13	12	breq1d	⊢ ( 𝑥 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ↔ 𝑏 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) )
14	12	eqeq1d	⊢ ( 𝑥 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ↔ 𝑏 = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) )
15	13 14	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 ‘ 𝑦 ) ) ) ) )
16		opex	⊢ ⟨ 𝑎 , 𝑏 ⟩ ∈ V
17	16 7	op2ndd	⊢ ( 𝑥 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → ( 2^nd ‘ 𝑥 ) = 𝑐 )
18	17	breq1d	⊢ ( 𝑥 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → ( ( 2^nd ‘ 𝑥 ) 𝑇 ( 2^nd ‘ 𝑦 ) ↔ 𝑐 𝑇 ( 2^nd ‘ 𝑦 ) ) )
19	17	eqeq1d	⊢ ( 𝑥 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → ( ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ↔ 𝑐 = ( 2^nd ‘ 𝑦 ) ) )
20	18 19	orbi12d	⊢ ( 𝑥 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → ( ( ( 2^nd ‘ 𝑥 ) 𝑇 ( 2^nd ‘ 𝑦 ) ∨ ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑦 ) ) ↔ ( 𝑐 𝑇 ( 2^nd ‘ 𝑦 ) ∨ 𝑐 = ( 2^nd ‘ 𝑦 ) ) ) )
21	11 15 20	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 ‘ 𝑦 ) ) ) ) )
22		neeq1	⊢ ( 𝑥 = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ → ( 𝑥 ≠ 𝑦 ↔ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ≠ 𝑦 ) )
23	21 22	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 ‘ 𝑦 ) ) ) ∧ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ≠ 𝑦 ) ) )
24	4 23	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 ‘ 𝑦 ) ) ) ∧ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ≠ 𝑦 ) ) ) )
25		eleq1	⊢ ( 𝑦 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) )
26		vex	⊢ 𝑑 ∈ V
27		vex	⊢ 𝑒 ∈ V
28		vex	⊢ 𝑓 ∈ V
29	26 27 28	ot21std	⊢ ( 𝑦 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) = 𝑑 )
30	29	breq2d	⊢ ( 𝑦 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 𝑎 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ↔ 𝑎 𝑅 𝑑 ) )
31	29	eqeq2d	⊢ ( 𝑦 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 𝑎 = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ↔ 𝑎 = 𝑑 ) )
32	30 31	orbi12d	⊢ ( 𝑦 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( ( 𝑎 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑎 = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ↔ ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ) )
33	26 27 28	ot22ndd	⊢ ( 𝑦 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) = 𝑒 )
34	33	breq2d	⊢ ( 𝑦 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 𝑏 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ↔ 𝑏 𝑆 𝑒 ) )
35	33	eqeq2d	⊢ ( 𝑦 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 𝑏 = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ↔ 𝑏 = 𝑒 ) )
36	34 35	orbi12d	⊢ ( 𝑦 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( ( 𝑏 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑏 = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ↔ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ) )
37		opex	⊢ ⟨ 𝑑 , 𝑒 ⟩ ∈ V
38	37 28	op2ndd	⊢ ( 𝑦 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 2^nd ‘ 𝑦 ) = 𝑓 )
39	38	breq2d	⊢ ( 𝑦 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 𝑐 𝑇 ( 2^nd ‘ 𝑦 ) ↔ 𝑐 𝑇 𝑓 ) )
40	38	eqeq2d	⊢ ( 𝑦 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 𝑐 = ( 2^nd ‘ 𝑦 ) ↔ 𝑐 = 𝑓 ) )
41	39 40	orbi12d	⊢ ( 𝑦 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( ( 𝑐 𝑇 ( 2^nd ‘ 𝑦 ) ∨ 𝑐 = ( 2^nd ‘ 𝑦 ) ) ↔ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) )
42	32 36 41	3anbi123d	⊢ ( 𝑦 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( ( ( 𝑎 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑎 = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑏 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑏 = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑐 𝑇 ( 2^nd ‘ 𝑦 ) ∨ 𝑐 = ( 2^nd ‘ 𝑦 ) ) ) ↔ ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ) )
43		neeq2	⊢ ( 𝑦 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ≠ 𝑦 ↔ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ≠ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ) )
44	42 43	anbi12d	⊢ ( 𝑦 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( ( ( ( 𝑎 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑎 = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑏 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑏 = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑐 𝑇 ( 2^nd ‘ 𝑦 ) ∨ 𝑐 = ( 2^nd ‘ 𝑦 ) ) ) ∧ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ≠ 𝑦 ) ↔ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ≠ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ) ) )
45	25 44	3anbi23d	⊢ ( 𝑦 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( ( ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( 𝑎 𝑅 ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑎 = ( 1^st ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑏 𝑆 ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ∨ 𝑏 = ( 2^nd ‘ ( 1^st ‘ 𝑦 ) ) ) ∧ ( 𝑐 𝑇 ( 2^nd ‘ 𝑦 ) ∨ 𝑐 = ( 2^nd ‘ 𝑦 ) ) ) ∧ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ≠ 𝑦 ) ) ↔ ( ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ≠ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ) ) ) )
46	2 3 24 45 1	brab	⊢ ( ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ 𝑈 ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ↔ ( ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ≠ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ) ) )
47		ot2elxp	⊢ ( ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) )
48		ot2elxp	⊢ ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) )
49	5 6 7	otthne	⊢ ( ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ≠ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ↔ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) )
50	49	anbi2i	⊢ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ≠ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ) ↔ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) )
51	47 48 50	3anbi123i	⊢ ( ( ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ≠ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ) ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ) )
52	46 51	bitri	⊢ ( ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ 𝑈 ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ) )

Metamath Proof Explorer

Theorem xpord3lem

Proof