Theorem xpord2lem

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

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

Proof

Step	Hyp	Ref	Expression
1		xpord2.1	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
2		opex	⊢ ⟨ 𝑎 , 𝑏 ⟩ ∈ V
3		opex	⊢ ⟨ 𝑐 , 𝑑 ⟩ ∈ V
4		eleq1	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
5		opelxp	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) )
6	4 5	bitrdi	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) )
7		vex	⊢ 𝑎 ∈ V
8		vex	⊢ 𝑏 ∈ V
9	7 8	op1std	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 1st ‘ 𝑥 ) = 𝑎 )
10	9	breq1d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ↔ 𝑎 𝑅 ( 1st ‘ 𝑦 ) ) )
11	9	eqeq1d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ↔ 𝑎 = ( 1st ‘ 𝑦 ) ) )
12	10 11	orbi12d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ↔ ( 𝑎 𝑅 ( 1st ‘ 𝑦 ) ∨ 𝑎 = ( 1st ‘ 𝑦 ) ) ) )
13	7 8	op2ndd	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 2nd ‘ 𝑥 ) = 𝑏 )
14	13	breq1d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ↔ 𝑏 𝑆 ( 2nd ‘ 𝑦 ) ) )
15	13	eqeq1d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ↔ 𝑏 = ( 2nd ‘ 𝑦 ) ) )
16	14 15	orbi12d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ↔ ( 𝑏 𝑆 ( 2nd ‘ 𝑦 ) ∨ 𝑏 = ( 2nd ‘ 𝑦 ) ) ) )
17		neeq1	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑥 ≠ 𝑦 ↔ ⟨ 𝑎 , 𝑏 ⟩ ≠ 𝑦 ) )
18	12 16 17	3anbi123d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ↔ ( ( 𝑎 𝑅 ( 1st ‘ 𝑦 ) ∨ 𝑎 = ( 1st ‘ 𝑦 ) ) ∧ ( 𝑏 𝑆 ( 2nd ‘ 𝑦 ) ∨ 𝑏 = ( 2nd ‘ 𝑦 ) ) ∧ ⟨ 𝑎 , 𝑏 ⟩ ≠ 𝑦 ) ) )
19	6 18	3anbi13d	⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( 𝑎 𝑅 ( 1st ‘ 𝑦 ) ∨ 𝑎 = ( 1st ‘ 𝑦 ) ) ∧ ( 𝑏 𝑆 ( 2nd ‘ 𝑦 ) ∨ 𝑏 = ( 2nd ‘ 𝑦 ) ) ∧ ⟨ 𝑎 , 𝑏 ⟩ ≠ 𝑦 ) ) ) )
20		eleq1	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑦 ∈ ( 𝐴 × 𝐵 ) ↔ ⟨ 𝑐 , 𝑑 ⟩ ∈ ( 𝐴 × 𝐵 ) ) )
21		opelxp	⊢ ( ⟨ 𝑐 , 𝑑 ⟩ ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) )
22	20 21	bitrdi	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑦 ∈ ( 𝐴 × 𝐵 ) ↔ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) )
23		vex	⊢ 𝑐 ∈ V
24		vex	⊢ 𝑑 ∈ V
25	23 24	op1std	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( 1st ‘ 𝑦 ) = 𝑐 )
26	25	breq2d	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑎 𝑅 ( 1st ‘ 𝑦 ) ↔ 𝑎 𝑅 𝑐 ) )
27	25	eqeq2d	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑎 = ( 1st ‘ 𝑦 ) ↔ 𝑎 = 𝑐 ) )
28	26 27	orbi12d	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( 𝑎 𝑅 ( 1st ‘ 𝑦 ) ∨ 𝑎 = ( 1st ‘ 𝑦 ) ) ↔ ( 𝑎 𝑅 𝑐 ∨ 𝑎 = 𝑐 ) ) )
29	23 24	op2ndd	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( 2nd ‘ 𝑦 ) = 𝑑 )
30	29	breq2d	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑏 𝑆 ( 2nd ‘ 𝑦 ) ↔ 𝑏 𝑆 𝑑 ) )
31	29	eqeq2d	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( 𝑏 = ( 2nd ‘ 𝑦 ) ↔ 𝑏 = 𝑑 ) )
32	30 31	orbi12d	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( 𝑏 𝑆 ( 2nd ‘ 𝑦 ) ∨ 𝑏 = ( 2nd ‘ 𝑦 ) ) ↔ ( 𝑏 𝑆 𝑑 ∨ 𝑏 = 𝑑 ) ) )
33		neeq2	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( ⟨ 𝑎 , 𝑏 ⟩ ≠ 𝑦 ↔ ⟨ 𝑎 , 𝑏 ⟩ ≠ ⟨ 𝑐 , 𝑑 ⟩ ) )
34	7 8	opthne	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ≠ ⟨ 𝑐 , 𝑑 ⟩ ↔ ( 𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑 ) )
35	33 34	bitrdi	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( ⟨ 𝑎 , 𝑏 ⟩ ≠ 𝑦 ↔ ( 𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑 ) ) )
36	28 32 35	3anbi123d	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( ( 𝑎 𝑅 ( 1st ‘ 𝑦 ) ∨ 𝑎 = ( 1st ‘ 𝑦 ) ) ∧ ( 𝑏 𝑆 ( 2nd ‘ 𝑦 ) ∨ 𝑏 = ( 2nd ‘ 𝑦 ) ) ∧ ⟨ 𝑎 , 𝑏 ⟩ ≠ 𝑦 ) ↔ ( ( 𝑎 𝑅 𝑐 ∨ 𝑎 = 𝑐 ) ∧ ( 𝑏 𝑆 𝑑 ∨ 𝑏 = 𝑑 ) ∧ ( 𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑 ) ) ) )
37	22 36	3anbi23d	⊢ ( 𝑦 = ⟨ 𝑐 , 𝑑 ⟩ → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( 𝑎 𝑅 ( 1st ‘ 𝑦 ) ∨ 𝑎 = ( 1st ‘ 𝑦 ) ) ∧ ( 𝑏 𝑆 ( 2nd ‘ 𝑦 ) ∨ 𝑏 = ( 2nd ‘ 𝑦 ) ) ∧ ⟨ 𝑎 , 𝑏 ⟩ ≠ 𝑦 ) ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( ( 𝑎 𝑅 𝑐 ∨ 𝑎 = 𝑐 ) ∧ ( 𝑏 𝑆 𝑑 ∨ 𝑏 = 𝑑 ) ∧ ( 𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑 ) ) ) ) )
38	2 3 19 37 1	brab	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( ( 𝑎 𝑅 𝑐 ∨ 𝑎 = 𝑐 ) ∧ ( 𝑏 𝑆 𝑑 ∨ 𝑏 = 𝑑 ) ∧ ( 𝑎 ≠ 𝑐 ∨ 𝑏 ≠ 𝑑 ) ) ) )