Metamath Proof Explorer

Theorem poxp2

Description: Another way of partially ordering a cross product of two classes. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Hypotheses xpord2.1 ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
poxp2.1 ⊢ ( 𝜑 → 𝑅 Po 𝐴 )
poxp2.2 ⊢ ( 𝜑 → 𝑆 Po 𝐵 )
Assertion poxp2 ( 𝜑 → 𝑇 Po ( 𝐴 × 𝐵 ) )

Proof

Step Hyp Ref Expression
1 xpord2.1 ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ∧ ( ( ( 1st ‘ 𝑥 ) 𝑅 ( 1st ‘ 𝑦 ) ∨ ( 1st ‘ 𝑥 ) = ( 1st ‘ 𝑦 ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
2 poxp2.1 ⊢ ( 𝜑 → 𝑅 Po 𝐴 )
3 poxp2.2 ⊢ ( 𝜑 → 𝑆 Po 𝐵 )
4 elxp2 ⊢ ( 𝑎 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ )
5 equid ⊢ 𝑝 = 𝑝
6 equid ⊢ 𝑞 = 𝑞
7 5 6 pm3.2i ⊢ ( 𝑝 = 𝑝 ∧ 𝑞 = 𝑞 )
8 neorian ⊢ ( ( 𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞 ) ↔ ¬ ( 𝑝 = 𝑝 ∧ 𝑞 = 𝑞 ) )
9 8 con2bii ⊢ ( ( 𝑝 = 𝑝 ∧ 𝑞 = 𝑞 ) ↔ ¬ ( 𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞 ) )
10 7 9 mpbi ⊢ ¬ ( 𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞 )
11 simp3 ⊢ ( ( ( 𝑝 𝑅 𝑝 ∨ 𝑝 = 𝑝 ) ∧ ( 𝑞 𝑆 𝑞 ∨ 𝑞 = 𝑞 ) ∧ ( 𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞 ) ) → ( 𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞 ) )
12 10 11 mto ⊢ ¬ ( ( 𝑝 𝑅 𝑝 ∨ 𝑝 = 𝑝 ) ∧ ( 𝑞 𝑆 𝑞 ∨ 𝑞 = 𝑞 ) ∧ ( 𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞 ) )
13 simp3 ⊢ ( ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( ( 𝑝 𝑅 𝑝 ∨ 𝑝 = 𝑝 ) ∧ ( 𝑞 𝑆 𝑞 ∨ 𝑞 = 𝑞 ) ∧ ( 𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞 ) ) ) → ( ( 𝑝 𝑅 𝑝 ∨ 𝑝 = 𝑝 ) ∧ ( 𝑞 𝑆 𝑞 ∨ 𝑞 = 𝑞 ) ∧ ( 𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞 ) ) )
14 12 13 mto ⊢ ¬ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( ( 𝑝 𝑅 𝑝 ∨ 𝑝 = 𝑝 ) ∧ ( 𝑞 𝑆 𝑞 ∨ 𝑞 = 𝑞 ) ∧ ( 𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞 ) ) )
15 1 xpord2lem ⊢ ( ⟨ 𝑝 , 𝑞 ⟩ 𝑇 ⟨ 𝑝 , 𝑞 ⟩ ↔ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( ( 𝑝 𝑅 𝑝 ∨ 𝑝 = 𝑝 ) ∧ ( 𝑞 𝑆 𝑞 ∨ 𝑞 = 𝑞 ) ∧ ( 𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞 ) ) ) )
16 14 15 mtbir ⊢ ¬ ⟨ 𝑝 , 𝑞 ⟩ 𝑇 ⟨ 𝑝 , 𝑞 ⟩
17 breq12 ⊢ ( ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ) → ( 𝑎 𝑇 𝑎 ↔ ⟨ 𝑝 , 𝑞 ⟩ 𝑇 ⟨ 𝑝 , 𝑞 ⟩ ) )
18 17 anidms ⊢ ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ → ( 𝑎 𝑇 𝑎 ↔ ⟨ 𝑝 , 𝑞 ⟩ 𝑇 ⟨ 𝑝 , 𝑞 ⟩ ) )
19 16 18 mtbiri ⊢ ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ → ¬ 𝑎 𝑇 𝑎 )
20 19 rexlimivw ⊢ ( ∃ 𝑞 ∈ 𝐵 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ → ¬ 𝑎 𝑇 𝑎 )
21 20 rexlimivw ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ → ¬ 𝑎 𝑇 𝑎 )
22 4 21 sylbi ⊢ ( 𝑎 ∈ ( 𝐴 × 𝐵 ) → ¬ 𝑎 𝑇 𝑎 )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝐴 × 𝐵 ) ) → ¬ 𝑎 𝑇 𝑎 )
24 3reeanv ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑡 ∈ 𝐴 ( ∃ 𝑞 ∈ 𝐵 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ ∃ 𝑠 ∈ 𝐵 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ∃ 𝑢 ∈ 𝐵 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) ↔ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐵 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ∃ 𝑡 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) )
25 3reeanv ⊢ ( ∃ 𝑞 ∈ 𝐵 ∃ 𝑠 ∈ 𝐵 ∃ 𝑢 ∈ 𝐵 ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) ↔ ( ∃ 𝑞 ∈ 𝐵 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ ∃ 𝑠 ∈ 𝐵 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ∃ 𝑢 ∈ 𝐵 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) )
26 25 rexbii ⊢ ( ∃ 𝑡 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ∃ 𝑠 ∈ 𝐵 ∃ 𝑢 ∈ 𝐵 ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) ↔ ∃ 𝑡 ∈ 𝐴 ( ∃ 𝑞 ∈ 𝐵 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ ∃ 𝑠 ∈ 𝐵 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ∃ 𝑢 ∈ 𝐵 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) )
27 26 2rexbii ⊢ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑡 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ∃ 𝑠 ∈ 𝐵 ∃ 𝑢 ∈ 𝐵 ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑡 ∈ 𝐴 ( ∃ 𝑞 ∈ 𝐵 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ ∃ 𝑠 ∈ 𝐵 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ∃ 𝑢 ∈ 𝐵 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) )
28 elxp2 ⊢ ( 𝑏 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐵 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ )
29 elxp2 ⊢ ( 𝑐 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑡 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ )
30 4 28 29 3anbi123i ⊢ ( ( 𝑎 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑐 ∈ ( 𝐴 × 𝐵 ) ) ↔ ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐵 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ ∃ 𝑡 ∈ 𝐴 ∃ 𝑢 ∈ 𝐵 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) )
31 24 27 30 3bitr4ri ⊢ ( ( 𝑎 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑐 ∈ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑝 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑡 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ∃ 𝑠 ∈ 𝐵 ∃ 𝑢 ∈ 𝐵 ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) )
32 df-3an ⊢ ( ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ↔ ( ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) )
33 simp3 ⊢ ( ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ) → ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) )
34 simp3 ⊢ ( ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) → ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) )
35 simpr1l ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → 𝑝 ∈ 𝐴 )
36 35 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → 𝑝 ∈ 𝐴 )
37 simpr2r ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → 𝑞 ∈ 𝐵 )
38 37 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → 𝑞 ∈ 𝐵 )
39 36 38 jca ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) )
40 simpr2l ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → 𝑡 ∈ 𝐴 )
41 40 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → 𝑡 ∈ 𝐴 )
42 simpr3r ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → 𝑢 ∈ 𝐵 )
43 42 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → 𝑢 ∈ 𝐵 )
44 41 43 jca ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) )
45 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → 𝑅 Po 𝐴 )
46 simpr1r ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → 𝑟 ∈ 𝐴 )
47 46 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → 𝑟 ∈ 𝐴 )
48 potr ⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴 ) ) → ( ( 𝑝 𝑅 𝑟 ∧ 𝑟 𝑅 𝑡 ) → 𝑝 𝑅 𝑡 ) )
49 45 36 47 41 48 syl13anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( ( 𝑝 𝑅 𝑟 ∧ 𝑟 𝑅 𝑡 ) → 𝑝 𝑅 𝑡 ) )
50 orc ⊢ ( 𝑝 𝑅 𝑡 → ( 𝑝 𝑅 𝑡 ∨ 𝑝 = 𝑡 ) )
51 49 50 syl6 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( ( 𝑝 𝑅 𝑟 ∧ 𝑟 𝑅 𝑡 ) → ( 𝑝 𝑅 𝑡 ∨ 𝑝 = 𝑡 ) ) )
52 51 expd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑝 𝑅 𝑟 → ( 𝑟 𝑅 𝑡 → ( 𝑝 𝑅 𝑡 ∨ 𝑝 = 𝑡 ) ) ) )
53 breq1 ⊢ ( 𝑝 = 𝑟 → ( 𝑝 𝑅 𝑡 ↔ 𝑟 𝑅 𝑡 ) )
54 53 50 syl6bir ⊢ ( 𝑝 = 𝑟 → ( 𝑟 𝑅 𝑡 → ( 𝑝 𝑅 𝑡 ∨ 𝑝 = 𝑡 ) ) )
55 54 a1i ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑝 = 𝑟 → ( 𝑟 𝑅 𝑡 → ( 𝑝 𝑅 𝑡 ∨ 𝑝 = 𝑡 ) ) ) )
56 simprl1 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) )
57 52 55 56 mpjaod ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑟 𝑅 𝑡 → ( 𝑝 𝑅 𝑡 ∨ 𝑝 = 𝑡 ) ) )
58 breq2 ⊢ ( 𝑟 = 𝑡 → ( 𝑝 𝑅 𝑟 ↔ 𝑝 𝑅 𝑡 ) )
59 equequ2 ⊢ ( 𝑟 = 𝑡 → ( 𝑝 = 𝑟 ↔ 𝑝 = 𝑡 ) )
60 58 59 orbi12d ⊢ ( 𝑟 = 𝑡 → ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ↔ ( 𝑝 𝑅 𝑡 ∨ 𝑝 = 𝑡 ) ) )
61 56 60 syl5ibcom ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑟 = 𝑡 → ( 𝑝 𝑅 𝑡 ∨ 𝑝 = 𝑡 ) ) )
62 simprr1 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) )
63 57 61 62 mpjaod ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑝 𝑅 𝑡 ∨ 𝑝 = 𝑡 ) )
64 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → 𝑆 Po 𝐵 )
65 simpr3l ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → 𝑠 ∈ 𝐵 )
66 65 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → 𝑠 ∈ 𝐵 )
67 potr ⊢ ( ( 𝑆 Po 𝐵 ∧ ( 𝑞 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) → ( ( 𝑞 𝑆 𝑠 ∧ 𝑠 𝑆 𝑢 ) → 𝑞 𝑆 𝑢 ) )
68 64 38 66 43 67 syl13anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( ( 𝑞 𝑆 𝑠 ∧ 𝑠 𝑆 𝑢 ) → 𝑞 𝑆 𝑢 ) )
69 orc ⊢ ( 𝑞 𝑆 𝑢 → ( 𝑞 𝑆 𝑢 ∨ 𝑞 = 𝑢 ) )
70 68 69 syl6 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( ( 𝑞 𝑆 𝑠 ∧ 𝑠 𝑆 𝑢 ) → ( 𝑞 𝑆 𝑢 ∨ 𝑞 = 𝑢 ) ) )
71 70 expd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑞 𝑆 𝑠 → ( 𝑠 𝑆 𝑢 → ( 𝑞 𝑆 𝑢 ∨ 𝑞 = 𝑢 ) ) ) )
72 breq1 ⊢ ( 𝑞 = 𝑠 → ( 𝑞 𝑆 𝑢 ↔ 𝑠 𝑆 𝑢 ) )
73 72 69 syl6bir ⊢ ( 𝑞 = 𝑠 → ( 𝑠 𝑆 𝑢 → ( 𝑞 𝑆 𝑢 ∨ 𝑞 = 𝑢 ) ) )
74 73 a1i ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑞 = 𝑠 → ( 𝑠 𝑆 𝑢 → ( 𝑞 𝑆 𝑢 ∨ 𝑞 = 𝑢 ) ) ) )
75 simprl2 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) )
76 71 74 75 mpjaod ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑠 𝑆 𝑢 → ( 𝑞 𝑆 𝑢 ∨ 𝑞 = 𝑢 ) ) )
77 breq2 ⊢ ( 𝑠 = 𝑢 → ( 𝑞 𝑆 𝑠 ↔ 𝑞 𝑆 𝑢 ) )
78 equequ2 ⊢ ( 𝑠 = 𝑢 → ( 𝑞 = 𝑠 ↔ 𝑞 = 𝑢 ) )
79 77 78 orbi12d ⊢ ( 𝑠 = 𝑢 → ( ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ↔ ( 𝑞 𝑆 𝑢 ∨ 𝑞 = 𝑢 ) ) )
80 75 79 syl5ibcom ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑠 = 𝑢 → ( 𝑞 𝑆 𝑢 ∨ 𝑞 = 𝑢 ) ) )
81 simprr2 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) )
82 76 80 81 mpjaod ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑞 𝑆 𝑢 ∨ 𝑞 = 𝑢 ) )
83 simprr3 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) )
84 neorian ⊢ ( ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ↔ ¬ ( 𝑟 = 𝑡 ∧ 𝑠 = 𝑢 ) )
85 83 84 sylib ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ¬ ( 𝑟 = 𝑡 ∧ 𝑠 = 𝑢 ) )
86 neorian ⊢ ( ( 𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢 ) ↔ ¬ ( 𝑝 = 𝑡 ∧ 𝑞 = 𝑢 ) )
87 86 con2bii ⊢ ( ( 𝑝 = 𝑡 ∧ 𝑞 = 𝑢 ) ↔ ¬ ( 𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢 ) )
88 breq1 ⊢ ( 𝑝 = 𝑡 → ( 𝑝 𝑅 𝑟 ↔ 𝑡 𝑅 𝑟 ) )
89 equequ1 ⊢ ( 𝑝 = 𝑡 → ( 𝑝 = 𝑟 ↔ 𝑡 = 𝑟 ) )
90 88 89 orbi12d ⊢ ( 𝑝 = 𝑡 → ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ↔ ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ) )
91 90 adantr ⊢ ( ( 𝑝 = 𝑡 ∧ 𝑞 = 𝑢 ) → ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ↔ ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ) )
92 breq1 ⊢ ( 𝑞 = 𝑢 → ( 𝑞 𝑆 𝑠 ↔ 𝑢 𝑆 𝑠 ) )
93 equequ1 ⊢ ( 𝑞 = 𝑢 → ( 𝑞 = 𝑠 ↔ 𝑢 = 𝑠 ) )
94 92 93 orbi12d ⊢ ( 𝑞 = 𝑢 → ( ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ↔ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ) )
95 94 adantl ⊢ ( ( 𝑝 = 𝑡 ∧ 𝑞 = 𝑢 ) → ( ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ↔ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ) )
96 neeq1 ⊢ ( 𝑝 = 𝑡 → ( 𝑝 ≠ 𝑟 ↔ 𝑡 ≠ 𝑟 ) )
97 96 adantr ⊢ ( ( 𝑝 = 𝑡 ∧ 𝑞 = 𝑢 ) → ( 𝑝 ≠ 𝑟 ↔ 𝑡 ≠ 𝑟 ) )
98 neeq1 ⊢ ( 𝑞 = 𝑢 → ( 𝑞 ≠ 𝑠 ↔ 𝑢 ≠ 𝑠 ) )
99 98 adantl ⊢ ( ( 𝑝 = 𝑡 ∧ 𝑞 = 𝑢 ) → ( 𝑞 ≠ 𝑠 ↔ 𝑢 ≠ 𝑠 ) )
100 97 99 orbi12d ⊢ ( ( 𝑝 = 𝑡 ∧ 𝑞 = 𝑢 ) → ( ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ↔ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) )
101 91 95 100 3anbi123d ⊢ ( ( 𝑝 = 𝑡 ∧ 𝑞 = 𝑢 ) → ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ↔ ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ) )
102 101 anbi1d ⊢ ( ( 𝑝 = 𝑡 ∧ 𝑞 = 𝑢 ) → ( ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ↔ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) )
103 102 anbi2d ⊢ ( ( 𝑝 = 𝑡 ∧ 𝑞 = 𝑢 ) → ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) ↔ ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) ) )
104 simprl1 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) )
105 simprr1 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) )
106 orcom ⊢ ( ( ( 𝑡 𝑅 𝑟 ∧ 𝑟 𝑅 𝑡 ) ∨ 𝑟 = 𝑡 ) ↔ ( 𝑟 = 𝑡 ∨ ( 𝑡 𝑅 𝑟 ∧ 𝑟 𝑅 𝑡 ) ) )
107 ordi ⊢ ( ( 𝑟 = 𝑡 ∨ ( 𝑡 𝑅 𝑟 ∧ 𝑟 𝑅 𝑡 ) ) ↔ ( ( 𝑟 = 𝑡 ∨ 𝑡 𝑅 𝑟 ) ∧ ( 𝑟 = 𝑡 ∨ 𝑟 𝑅 𝑡 ) ) )
108 orcom ⊢ ( ( 𝑟 = 𝑡 ∨ 𝑡 𝑅 𝑟 ) ↔ ( 𝑡 𝑅 𝑟 ∨ 𝑟 = 𝑡 ) )
109 equcom ⊢ ( 𝑟 = 𝑡 ↔ 𝑡 = 𝑟 )
110 109 orbi2i ⊢ ( ( 𝑡 𝑅 𝑟 ∨ 𝑟 = 𝑡 ) ↔ ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) )
111 108 110 bitri ⊢ ( ( 𝑟 = 𝑡 ∨ 𝑡 𝑅 𝑟 ) ↔ ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) )
112 orcom ⊢ ( ( 𝑟 = 𝑡 ∨ 𝑟 𝑅 𝑡 ) ↔ ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) )
113 111 112 anbi12i ⊢ ( ( ( 𝑟 = 𝑡 ∨ 𝑡 𝑅 𝑟 ) ∧ ( 𝑟 = 𝑡 ∨ 𝑟 𝑅 𝑡 ) ) ↔ ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ) )
114 106 107 113 3bitri ⊢ ( ( ( 𝑡 𝑅 𝑟 ∧ 𝑟 𝑅 𝑡 ) ∨ 𝑟 = 𝑡 ) ↔ ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ) )
115 104 105 114 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( ( 𝑡 𝑅 𝑟 ∧ 𝑟 𝑅 𝑡 ) ∨ 𝑟 = 𝑡 ) )
116 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → 𝑅 Po 𝐴 )
117 40 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → 𝑡 ∈ 𝐴 )
118 46 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → 𝑟 ∈ 𝐴 )
119 po2nr ⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) → ¬ ( 𝑡 𝑅 𝑟 ∧ 𝑟 𝑅 𝑡 ) )
120 116 117 118 119 syl12anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ¬ ( 𝑡 𝑅 𝑟 ∧ 𝑟 𝑅 𝑡 ) )
121 115 120 orcnd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → 𝑟 = 𝑡 )
122 simprl2 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) )
123 simprr2 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) )
124 orcom ⊢ ( ( ( 𝑢 𝑆 𝑠 ∧ 𝑠 𝑆 𝑢 ) ∨ 𝑠 = 𝑢 ) ↔ ( 𝑠 = 𝑢 ∨ ( 𝑢 𝑆 𝑠 ∧ 𝑠 𝑆 𝑢 ) ) )
125 ordi ⊢ ( ( 𝑠 = 𝑢 ∨ ( 𝑢 𝑆 𝑠 ∧ 𝑠 𝑆 𝑢 ) ) ↔ ( ( 𝑠 = 𝑢 ∨ 𝑢 𝑆 𝑠 ) ∧ ( 𝑠 = 𝑢 ∨ 𝑠 𝑆 𝑢 ) ) )
126 orcom ⊢ ( ( 𝑠 = 𝑢 ∨ 𝑢 𝑆 𝑠 ) ↔ ( 𝑢 𝑆 𝑠 ∨ 𝑠 = 𝑢 ) )
127 equcom ⊢ ( 𝑠 = 𝑢 ↔ 𝑢 = 𝑠 )
128 127 orbi2i ⊢ ( ( 𝑢 𝑆 𝑠 ∨ 𝑠 = 𝑢 ) ↔ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) )
129 126 128 bitri ⊢ ( ( 𝑠 = 𝑢 ∨ 𝑢 𝑆 𝑠 ) ↔ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) )
130 orcom ⊢ ( ( 𝑠 = 𝑢 ∨ 𝑠 𝑆 𝑢 ) ↔ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) )
131 129 130 anbi12i ⊢ ( ( ( 𝑠 = 𝑢 ∨ 𝑢 𝑆 𝑠 ) ∧ ( 𝑠 = 𝑢 ∨ 𝑠 𝑆 𝑢 ) ) ↔ ( ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ) )
132 124 125 131 3bitri ⊢ ( ( ( 𝑢 𝑆 𝑠 ∧ 𝑠 𝑆 𝑢 ) ∨ 𝑠 = 𝑢 ) ↔ ( ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ) )
133 122 123 132 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( ( 𝑢 𝑆 𝑠 ∧ 𝑠 𝑆 𝑢 ) ∨ 𝑠 = 𝑢 ) )
134 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → 𝑆 Po 𝐵 )
135 42 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → 𝑢 ∈ 𝐵 )
136 65 adantr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → 𝑠 ∈ 𝐵 )
137 po2nr ⊢ ( ( 𝑆 Po 𝐵 ∧ ( 𝑢 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵 ) ) → ¬ ( 𝑢 𝑆 𝑠 ∧ 𝑠 𝑆 𝑢 ) )
138 134 135 136 137 syl12anc ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ¬ ( 𝑢 𝑆 𝑠 ∧ 𝑠 𝑆 𝑢 ) )
139 133 138 orcnd ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → 𝑠 = 𝑢 )
140 121 139 jca ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑡 𝑅 𝑟 ∨ 𝑡 = 𝑟 ) ∧ ( 𝑢 𝑆 𝑠 ∨ 𝑢 = 𝑠 ) ∧ ( 𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑟 = 𝑡 ∧ 𝑠 = 𝑢 ) )
141 103 140 syl6bi ⊢ ( ( 𝑝 = 𝑡 ∧ 𝑞 = 𝑢 ) → ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑟 = 𝑡 ∧ 𝑠 = 𝑢 ) ) )
142 141 com12 ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( ( 𝑝 = 𝑡 ∧ 𝑞 = 𝑢 ) → ( 𝑟 = 𝑡 ∧ 𝑠 = 𝑢 ) ) )
143 87 142 syl5bir ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( ¬ ( 𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢 ) → ( 𝑟 = 𝑡 ∧ 𝑠 = 𝑢 ) ) )
144 85 143 mt3d ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( 𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢 ) )
145 63 82 144 3jca ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( ( 𝑝 𝑅 𝑡 ∨ 𝑝 = 𝑡 ) ∧ ( 𝑞 𝑆 𝑢 ∨ 𝑞 = 𝑢 ) ∧ ( 𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢 ) ) )
146 39 44 145 3jca ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) ∧ ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑝 𝑅 𝑡 ∨ 𝑝 = 𝑡 ) ∧ ( 𝑞 𝑆 𝑢 ∨ 𝑞 = 𝑢 ) ∧ ( 𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢 ) ) ) )
147 146 ex ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑝 𝑅 𝑡 ∨ 𝑝 = 𝑡 ) ∧ ( 𝑞 𝑆 𝑢 ∨ 𝑞 = 𝑢 ) ∧ ( 𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢 ) ) ) ) )
148 33 34 147 syl2ani ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑝 𝑅 𝑡 ∨ 𝑝 = 𝑡 ) ∧ ( 𝑞 𝑆 𝑢 ∨ 𝑞 = 𝑢 ) ∧ ( 𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢 ) ) ) ) )
149 breq12 ⊢ ( ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ) → ( 𝑎 𝑇 𝑏 ↔ ⟨ 𝑝 , 𝑞 ⟩ 𝑇 ⟨ 𝑟 , 𝑠 ⟩ ) )
150 149 3adant3 ⊢ ( ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) → ( 𝑎 𝑇 𝑏 ↔ ⟨ 𝑝 , 𝑞 ⟩ 𝑇 ⟨ 𝑟 , 𝑠 ⟩ ) )
151 1 xpord2lem ⊢ ( ⟨ 𝑝 , 𝑞 ⟩ 𝑇 ⟨ 𝑟 , 𝑠 ⟩ ↔ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ) )
152 150 151 bitrdi ⊢ ( ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) → ( 𝑎 𝑇 𝑏 ↔ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ) ) )
153 breq12 ⊢ ( ( 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) → ( 𝑏 𝑇 𝑐 ↔ ⟨ 𝑟 , 𝑠 ⟩ 𝑇 ⟨ 𝑡 , 𝑢 ⟩ ) )
154 153 3adant1 ⊢ ( ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) → ( 𝑏 𝑇 𝑐 ↔ ⟨ 𝑟 , 𝑠 ⟩ 𝑇 ⟨ 𝑡 , 𝑢 ⟩ ) )
155 1 xpord2lem ⊢ ( ⟨ 𝑟 , 𝑠 ⟩ 𝑇 ⟨ 𝑡 , 𝑢 ⟩ ↔ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) )
156 154 155 bitrdi ⊢ ( ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) → ( 𝑏 𝑇 𝑐 ↔ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) )
157 152 156 anbi12d ⊢ ( ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) → ( ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) ↔ ( ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) ) )
158 breq12 ⊢ ( ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) → ( 𝑎 𝑇 𝑐 ↔ ⟨ 𝑝 , 𝑞 ⟩ 𝑇 ⟨ 𝑡 , 𝑢 ⟩ ) )
159 158 3adant2 ⊢ ( ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) → ( 𝑎 𝑇 𝑐 ↔ ⟨ 𝑝 , 𝑞 ⟩ 𝑇 ⟨ 𝑡 , 𝑢 ⟩ ) )
160 1 xpord2lem ⊢ ( ⟨ 𝑝 , 𝑞 ⟩ 𝑇 ⟨ 𝑡 , 𝑢 ⟩ ↔ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑝 𝑅 𝑡 ∨ 𝑝 = 𝑡 ) ∧ ( 𝑞 𝑆 𝑢 ∨ 𝑞 = 𝑢 ) ∧ ( 𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢 ) ) ) )
161 159 160 bitrdi ⊢ ( ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) → ( 𝑎 𝑇 𝑐 ↔ ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑝 𝑅 𝑡 ∨ 𝑝 = 𝑡 ) ∧ ( 𝑞 𝑆 𝑢 ∨ 𝑞 = 𝑢 ) ∧ ( 𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢 ) ) ) ) )
162 157 161 imbi12d ⊢ ( ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) → ( ( ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) → 𝑎 𝑇 𝑐 ) ↔ ( ( ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ) ∧ ( ( 𝑝 𝑅 𝑟 ∨ 𝑝 = 𝑟 ) ∧ ( 𝑞 𝑆 𝑠 ∨ 𝑞 = 𝑠 ) ∧ ( 𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠 ) ) ) ∧ ( ( 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑟 𝑅 𝑡 ∨ 𝑟 = 𝑡 ) ∧ ( 𝑠 𝑆 𝑢 ∨ 𝑠 = 𝑢 ) ∧ ( 𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢 ) ) ) ) → ( ( 𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵 ) ∧ ( ( 𝑝 𝑅 𝑡 ∨ 𝑝 = 𝑡 ) ∧ ( 𝑞 𝑆 𝑢 ∨ 𝑞 = 𝑢 ) ∧ ( 𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢 ) ) ) ) ) )
163 148 162 syl5ibrcom ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) → ( ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) → 𝑎 𝑇 𝑐 ) ) )
164 32 163 sylan2br ⊢ ( ( 𝜑 ∧ ( ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) ) → ( ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) → ( ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) → 𝑎 𝑇 𝑐 ) ) )
165 164 anassrs ⊢ ( ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) ) ∧ ( 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵 ) ) → ( ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) → ( ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) → 𝑎 𝑇 𝑐 ) ) )
166 165 rexlimdvva ⊢ ( ( 𝜑 ∧ ( ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) ) → ( ∃ 𝑠 ∈ 𝐵 ∃ 𝑢 ∈ 𝐵 ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) → ( ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) → 𝑎 𝑇 𝑐 ) ) )
167 166 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) ∧ ( 𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵 ) ) → ( ∃ 𝑠 ∈ 𝐵 ∃ 𝑢 ∈ 𝐵 ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) → ( ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) → 𝑎 𝑇 𝑐 ) ) )
168 167 rexlimdvva ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ) ) → ( ∃ 𝑡 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ∃ 𝑠 ∈ 𝐵 ∃ 𝑢 ∈ 𝐵 ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) → ( ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) → 𝑎 𝑇 𝑐 ) ) )
169 168 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑝 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑡 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ∃ 𝑠 ∈ 𝐵 ∃ 𝑢 ∈ 𝐵 ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) → ( ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) → 𝑎 𝑇 𝑐 ) ) )
170 169 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑝 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑡 ∈ 𝐴 ∃ 𝑞 ∈ 𝐵 ∃ 𝑠 ∈ 𝐵 ∃ 𝑢 ∈ 𝐵 ( 𝑎 = ⟨ 𝑝 , 𝑞 ⟩ ∧ 𝑏 = ⟨ 𝑟 , 𝑠 ⟩ ∧ 𝑐 = ⟨ 𝑡 , 𝑢 ⟩ ) ) → ( ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) → 𝑎 𝑇 𝑐 ) )
171 31 170 sylan2b ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑏 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑐 ∈ ( 𝐴 × 𝐵 ) ) ) → ( ( 𝑎 𝑇 𝑏 ∧ 𝑏 𝑇 𝑐 ) → 𝑎 𝑇 𝑐 ) )
172 23 171 ispod ⊢ ( 𝜑 → 𝑇 Po ( 𝐴 × 𝐵 ) )