Metamath Proof Explorer


Theorem xpord2lem

Description: Lemma for cross product ordering. Calculate the value of the cross product relationship. (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 ( ⟨ 𝑎 , 𝑏𝑇𝑐 , 𝑑 ⟩ ↔ ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ∧ ( ( 𝑎 𝑅 𝑐𝑎 = 𝑐 ) ∧ ( 𝑏 𝑆 𝑑𝑏 = 𝑑 ) ∧ ( 𝑎𝑐𝑏𝑑 ) ) ) )