Metamath Proof Explorer


Theorem poxp

Description: A lexicographical ordering of two posets. (Contributed by Scott Fenton, 16-Mar-2011) (Revised by Mario Carneiro, 7-Mar-2013)

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

Proof

Step Hyp Ref Expression
1 poxp.1 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1st𝑥 ) 𝑅 ( 1st𝑦 ) ∨ ( ( 1st𝑥 ) = ( 1st𝑦 ) ∧ ( 2nd𝑥 ) 𝑆 ( 2nd𝑦 ) ) ) ) }
2 elxp ( 𝑡 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑎𝑏 ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎𝐴𝑏𝐵 ) ) )
3 elxp ( 𝑢 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑐𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐𝐴𝑑𝐵 ) ) )
4 elxp ( 𝑣 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑒𝑓 ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒𝐴𝑓𝐵 ) ) )
5 3an6 ( ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎𝐴𝑏𝐵 ) ) ∧ ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐𝐴𝑑𝐵 ) ) ∧ ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒𝐴𝑓𝐵 ) ) ) ↔ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) ∧ ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑒𝐴𝑓𝐵 ) ) ) )
6 poirr ( ( 𝑅 Po 𝐴𝑎𝐴 ) → ¬ 𝑎 𝑅 𝑎 )
7 6 ex ( 𝑅 Po 𝐴 → ( 𝑎𝐴 → ¬ 𝑎 𝑅 𝑎 ) )
8 poirr ( ( 𝑆 Po 𝐵𝑏𝐵 ) → ¬ 𝑏 𝑆 𝑏 )
9 8 intnand ( ( 𝑆 Po 𝐵𝑏𝐵 ) → ¬ ( 𝑎 = 𝑎𝑏 𝑆 𝑏 ) )
10 9 ex ( 𝑆 Po 𝐵 → ( 𝑏𝐵 → ¬ ( 𝑎 = 𝑎𝑏 𝑆 𝑏 ) ) )
11 7 10 im2anan9 ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → ( ( 𝑎𝐴𝑏𝐵 ) → ( ¬ 𝑎 𝑅 𝑎 ∧ ¬ ( 𝑎 = 𝑎𝑏 𝑆 𝑏 ) ) ) )
12 ioran ( ¬ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎𝑏 𝑆 𝑏 ) ) ↔ ( ¬ 𝑎 𝑅 𝑎 ∧ ¬ ( 𝑎 = 𝑎𝑏 𝑆 𝑏 ) ) )
13 11 12 syl6ibr ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → ( ( 𝑎𝐴𝑏𝐵 ) → ¬ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎𝑏 𝑆 𝑏 ) ) ) )
14 13 imp ( ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) ∧ ( 𝑎𝐴𝑏𝐵 ) ) → ¬ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎𝑏 𝑆 𝑏 ) ) )
15 14 intnand ( ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) ∧ ( 𝑎𝐴𝑏𝐵 ) ) → ¬ ( ( ( 𝑎𝐴𝑎𝐴 ) ∧ ( 𝑏𝐵𝑏𝐵 ) ) ∧ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎𝑏 𝑆 𝑏 ) ) ) )
16 15 3ad2antr1 ( ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) ∧ ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑒𝐴𝑓𝐵 ) ) ) → ¬ ( ( ( 𝑎𝐴𝑎𝐴 ) ∧ ( 𝑏𝐵𝑏𝐵 ) ) ∧ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎𝑏 𝑆 𝑏 ) ) ) )
17 an4 ( ( ( ( ( 𝑎𝐴𝑐𝐴 ) ∧ ( 𝑏𝐵𝑑𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐𝑏 𝑆 𝑑 ) ) ) ∧ ( ( ( 𝑐𝐴𝑒𝐴 ) ∧ ( 𝑑𝐵𝑓𝐵 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) ) ) ↔ ( ( ( ( 𝑎𝐴𝑐𝐴 ) ∧ ( 𝑏𝐵𝑑𝐵 ) ) ∧ ( ( 𝑐𝐴𝑒𝐴 ) ∧ ( 𝑑𝐵𝑓𝐵 ) ) ) ∧ ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐𝑏 𝑆 𝑑 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) ) ) )
18 3an6 ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑒𝐴𝑓𝐵 ) ) ↔ ( ( 𝑎𝐴𝑐𝐴𝑒𝐴 ) ∧ ( 𝑏𝐵𝑑𝐵𝑓𝐵 ) ) )
19 potr ( ( 𝑅 Po 𝐴 ∧ ( 𝑎𝐴𝑐𝐴𝑒𝐴 ) ) → ( ( 𝑎 𝑅 𝑐𝑐 𝑅 𝑒 ) → 𝑎 𝑅 𝑒 ) )
20 19 3impia ( ( 𝑅 Po 𝐴 ∧ ( 𝑎𝐴𝑐𝐴𝑒𝐴 ) ∧ ( 𝑎 𝑅 𝑐𝑐 𝑅 𝑒 ) ) → 𝑎 𝑅 𝑒 )
21 20 orcd ( ( 𝑅 Po 𝐴 ∧ ( 𝑎𝐴𝑐𝐴𝑒𝐴 ) ∧ ( 𝑎 𝑅 𝑐𝑐 𝑅 𝑒 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) )
22 21 3expia ( ( 𝑅 Po 𝐴 ∧ ( 𝑎𝐴𝑐𝐴𝑒𝐴 ) ) → ( ( 𝑎 𝑅 𝑐𝑐 𝑅 𝑒 ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) )
23 22 expdimp ( ( ( 𝑅 Po 𝐴 ∧ ( 𝑎𝐴𝑐𝐴𝑒𝐴 ) ) ∧ 𝑎 𝑅 𝑐 ) → ( 𝑐 𝑅 𝑒 → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) )
24 breq2 ( 𝑐 = 𝑒 → ( 𝑎 𝑅 𝑐𝑎 𝑅 𝑒 ) )
25 24 biimpa ( ( 𝑐 = 𝑒𝑎 𝑅 𝑐 ) → 𝑎 𝑅 𝑒 )
26 25 orcd ( ( 𝑐 = 𝑒𝑎 𝑅 𝑐 ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) )
27 26 expcom ( 𝑎 𝑅 𝑐 → ( 𝑐 = 𝑒 → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) )
28 27 adantrd ( 𝑎 𝑅 𝑐 → ( ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) )
29 28 adantl ( ( ( 𝑅 Po 𝐴 ∧ ( 𝑎𝐴𝑐𝐴𝑒𝐴 ) ) ∧ 𝑎 𝑅 𝑐 ) → ( ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) )
30 23 29 jaod ( ( ( 𝑅 Po 𝐴 ∧ ( 𝑎𝐴𝑐𝐴𝑒𝐴 ) ) ∧ 𝑎 𝑅 𝑐 ) → ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) )
31 30 ex ( ( 𝑅 Po 𝐴 ∧ ( 𝑎𝐴𝑐𝐴𝑒𝐴 ) ) → ( 𝑎 𝑅 𝑐 → ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) ) )
32 potr ( ( 𝑆 Po 𝐵 ∧ ( 𝑏𝐵𝑑𝐵𝑓𝐵 ) ) → ( ( 𝑏 𝑆 𝑑𝑑 𝑆 𝑓 ) → 𝑏 𝑆 𝑓 ) )
33 32 expdimp ( ( ( 𝑆 Po 𝐵 ∧ ( 𝑏𝐵𝑑𝐵𝑓𝐵 ) ) ∧ 𝑏 𝑆 𝑑 ) → ( 𝑑 𝑆 𝑓𝑏 𝑆 𝑓 ) )
34 33 anim2d ( ( ( 𝑆 Po 𝐵 ∧ ( 𝑏𝐵𝑑𝐵𝑓𝐵 ) ) ∧ 𝑏 𝑆 𝑑 ) → ( ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) → ( 𝑐 = 𝑒𝑏 𝑆 𝑓 ) ) )
35 34 orim2d ( ( ( 𝑆 Po 𝐵 ∧ ( 𝑏𝐵𝑑𝐵𝑓𝐵 ) ) ∧ 𝑏 𝑆 𝑑 ) → ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) → ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑏 𝑆 𝑓 ) ) ) )
36 breq1 ( 𝑎 = 𝑐 → ( 𝑎 𝑅 𝑒𝑐 𝑅 𝑒 ) )
37 equequ1 ( 𝑎 = 𝑐 → ( 𝑎 = 𝑒𝑐 = 𝑒 ) )
38 37 anbi1d ( 𝑎 = 𝑐 → ( ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ↔ ( 𝑐 = 𝑒𝑏 𝑆 𝑓 ) ) )
39 36 38 orbi12d ( 𝑎 = 𝑐 → ( ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ↔ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑏 𝑆 𝑓 ) ) ) )
40 39 imbi2d ( 𝑎 = 𝑐 → ( ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) ↔ ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) → ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑏 𝑆 𝑓 ) ) ) ) )
41 35 40 syl5ibr ( 𝑎 = 𝑐 → ( ( ( 𝑆 Po 𝐵 ∧ ( 𝑏𝐵𝑑𝐵𝑓𝐵 ) ) ∧ 𝑏 𝑆 𝑑 ) → ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) ) )
42 41 expd ( 𝑎 = 𝑐 → ( ( 𝑆 Po 𝐵 ∧ ( 𝑏𝐵𝑑𝐵𝑓𝐵 ) ) → ( 𝑏 𝑆 𝑑 → ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) ) ) )
43 42 com12 ( ( 𝑆 Po 𝐵 ∧ ( 𝑏𝐵𝑑𝐵𝑓𝐵 ) ) → ( 𝑎 = 𝑐 → ( 𝑏 𝑆 𝑑 → ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) ) ) )
44 43 impd ( ( 𝑆 Po 𝐵 ∧ ( 𝑏𝐵𝑑𝐵𝑓𝐵 ) ) → ( ( 𝑎 = 𝑐𝑏 𝑆 𝑑 ) → ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) ) )
45 31 44 jaao ( ( ( 𝑅 Po 𝐴 ∧ ( 𝑎𝐴𝑐𝐴𝑒𝐴 ) ) ∧ ( 𝑆 Po 𝐵 ∧ ( 𝑏𝐵𝑑𝐵𝑓𝐵 ) ) ) → ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐𝑏 𝑆 𝑑 ) ) → ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) ) )
46 45 impd ( ( ( 𝑅 Po 𝐴 ∧ ( 𝑎𝐴𝑐𝐴𝑒𝐴 ) ) ∧ ( 𝑆 Po 𝐵 ∧ ( 𝑏𝐵𝑑𝐵𝑓𝐵 ) ) ) → ( ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐𝑏 𝑆 𝑑 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) )
47 46 an4s ( ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) ∧ ( ( 𝑎𝐴𝑐𝐴𝑒𝐴 ) ∧ ( 𝑏𝐵𝑑𝐵𝑓𝐵 ) ) ) → ( ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐𝑏 𝑆 𝑑 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) )
48 18 47 sylan2b ( ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) ∧ ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑒𝐴𝑓𝐵 ) ) ) → ( ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐𝑏 𝑆 𝑑 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) )
49 an4 ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑒𝐴𝑓𝐵 ) ) ↔ ( ( 𝑎𝐴𝑒𝐴 ) ∧ ( 𝑏𝐵𝑓𝐵 ) ) )
50 49 biimpi ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑒𝐴𝑓𝐵 ) ) → ( ( 𝑎𝐴𝑒𝐴 ) ∧ ( 𝑏𝐵𝑓𝐵 ) ) )
51 50 3adant2 ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑒𝐴𝑓𝐵 ) ) → ( ( 𝑎𝐴𝑒𝐴 ) ∧ ( 𝑏𝐵𝑓𝐵 ) ) )
52 51 adantl ( ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) ∧ ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑒𝐴𝑓𝐵 ) ) ) → ( ( 𝑎𝐴𝑒𝐴 ) ∧ ( 𝑏𝐵𝑓𝐵 ) ) )
53 48 52 jctild ( ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) ∧ ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑒𝐴𝑓𝐵 ) ) ) → ( ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐𝑏 𝑆 𝑑 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) ) → ( ( ( 𝑎𝐴𝑒𝐴 ) ∧ ( 𝑏𝐵𝑓𝐵 ) ) ∧ ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) ) )
54 53 adantld ( ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) ∧ ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑒𝐴𝑓𝐵 ) ) ) → ( ( ( ( ( 𝑎𝐴𝑐𝐴 ) ∧ ( 𝑏𝐵𝑑𝐵 ) ) ∧ ( ( 𝑐𝐴𝑒𝐴 ) ∧ ( 𝑑𝐵𝑓𝐵 ) ) ) ∧ ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐𝑏 𝑆 𝑑 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) ) ) → ( ( ( 𝑎𝐴𝑒𝐴 ) ∧ ( 𝑏𝐵𝑓𝐵 ) ) ∧ ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) ) )
55 17 54 syl5bi ( ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) ∧ ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑒𝐴𝑓𝐵 ) ) ) → ( ( ( ( ( 𝑎𝐴𝑐𝐴 ) ∧ ( 𝑏𝐵𝑑𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐𝑏 𝑆 𝑑 ) ) ) ∧ ( ( ( 𝑐𝐴𝑒𝐴 ) ∧ ( 𝑑𝐵𝑓𝐵 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) ) ) → ( ( ( 𝑎𝐴𝑒𝐴 ) ∧ ( 𝑏𝐵𝑓𝐵 ) ) ∧ ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) ) )
56 16 55 jca ( ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) ∧ ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑒𝐴𝑓𝐵 ) ) ) → ( ¬ ( ( ( 𝑎𝐴𝑎𝐴 ) ∧ ( 𝑏𝐵𝑏𝐵 ) ) ∧ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎𝑏 𝑆 𝑏 ) ) ) ∧ ( ( ( ( ( 𝑎𝐴𝑐𝐴 ) ∧ ( 𝑏𝐵𝑑𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐𝑏 𝑆 𝑑 ) ) ) ∧ ( ( ( 𝑐𝐴𝑒𝐴 ) ∧ ( 𝑑𝐵𝑓𝐵 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) ) ) → ( ( ( 𝑎𝐴𝑒𝐴 ) ∧ ( 𝑏𝐵𝑓𝐵 ) ) ∧ ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) ) ) )
57 breq12 ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ) → ( 𝑡 𝑇 𝑡 ↔ ⟨ 𝑎 , 𝑏𝑇𝑎 , 𝑏 ⟩ ) )
58 57 anidms ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑡 𝑇 𝑡 ↔ ⟨ 𝑎 , 𝑏𝑇𝑎 , 𝑏 ⟩ ) )
59 58 notbid ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ( ¬ 𝑡 𝑇 𝑡 ↔ ¬ ⟨ 𝑎 , 𝑏𝑇𝑎 , 𝑏 ⟩ ) )
60 59 3ad2ant1 ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( ¬ 𝑡 𝑇 𝑡 ↔ ¬ ⟨ 𝑎 , 𝑏𝑇𝑎 , 𝑏 ⟩ ) )
61 breq12 ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ) → ( 𝑡 𝑇 𝑢 ↔ ⟨ 𝑎 , 𝑏𝑇𝑐 , 𝑑 ⟩ ) )
62 61 3adant3 ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( 𝑡 𝑇 𝑢 ↔ ⟨ 𝑎 , 𝑏𝑇𝑐 , 𝑑 ⟩ ) )
63 breq12 ( ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( 𝑢 𝑇 𝑣 ↔ ⟨ 𝑐 , 𝑑𝑇𝑒 , 𝑓 ⟩ ) )
64 63 3adant1 ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( 𝑢 𝑇 𝑣 ↔ ⟨ 𝑐 , 𝑑𝑇𝑒 , 𝑓 ⟩ ) )
65 62 64 anbi12d ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) ↔ ( ⟨ 𝑎 , 𝑏𝑇𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑐 , 𝑑𝑇𝑒 , 𝑓 ⟩ ) ) )
66 breq12 ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( 𝑡 𝑇 𝑣 ↔ ⟨ 𝑎 , 𝑏𝑇𝑒 , 𝑓 ⟩ ) )
67 66 3adant2 ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( 𝑡 𝑇 𝑣 ↔ ⟨ 𝑎 , 𝑏𝑇𝑒 , 𝑓 ⟩ ) )
68 65 67 imbi12d ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ↔ ( ( ⟨ 𝑎 , 𝑏𝑇𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑐 , 𝑑𝑇𝑒 , 𝑓 ⟩ ) → ⟨ 𝑎 , 𝑏𝑇𝑒 , 𝑓 ⟩ ) ) )
69 60 68 anbi12d ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ↔ ( ¬ ⟨ 𝑎 , 𝑏𝑇𝑎 , 𝑏 ⟩ ∧ ( ( ⟨ 𝑎 , 𝑏𝑇𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑐 , 𝑑𝑇𝑒 , 𝑓 ⟩ ) → ⟨ 𝑎 , 𝑏𝑇𝑒 , 𝑓 ⟩ ) ) ) )
70 1 xporderlem ( ⟨ 𝑎 , 𝑏𝑇𝑎 , 𝑏 ⟩ ↔ ( ( ( 𝑎𝐴𝑎𝐴 ) ∧ ( 𝑏𝐵𝑏𝐵 ) ) ∧ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎𝑏 𝑆 𝑏 ) ) ) )
71 70 notbii ( ¬ ⟨ 𝑎 , 𝑏𝑇𝑎 , 𝑏 ⟩ ↔ ¬ ( ( ( 𝑎𝐴𝑎𝐴 ) ∧ ( 𝑏𝐵𝑏𝐵 ) ) ∧ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎𝑏 𝑆 𝑏 ) ) ) )
72 1 xporderlem ( ⟨ 𝑎 , 𝑏𝑇𝑐 , 𝑑 ⟩ ↔ ( ( ( 𝑎𝐴𝑐𝐴 ) ∧ ( 𝑏𝐵𝑑𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐𝑏 𝑆 𝑑 ) ) ) )
73 1 xporderlem ( ⟨ 𝑐 , 𝑑𝑇𝑒 , 𝑓 ⟩ ↔ ( ( ( 𝑐𝐴𝑒𝐴 ) ∧ ( 𝑑𝐵𝑓𝐵 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) ) )
74 72 73 anbi12i ( ( ⟨ 𝑎 , 𝑏𝑇𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑐 , 𝑑𝑇𝑒 , 𝑓 ⟩ ) ↔ ( ( ( ( 𝑎𝐴𝑐𝐴 ) ∧ ( 𝑏𝐵𝑑𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐𝑏 𝑆 𝑑 ) ) ) ∧ ( ( ( 𝑐𝐴𝑒𝐴 ) ∧ ( 𝑑𝐵𝑓𝐵 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) ) ) )
75 1 xporderlem ( ⟨ 𝑎 , 𝑏𝑇𝑒 , 𝑓 ⟩ ↔ ( ( ( 𝑎𝐴𝑒𝐴 ) ∧ ( 𝑏𝐵𝑓𝐵 ) ) ∧ ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) )
76 74 75 imbi12i ( ( ( ⟨ 𝑎 , 𝑏𝑇𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑐 , 𝑑𝑇𝑒 , 𝑓 ⟩ ) → ⟨ 𝑎 , 𝑏𝑇𝑒 , 𝑓 ⟩ ) ↔ ( ( ( ( ( 𝑎𝐴𝑐𝐴 ) ∧ ( 𝑏𝐵𝑑𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐𝑏 𝑆 𝑑 ) ) ) ∧ ( ( ( 𝑐𝐴𝑒𝐴 ) ∧ ( 𝑑𝐵𝑓𝐵 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) ) ) → ( ( ( 𝑎𝐴𝑒𝐴 ) ∧ ( 𝑏𝐵𝑓𝐵 ) ) ∧ ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) ) )
77 71 76 anbi12i ( ( ¬ ⟨ 𝑎 , 𝑏𝑇𝑎 , 𝑏 ⟩ ∧ ( ( ⟨ 𝑎 , 𝑏𝑇𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑐 , 𝑑𝑇𝑒 , 𝑓 ⟩ ) → ⟨ 𝑎 , 𝑏𝑇𝑒 , 𝑓 ⟩ ) ) ↔ ( ¬ ( ( ( 𝑎𝐴𝑎𝐴 ) ∧ ( 𝑏𝐵𝑏𝐵 ) ) ∧ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎𝑏 𝑆 𝑏 ) ) ) ∧ ( ( ( ( ( 𝑎𝐴𝑐𝐴 ) ∧ ( 𝑏𝐵𝑑𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐𝑏 𝑆 𝑑 ) ) ) ∧ ( ( ( 𝑐𝐴𝑒𝐴 ) ∧ ( 𝑑𝐵𝑓𝐵 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) ) ) → ( ( ( 𝑎𝐴𝑒𝐴 ) ∧ ( 𝑏𝐵𝑓𝐵 ) ) ∧ ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) ) ) )
78 69 77 bitrdi ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ↔ ( ¬ ( ( ( 𝑎𝐴𝑎𝐴 ) ∧ ( 𝑏𝐵𝑏𝐵 ) ) ∧ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎𝑏 𝑆 𝑏 ) ) ) ∧ ( ( ( ( ( 𝑎𝐴𝑐𝐴 ) ∧ ( 𝑏𝐵𝑑𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐𝑏 𝑆 𝑑 ) ) ) ∧ ( ( ( 𝑐𝐴𝑒𝐴 ) ∧ ( 𝑑𝐵𝑓𝐵 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒𝑑 𝑆 𝑓 ) ) ) ) → ( ( ( 𝑎𝐴𝑒𝐴 ) ∧ ( 𝑏𝐵𝑓𝐵 ) ) ∧ ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒𝑏 𝑆 𝑓 ) ) ) ) ) ) )
79 56 78 syl5ibr ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) ∧ ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑒𝐴𝑓𝐵 ) ) ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) )
80 79 expcomd ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑒𝐴𝑓𝐵 ) ) → ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) )
81 80 imp ( ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) ∧ ( ( 𝑎𝐴𝑏𝐵 ) ∧ ( 𝑐𝐴𝑑𝐵 ) ∧ ( 𝑒𝐴𝑓𝐵 ) ) ) → ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) )
82 5 81 sylbi ( ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎𝐴𝑏𝐵 ) ) ∧ ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐𝐴𝑑𝐵 ) ) ∧ ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒𝐴𝑓𝐵 ) ) ) → ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) )
83 82 3exp ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎𝐴𝑏𝐵 ) ) → ( ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒𝐴𝑓𝐵 ) ) → ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) ) )
84 83 com3l ( ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒𝐴𝑓𝐵 ) ) → ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎𝐴𝑏𝐵 ) ) → ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) ) )
85 84 exlimivv ( ∃ 𝑐𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒𝐴𝑓𝐵 ) ) → ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎𝐴𝑏𝐵 ) ) → ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) ) )
86 85 com3l ( ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒𝐴𝑓𝐵 ) ) → ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎𝐴𝑏𝐵 ) ) → ( ∃ 𝑐𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) ) )
87 86 exlimivv ( ∃ 𝑒𝑓 ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒𝐴𝑓𝐵 ) ) → ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎𝐴𝑏𝐵 ) ) → ( ∃ 𝑐𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) ) )
88 87 com3l ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎𝐴𝑏𝐵 ) ) → ( ∃ 𝑐𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ∃ 𝑒𝑓 ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒𝐴𝑓𝐵 ) ) → ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) ) )
89 88 exlimivv ( ∃ 𝑎𝑏 ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎𝐴𝑏𝐵 ) ) → ( ∃ 𝑐𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐𝐴𝑑𝐵 ) ) → ( ∃ 𝑒𝑓 ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒𝐴𝑓𝐵 ) ) → ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) ) )
90 89 3imp ( ( ∃ 𝑎𝑏 ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎𝐴𝑏𝐵 ) ) ∧ ∃ 𝑐𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐𝐴𝑑𝐵 ) ) ∧ ∃ 𝑒𝑓 ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒𝐴𝑓𝐵 ) ) ) → ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) )
91 2 3 4 90 syl3anb ( ( 𝑡 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑢 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 × 𝐵 ) ) → ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) )
92 91 3expia ( ( 𝑡 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑢 ∈ ( 𝐴 × 𝐵 ) ) → ( 𝑣 ∈ ( 𝐴 × 𝐵 ) → ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) )
93 92 com3r ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → ( ( 𝑡 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑢 ∈ ( 𝐴 × 𝐵 ) ) → ( 𝑣 ∈ ( 𝐴 × 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) )
94 93 imp ( ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) ∧ ( 𝑡 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑢 ∈ ( 𝐴 × 𝐵 ) ) ) → ( 𝑣 ∈ ( 𝐴 × 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) )
95 94 ralrimiv ( ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) ∧ ( 𝑡 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑢 ∈ ( 𝐴 × 𝐵 ) ) ) → ∀ 𝑣 ∈ ( 𝐴 × 𝐵 ) ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) )
96 95 ralrimivva ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → ∀ 𝑡 ∈ ( 𝐴 × 𝐵 ) ∀ 𝑢 ∈ ( 𝐴 × 𝐵 ) ∀ 𝑣 ∈ ( 𝐴 × 𝐵 ) ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) )
97 df-po ( 𝑇 Po ( 𝐴 × 𝐵 ) ↔ ∀ 𝑡 ∈ ( 𝐴 × 𝐵 ) ∀ 𝑢 ∈ ( 𝐴 × 𝐵 ) ∀ 𝑣 ∈ ( 𝐴 × 𝐵 ) ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) )
98 96 97 sylibr ( ( 𝑅 Po 𝐴𝑆 Po 𝐵 ) → 𝑇 Po ( 𝐴 × 𝐵 ) )