Metamath Proof Explorer

Theorem soxp

Description: A lexicographical ordering of two strictly ordered classes. (Contributed by Scott Fenton, 17-Mar-2011) (Revised by Mario Carneiro, 7-Mar-2013)

Ref Expression
Hypothesis soxp.1 ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ) ) ) }
Assertion soxp ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → 𝑇 Or ( 𝐴 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 soxp.1 ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ∧ ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ) ) ) }
2 sopo ⊢ ( 𝑅 Or 𝐴 → 𝑅 Po 𝐴 )
3 sopo ⊢ ( 𝑆 Or 𝐵 → 𝑆 Po 𝐵 )
4 1 poxp ⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → 𝑇 Po ( 𝐴 × 𝐵 ) )
5 2 3 4 syl2an ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → 𝑇 Po ( 𝐴 × 𝐵 ) )
6 elxp ⊢ ( 𝑡 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) )
7 elxp ⊢ ( 𝑢 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑐 ∃ 𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) )
8 ioran ⊢ ( ¬ ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) ↔ ( ¬ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∧ ¬ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) )
9 ioran ⊢ ( ¬ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ↔ ( ¬ 𝑎 𝑅 𝑐 ∧ ¬ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) )
10 ianor ⊢ ( ¬ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ↔ ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 𝑆 𝑑 ) )
11 10 anbi2i ⊢ ( ( ¬ 𝑎 𝑅 𝑐 ∧ ¬ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ↔ ( ¬ 𝑎 𝑅 𝑐 ∧ ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 𝑆 𝑑 ) ) )
12 9 11 bitri ⊢ ( ¬ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ↔ ( ¬ 𝑎 𝑅 𝑐 ∧ ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 𝑆 𝑑 ) ) )
13 ianor ⊢ ( ¬ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ↔ ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑 ) )
14 12 13 anbi12i ⊢ ( ( ¬ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∧ ¬ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) ↔ ( ( ¬ 𝑎 𝑅 𝑐 ∧ ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 𝑆 𝑑 ) ) ∧ ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑 ) ) )
15 8 14 bitri ⊢ ( ¬ ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) ↔ ( ( ¬ 𝑎 𝑅 𝑐 ∧ ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 𝑆 𝑑 ) ) ∧ ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑 ) ) )
16 solin ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) → ( 𝑎 𝑅 𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) )
17 3orass ⊢ ( ( 𝑎 𝑅 𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) ↔ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) ) )
18 df-or ⊢ ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) ) ↔ ( ¬ 𝑎 𝑅 𝑐 → ( 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) ) )
19 17 18 bitri ⊢ ( ( 𝑎 𝑅 𝑐 ∨ 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) ↔ ( ¬ 𝑎 𝑅 𝑐 → ( 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) ) )
20 16 19 sylib ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) → ( ¬ 𝑎 𝑅 𝑐 → ( 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) ) )
21 solin ⊢ ( ( 𝑆 Or 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) → ( 𝑏 𝑆 𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑 𝑆 𝑏 ) )
22 3orass ⊢ ( ( 𝑏 𝑆 𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑 𝑆 𝑏 ) ↔ ( 𝑏 𝑆 𝑑 ∨ ( 𝑏 = 𝑑 ∨ 𝑑 𝑆 𝑏 ) ) )
23 df-or ⊢ ( ( 𝑏 𝑆 𝑑 ∨ ( 𝑏 = 𝑑 ∨ 𝑑 𝑆 𝑏 ) ) ↔ ( ¬ 𝑏 𝑆 𝑑 → ( 𝑏 = 𝑑 ∨ 𝑑 𝑆 𝑏 ) ) )
24 22 23 bitri ⊢ ( ( 𝑏 𝑆 𝑑 ∨ 𝑏 = 𝑑 ∨ 𝑑 𝑆 𝑏 ) ↔ ( ¬ 𝑏 𝑆 𝑑 → ( 𝑏 = 𝑑 ∨ 𝑑 𝑆 𝑏 ) ) )
25 21 24 sylib ⊢ ( ( 𝑆 Or 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) → ( ¬ 𝑏 𝑆 𝑑 → ( 𝑏 = 𝑑 ∨ 𝑑 𝑆 𝑏 ) ) )
26 25 orim2d ⊢ ( ( 𝑆 Or 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 𝑆 𝑑 ) → ( ¬ 𝑎 = 𝑐 ∨ ( 𝑏 = 𝑑 ∨ 𝑑 𝑆 𝑏 ) ) ) )
27 20 26 im2anan9 ⊢ ( ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( 𝑆 Or 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ) → ( ( ¬ 𝑎 𝑅 𝑐 ∧ ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 𝑆 𝑑 ) ) → ( ( 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) ∧ ( ¬ 𝑎 = 𝑐 ∨ ( 𝑏 = 𝑑 ∨ 𝑑 𝑆 𝑏 ) ) ) ) )
28 pm2.53 ⊢ ( ( 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) → ( ¬ 𝑎 = 𝑐 → 𝑐 𝑅 𝑎 ) )
29 orc ⊢ ( 𝑐 𝑅 𝑎 → ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) )
30 28 29 syl6 ⊢ ( ( 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) → ( ¬ 𝑎 = 𝑐 → ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) )
31 30 adantr ⊢ ( ( ( 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) ∧ ( ¬ 𝑎 = 𝑐 ∨ ( 𝑏 = 𝑑 ∨ 𝑑 𝑆 𝑏 ) ) ) → ( ¬ 𝑎 = 𝑐 → ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) )
32 orel1 ⊢ ( ¬ 𝑏 = 𝑑 → ( ( 𝑏 = 𝑑 ∨ 𝑑 𝑆 𝑏 ) → 𝑑 𝑆 𝑏 ) )
33 32 orim2d ⊢ ( ¬ 𝑏 = 𝑑 → ( ( ¬ 𝑎 = 𝑐 ∨ ( 𝑏 = 𝑑 ∨ 𝑑 𝑆 𝑏 ) ) → ( ¬ 𝑎 = 𝑐 ∨ 𝑑 𝑆 𝑏 ) ) )
34 33 anim2d ⊢ ( ¬ 𝑏 = 𝑑 → ( ( ( 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) ∧ ( ¬ 𝑎 = 𝑐 ∨ ( 𝑏 = 𝑑 ∨ 𝑑 𝑆 𝑏 ) ) ) → ( ( 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) ∧ ( ¬ 𝑎 = 𝑐 ∨ 𝑑 𝑆 𝑏 ) ) ) )
35 imor ⊢ ( ( 𝑎 = 𝑐 → 𝑑 𝑆 𝑏 ) ↔ ( ¬ 𝑎 = 𝑐 ∨ 𝑑 𝑆 𝑏 ) )
36 35 biimpri ⊢ ( ( ¬ 𝑎 = 𝑐 ∨ 𝑑 𝑆 𝑏 ) → ( 𝑎 = 𝑐 → 𝑑 𝑆 𝑏 ) )
37 36 com12 ⊢ ( 𝑎 = 𝑐 → ( ( ¬ 𝑎 = 𝑐 ∨ 𝑑 𝑆 𝑏 ) → 𝑑 𝑆 𝑏 ) )
38 equcomi ⊢ ( 𝑎 = 𝑐 → 𝑐 = 𝑎 )
39 38 anim1i ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑑 𝑆 𝑏 ) → ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) )
40 39 olcd ⊢ ( ( 𝑎 = 𝑐 ∧ 𝑑 𝑆 𝑏 ) → ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) )
41 40 ex ⊢ ( 𝑎 = 𝑐 → ( 𝑑 𝑆 𝑏 → ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) )
42 37 41 syld ⊢ ( 𝑎 = 𝑐 → ( ( ¬ 𝑎 = 𝑐 ∨ 𝑑 𝑆 𝑏 ) → ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) )
43 29 a1d ⊢ ( 𝑐 𝑅 𝑎 → ( ( ¬ 𝑎 = 𝑐 ∨ 𝑑 𝑆 𝑏 ) → ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) )
44 42 43 jaoi ⊢ ( ( 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) → ( ( ¬ 𝑎 = 𝑐 ∨ 𝑑 𝑆 𝑏 ) → ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) )
45 44 imp ⊢ ( ( ( 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) ∧ ( ¬ 𝑎 = 𝑐 ∨ 𝑑 𝑆 𝑏 ) ) → ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) )
46 34 45 syl6com ⊢ ( ( ( 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) ∧ ( ¬ 𝑎 = 𝑐 ∨ ( 𝑏 = 𝑑 ∨ 𝑑 𝑆 𝑏 ) ) ) → ( ¬ 𝑏 = 𝑑 → ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) )
47 31 46 jaod ⊢ ( ( ( 𝑎 = 𝑐 ∨ 𝑐 𝑅 𝑎 ) ∧ ( ¬ 𝑎 = 𝑐 ∨ ( 𝑏 = 𝑑 ∨ 𝑑 𝑆 𝑏 ) ) ) → ( ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑 ) → ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) )
48 27 47 syl6 ⊢ ( ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( 𝑆 Or 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ) → ( ( ¬ 𝑎 𝑅 𝑐 ∧ ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 𝑆 𝑑 ) ) → ( ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑 ) → ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) ) )
49 48 impd ⊢ ( ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( 𝑆 Or 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ) → ( ( ( ¬ 𝑎 𝑅 𝑐 ∧ ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 𝑆 𝑑 ) ) ∧ ( ¬ 𝑎 = 𝑐 ∨ ¬ 𝑏 = 𝑑 ) ) → ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) )
50 15 49 syl5bi ⊢ ( ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( 𝑆 Or 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ) → ( ¬ ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) → ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) )
51 df-3or ⊢ ( ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ∨ ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) ↔ ( ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) ∨ ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) )
52 df-or ⊢ ( ( ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) ∨ ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) ↔ ( ¬ ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) → ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) )
53 51 52 bitri ⊢ ( ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ∨ ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) ↔ ( ¬ ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) → ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) )
54 50 53 sylibr ⊢ ( ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( 𝑆 Or 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ) → ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ∨ ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) )
55 pm3.2 ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ) )
56 55 ad2ant2l ⊢ ( ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( 𝑆 Or 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ) → ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ) )
57 idd ⊢ ( ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( 𝑆 Or 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ) → ( ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) → ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ) )
58 simpr ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) → ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) )
59 58 ancomd ⊢ ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) → ( 𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) )
60 simpr ⊢ ( ( 𝑆 Or 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) → ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) )
61 60 ancomd ⊢ ( ( 𝑆 Or 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) → ( 𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) )
62 pm3.2 ⊢ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) → ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) ) )
63 59 61 62 syl2an ⊢ ( ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( 𝑆 Or 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ) → ( ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) → ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) ) )
64 56 57 63 3orim123d ⊢ ( ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( 𝑆 Or 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ) → ( ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ∨ ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) → ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ∨ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) ) ) )
65 54 64 mpd ⊢ ( ( ( 𝑅 Or 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ) ∧ ( 𝑆 Or 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ) → ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ∨ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) ) )
66 65 an4s ⊢ ( ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ) → ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ∨ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) ) )
67 66 expcom ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ∨ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) ) ) )
68 67 an4s ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ∨ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) ) ) )
69 breq12 ⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ) → ( 𝑡 𝑇 𝑢 ↔ ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ) )
70 eqeq12 ⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ) → ( 𝑡 = 𝑢 ↔ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ) )
71 breq12 ⊢ ( ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ) → ( 𝑢 𝑇 𝑡 ↔ ⟨ 𝑐 , 𝑑 ⟩ 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) )
72 71 ancoms ⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ) → ( 𝑢 𝑇 𝑡 ↔ ⟨ 𝑐 , 𝑑 ⟩ 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) )
73 69 70 72 3orbi123d ⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ) → ( ( 𝑡 𝑇 𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢 𝑇 𝑡 ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ∨ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∨ ⟨ 𝑐 , 𝑑 ⟩ 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) ) )
74 1 xporderlem ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ↔ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) )
75 vex ⊢ 𝑎 ∈ V
76 vex ⊢ 𝑏 ∈ V
77 75 76 opth ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ↔ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) )
78 1 xporderlem ⊢ ( ⟨ 𝑐 , 𝑑 ⟩ 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ↔ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) )
79 74 77 78 3orbi123i ⊢ ( ( ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ∨ ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑐 , 𝑑 ⟩ ∨ ⟨ 𝑐 , 𝑑 ⟩ 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ∨ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) ) )
80 73 79 bitrdi ⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ) → ( ( 𝑡 𝑇 𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢 𝑇 𝑡 ) ↔ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ∨ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) ) ) )
81 80 biimprcd ⊢ ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ∨ ( 𝑎 = 𝑐 ∧ 𝑏 = 𝑑 ) ∨ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑎 ∨ ( 𝑐 = 𝑎 ∧ 𝑑 𝑆 𝑏 ) ) ) ) → ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ) → ( 𝑡 𝑇 𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢 𝑇 𝑡 ) ) )
82 68 81 syl6 ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ) → ( 𝑡 𝑇 𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢 𝑇 𝑡 ) ) ) )
83 82 com3r ⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → ( 𝑡 𝑇 𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢 𝑇 𝑡 ) ) ) )
84 83 imp ⊢ ( ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) ) → ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → ( 𝑡 𝑇 𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢 𝑇 𝑡 ) ) )
85 84 an4s ⊢ ( ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) ) → ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → ( 𝑡 𝑇 𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢 𝑇 𝑡 ) ) )
86 85 expcom ⊢ ( ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → ( 𝑡 𝑇 𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢 𝑇 𝑡 ) ) ) )
87 86 exlimivv ⊢ ( ∃ 𝑐 ∃ 𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → ( 𝑡 𝑇 𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢 𝑇 𝑡 ) ) ) )
88 87 com12 ⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ∃ 𝑐 ∃ 𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → ( 𝑡 𝑇 𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢 𝑇 𝑡 ) ) ) )
89 88 exlimivv ⊢ ( ∃ 𝑎 ∃ 𝑏 ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ∃ 𝑐 ∃ 𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → ( 𝑡 𝑇 𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢 𝑇 𝑡 ) ) ) )
90 89 imp ⊢ ( ( ∃ 𝑎 ∃ 𝑏 ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∃ 𝑐 ∃ 𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) ) → ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → ( 𝑡 𝑇 𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢 𝑇 𝑡 ) ) )
91 6 7 90 syl2anb ⊢ ( ( 𝑡 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑢 ∈ ( 𝐴 × 𝐵 ) ) → ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → ( 𝑡 𝑇 𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢 𝑇 𝑡 ) ) )
92 91 com12 ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → ( ( 𝑡 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑢 ∈ ( 𝐴 × 𝐵 ) ) → ( 𝑡 𝑇 𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢 𝑇 𝑡 ) ) )
93 92 ralrimivv ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → ∀ 𝑡 ∈ ( 𝐴 × 𝐵 ) ∀ 𝑢 ∈ ( 𝐴 × 𝐵 ) ( 𝑡 𝑇 𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢 𝑇 𝑡 ) )
94 df-so ⊢ ( 𝑇 Or ( 𝐴 × 𝐵 ) ↔ ( 𝑇 Po ( 𝐴 × 𝐵 ) ∧ ∀ 𝑡 ∈ ( 𝐴 × 𝐵 ) ∀ 𝑢 ∈ ( 𝐴 × 𝐵 ) ( 𝑡 𝑇 𝑢 ∨ 𝑡 = 𝑢 ∨ 𝑢 𝑇 𝑡 ) ) )
95 5 93 94 sylanbrc ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → 𝑇 Or ( 𝐴 × 𝐵 ) )