Metamath Proof Explorer

Theorem poxp3

Description: Triple Cartesian product partial ordering. (Contributed by Scott Fenton, 21-Aug-2024)

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

Proof

Step Hyp Ref Expression
1 xpord3.1 ⊢ 𝑈 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( ( 1st ‘ ( 1st ‘ 𝑥 ) ) 𝑅 ( 1st ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 1st ‘ ( 1st ‘ 𝑥 ) ) = ( 1st ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ ( 1st ‘ 𝑥 ) ) 𝑆 ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 2nd ‘ ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑇 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
2 poxp3.1 ⊢ ( 𝜑 → 𝑅 Po 𝐴 )
3 poxp3.2 ⊢ ( 𝜑 → 𝑆 Po 𝐵 )
4 poxp3.3 ⊢ ( 𝜑 → 𝑇 Po 𝐶 )
5 el2xptp ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ )
6 neirr ⊢ ¬ 𝑎 ≠ 𝑎
7 neirr ⊢ ¬ 𝑏 ≠ 𝑏
8 neirr ⊢ ¬ 𝑐 ≠ 𝑐
9 6 7 8 3pm3.2ni ⊢ ¬ ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 )
10 9 intnan ⊢ ¬ ( ( ( 𝑎 𝑅 𝑎 ∨ 𝑎 = 𝑎 ) ∧ ( 𝑏 𝑆 𝑏 ∨ 𝑏 = 𝑏 ) ∧ ( 𝑐 𝑇 𝑐 ∨ 𝑐 = 𝑐 ) ) ∧ ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) )
11 simp3 ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑎 ∨ 𝑎 = 𝑎 ) ∧ ( 𝑏 𝑆 𝑏 ∨ 𝑏 = 𝑏 ) ∧ ( 𝑐 𝑇 𝑐 ∨ 𝑐 = 𝑐 ) ) ∧ ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) ) ) → ( ( ( 𝑎 𝑅 𝑎 ∨ 𝑎 = 𝑎 ) ∧ ( 𝑏 𝑆 𝑏 ∨ 𝑏 = 𝑏 ) ∧ ( 𝑐 𝑇 𝑐 ∨ 𝑐 = 𝑐 ) ) ∧ ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) ) )
12 10 11 mto ⊢ ¬ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑎 ∨ 𝑎 = 𝑎 ) ∧ ( 𝑏 𝑆 𝑏 ∨ 𝑏 = 𝑏 ) ∧ ( 𝑐 𝑇 𝑐 ∨ 𝑐 = 𝑐 ) ) ∧ ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) ) )
13 breq12 ⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → ( 𝑝 𝑈 𝑝 ↔ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) )
14 13 anidms ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( 𝑝 𝑈 𝑝 ↔ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) )
15 1 xpord3lem ⊢ ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑎 ∨ 𝑎 = 𝑎 ) ∧ ( 𝑏 𝑆 𝑏 ∨ 𝑏 = 𝑏 ) ∧ ( 𝑐 𝑇 𝑐 ∨ 𝑐 = 𝑐 ) ) ∧ ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) ) ) )
16 14 15 bitrdi ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ( 𝑝 𝑈 𝑝 ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑎 ∨ 𝑎 = 𝑎 ) ∧ ( 𝑏 𝑆 𝑏 ∨ 𝑏 = 𝑏 ) ∧ ( 𝑐 𝑇 𝑐 ∨ 𝑐 = 𝑐 ) ) ∧ ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) ) ) ) )
17 12 16 mtbiri ⊢ ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ¬ 𝑝 𝑈 𝑝 )
18 17 rexlimivw ⊢ ( ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ¬ 𝑝 𝑈 𝑝 )
19 18 rexlimivw ⊢ ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ¬ 𝑝 𝑈 𝑝 )
20 19 rexlimivw ⊢ ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ → ¬ 𝑝 𝑈 𝑝 )
21 5 20 sylbi ⊢ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ¬ 𝑝 𝑈 𝑝 )
22 21 adantl ⊢ ( ( 𝜑 ∧ 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) → ¬ 𝑝 𝑈 𝑝 )
23 3reeanv ⊢ ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑑 ∈ 𝐴 ∃ 𝑔 ∈ 𝐴 ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ∃ 𝑒 ∈ 𝐵 ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ ∃ ℎ ∈ 𝐵 ∃ 𝑖 ∈ 𝐶 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) ↔ ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ∃ 𝑑 ∈ 𝐴 ∃ 𝑒 ∈ 𝐵 ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 ∃ 𝑖 ∈ 𝐶 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) )
24 3reeanv ⊢ ( ∃ 𝑐 ∈ 𝐶 ∃ 𝑓 ∈ 𝐶 ∃ 𝑖 ∈ 𝐶 ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) ↔ ( ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ ∃ 𝑖 ∈ 𝐶 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) )
25 24 rexbii ⊢ ( ∃ ℎ ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑓 ∈ 𝐶 ∃ 𝑖 ∈ 𝐶 ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) ↔ ∃ ℎ ∈ 𝐵 ( ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ ∃ 𝑖 ∈ 𝐶 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) )
26 25 2rexbii ⊢ ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 ∃ ℎ ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑓 ∈ 𝐶 ∃ 𝑖 ∈ 𝐶 ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) ↔ ∃ 𝑏 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 ∃ ℎ ∈ 𝐵 ( ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ ∃ 𝑖 ∈ 𝐶 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) )
27 3reeanv ⊢ ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 ∃ ℎ ∈ 𝐵 ( ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ ∃ 𝑖 ∈ 𝐶 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) ↔ ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ∃ 𝑒 ∈ 𝐵 ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ ∃ ℎ ∈ 𝐵 ∃ 𝑖 ∈ 𝐶 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) )
28 26 27 bitri ⊢ ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 ∃ ℎ ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑓 ∈ 𝐶 ∃ 𝑖 ∈ 𝐶 ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) ↔ ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ∃ 𝑒 ∈ 𝐵 ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ ∃ ℎ ∈ 𝐵 ∃ 𝑖 ∈ 𝐶 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) )
29 28 rexbii ⊢ ( ∃ 𝑔 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 ∃ ℎ ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑓 ∈ 𝐶 ∃ 𝑖 ∈ 𝐶 ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) ↔ ∃ 𝑔 ∈ 𝐴 ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ∃ 𝑒 ∈ 𝐵 ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ ∃ ℎ ∈ 𝐵 ∃ 𝑖 ∈ 𝐶 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) )
30 29 2rexbii ⊢ ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑑 ∈ 𝐴 ∃ 𝑔 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 ∃ ℎ ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑓 ∈ 𝐶 ∃ 𝑖 ∈ 𝐶 ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑑 ∈ 𝐴 ∃ 𝑔 ∈ 𝐴 ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ∃ 𝑒 ∈ 𝐵 ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ ∃ ℎ ∈ 𝐵 ∃ 𝑖 ∈ 𝐶 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) )
31 el2xptp ⊢ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ∃ 𝑑 ∈ 𝐴 ∃ 𝑒 ∈ 𝐵 ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ )
32 el2xptp ⊢ ( 𝑟 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 ∃ 𝑖 ∈ 𝐶 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ )
33 5 31 32 3anbi123i ⊢ ( ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑟 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) ↔ ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ ∃ 𝑑 ∈ 𝐴 ∃ 𝑒 ∈ 𝐵 ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ ∃ 𝑔 ∈ 𝐴 ∃ ℎ ∈ 𝐵 ∃ 𝑖 ∈ 𝐶 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) )
34 23 30 33 3bitr4ri ⊢ ( ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑟 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) ↔ ∃ 𝑎 ∈ 𝐴 ∃ 𝑑 ∈ 𝐴 ∃ 𝑔 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 ∃ ℎ ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑓 ∈ 𝐶 ∃ 𝑖 ∈ 𝐶 ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) )
35 simpr1l ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) )
36 simpr2r ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) )
37 simp1l1 ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → 𝑎 ∈ 𝐴 )
38 simp2l1 ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → 𝑑 ∈ 𝐴 )
39 simp2r1 ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → 𝑔 ∈ 𝐴 )
40 37 38 39 3jca ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → ( 𝑎 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) )
41 potr ⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) ) → ( ( 𝑎 𝑅 𝑑 ∧ 𝑑 𝑅 𝑔 ) → 𝑎 𝑅 𝑔 ) )
42 2 40 41 syl2an ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( ( 𝑎 𝑅 𝑑 ∧ 𝑑 𝑅 𝑔 ) → 𝑎 𝑅 𝑔 ) )
43 42 expd ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑎 𝑅 𝑑 → ( 𝑑 𝑅 𝑔 → 𝑎 𝑅 𝑔 ) ) )
44 breq1 ⊢ ( 𝑎 = 𝑑 → ( 𝑎 𝑅 𝑔 ↔ 𝑑 𝑅 𝑔 ) )
45 44 biimprd ⊢ ( 𝑎 = 𝑑 → ( 𝑑 𝑅 𝑔 → 𝑎 𝑅 𝑔 ) )
46 45 a1i ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑎 = 𝑑 → ( 𝑑 𝑅 𝑔 → 𝑎 𝑅 𝑔 ) ) )
47 simpll1 ⊢ ( ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) → ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) )
48 47 3ad2ant3 ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) )
49 48 adantl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) )
50 43 46 49 mpjaod ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑑 𝑅 𝑔 → 𝑎 𝑅 𝑔 ) )
51 orc ⊢ ( 𝑎 𝑅 𝑔 → ( 𝑎 𝑅 𝑔 ∨ 𝑎 = 𝑔 ) )
52 50 51 syl6 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑑 𝑅 𝑔 → ( 𝑎 𝑅 𝑔 ∨ 𝑎 = 𝑔 ) ) )
53 breq2 ⊢ ( 𝑑 = 𝑔 → ( 𝑎 𝑅 𝑑 ↔ 𝑎 𝑅 𝑔 ) )
54 equequ2 ⊢ ( 𝑑 = 𝑔 → ( 𝑎 = 𝑑 ↔ 𝑎 = 𝑔 ) )
55 53 54 orbi12d ⊢ ( 𝑑 = 𝑔 → ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ↔ ( 𝑎 𝑅 𝑔 ∨ 𝑎 = 𝑔 ) ) )
56 49 55 syl5ibcom ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑑 = 𝑔 → ( 𝑎 𝑅 𝑔 ∨ 𝑎 = 𝑔 ) ) )
57 simprl1 ⊢ ( ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) → ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) )
58 57 3ad2ant3 ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) )
59 58 adantl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) )
60 52 56 59 mpjaod ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑎 𝑅 𝑔 ∨ 𝑎 = 𝑔 ) )
61 simp1l2 ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → 𝑏 ∈ 𝐵 )
62 simp2l2 ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → 𝑒 ∈ 𝐵 )
63 simp2r2 ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → ℎ ∈ 𝐵 )
64 61 62 63 3jca ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → ( 𝑏 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) )
65 potr ⊢ ( ( 𝑆 Po 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ( ( 𝑏 𝑆 𝑒 ∧ 𝑒 𝑆 ℎ ) → 𝑏 𝑆 ℎ ) )
66 3 64 65 syl2an ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( ( 𝑏 𝑆 𝑒 ∧ 𝑒 𝑆 ℎ ) → 𝑏 𝑆 ℎ ) )
67 66 expd ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑏 𝑆 𝑒 → ( 𝑒 𝑆 ℎ → 𝑏 𝑆 ℎ ) ) )
68 breq1 ⊢ ( 𝑏 = 𝑒 → ( 𝑏 𝑆 ℎ ↔ 𝑒 𝑆 ℎ ) )
69 68 biimprd ⊢ ( 𝑏 = 𝑒 → ( 𝑒 𝑆 ℎ → 𝑏 𝑆 ℎ ) )
70 69 a1i ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑏 = 𝑒 → ( 𝑒 𝑆 ℎ → 𝑏 𝑆 ℎ ) ) )
71 simpll2 ⊢ ( ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) → ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) )
72 71 3ad2ant3 ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) )
73 72 adantl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) )
74 67 70 73 mpjaod ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑒 𝑆 ℎ → 𝑏 𝑆 ℎ ) )
75 orc ⊢ ( 𝑏 𝑆 ℎ → ( 𝑏 𝑆 ℎ ∨ 𝑏 = ℎ ) )
76 74 75 syl6 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑒 𝑆 ℎ → ( 𝑏 𝑆 ℎ ∨ 𝑏 = ℎ ) ) )
77 breq2 ⊢ ( 𝑒 = ℎ → ( 𝑏 𝑆 𝑒 ↔ 𝑏 𝑆 ℎ ) )
78 equequ2 ⊢ ( 𝑒 = ℎ → ( 𝑏 = 𝑒 ↔ 𝑏 = ℎ ) )
79 77 78 orbi12d ⊢ ( 𝑒 = ℎ → ( ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ↔ ( 𝑏 𝑆 ℎ ∨ 𝑏 = ℎ ) ) )
80 73 79 syl5ibcom ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑒 = ℎ → ( 𝑏 𝑆 ℎ ∨ 𝑏 = ℎ ) ) )
81 simprl2 ⊢ ( ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) → ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) )
82 81 3ad2ant3 ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) )
83 82 adantl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) )
84 76 80 83 mpjaod ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑏 𝑆 ℎ ∨ 𝑏 = ℎ ) )
85 simp1l3 ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → 𝑐 ∈ 𝐶 )
86 simp2l3 ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → 𝑓 ∈ 𝐶 )
87 simp2r3 ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → 𝑖 ∈ 𝐶 )
88 85 86 87 3jca ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → ( 𝑐 ∈ 𝐶 ∧ 𝑓 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶 ) )
89 potr ⊢ ( ( 𝑇 Po 𝐶 ∧ ( 𝑐 ∈ 𝐶 ∧ 𝑓 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶 ) ) → ( ( 𝑐 𝑇 𝑓 ∧ 𝑓 𝑇 𝑖 ) → 𝑐 𝑇 𝑖 ) )
90 4 88 89 syl2an ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( ( 𝑐 𝑇 𝑓 ∧ 𝑓 𝑇 𝑖 ) → 𝑐 𝑇 𝑖 ) )
91 90 expd ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑐 𝑇 𝑓 → ( 𝑓 𝑇 𝑖 → 𝑐 𝑇 𝑖 ) ) )
92 breq1 ⊢ ( 𝑐 = 𝑓 → ( 𝑐 𝑇 𝑖 ↔ 𝑓 𝑇 𝑖 ) )
93 92 biimprd ⊢ ( 𝑐 = 𝑓 → ( 𝑓 𝑇 𝑖 → 𝑐 𝑇 𝑖 ) )
94 93 a1i ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑐 = 𝑓 → ( 𝑓 𝑇 𝑖 → 𝑐 𝑇 𝑖 ) ) )
95 simpll3 ⊢ ( ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) → ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) )
96 95 3ad2ant3 ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) )
97 96 adantl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) )
98 91 94 97 mpjaod ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑓 𝑇 𝑖 → 𝑐 𝑇 𝑖 ) )
99 orc ⊢ ( 𝑐 𝑇 𝑖 → ( 𝑐 𝑇 𝑖 ∨ 𝑐 = 𝑖 ) )
100 98 99 syl6 ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑓 𝑇 𝑖 → ( 𝑐 𝑇 𝑖 ∨ 𝑐 = 𝑖 ) ) )
101 breq2 ⊢ ( 𝑓 = 𝑖 → ( 𝑐 𝑇 𝑓 ↔ 𝑐 𝑇 𝑖 ) )
102 equequ2 ⊢ ( 𝑓 = 𝑖 → ( 𝑐 = 𝑓 ↔ 𝑐 = 𝑖 ) )
103 101 102 orbi12d ⊢ ( 𝑓 = 𝑖 → ( ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ↔ ( 𝑐 𝑇 𝑖 ∨ 𝑐 = 𝑖 ) ) )
104 97 103 syl5ibcom ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑓 = 𝑖 → ( 𝑐 𝑇 𝑖 ∨ 𝑐 = 𝑖 ) ) )
105 simprl3 ⊢ ( ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) → ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) )
106 105 3ad2ant3 ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) )
107 106 adantl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) )
108 100 104 107 mpjaod ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑐 𝑇 𝑖 ∨ 𝑐 = 𝑖 ) )
109 60 84 108 3jca ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( ( 𝑎 𝑅 𝑔 ∨ 𝑎 = 𝑔 ) ∧ ( 𝑏 𝑆 ℎ ∨ 𝑏 = ℎ ) ∧ ( 𝑐 𝑇 𝑖 ∨ 𝑐 = 𝑖 ) ) )
110 simp3rr ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) )
111 110 adantl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) )
112 59 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) ∧ 𝑎 = 𝑔 ) → ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) )
113 breq1 ⊢ ( 𝑎 = 𝑔 → ( 𝑎 𝑅 𝑑 ↔ 𝑔 𝑅 𝑑 ) )
114 equequ1 ⊢ ( 𝑎 = 𝑔 → ( 𝑎 = 𝑑 ↔ 𝑔 = 𝑑 ) )
115 equcom ⊢ ( 𝑔 = 𝑑 ↔ 𝑑 = 𝑔 )
116 114 115 bitrdi ⊢ ( 𝑎 = 𝑔 → ( 𝑎 = 𝑑 ↔ 𝑑 = 𝑔 ) )
117 113 116 orbi12d ⊢ ( 𝑎 = 𝑔 → ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ↔ ( 𝑔 𝑅 𝑑 ∨ 𝑑 = 𝑔 ) ) )
118 49 117 syl5ibcom ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑎 = 𝑔 → ( 𝑔 𝑅 𝑑 ∨ 𝑑 = 𝑔 ) ) )
119 118 imp ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) ∧ 𝑎 = 𝑔 ) → ( 𝑔 𝑅 𝑑 ∨ 𝑑 = 𝑔 ) )
120 ordir ⊢ ( ( ( 𝑑 𝑅 𝑔 ∧ 𝑔 𝑅 𝑑 ) ∨ 𝑑 = 𝑔 ) ↔ ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑔 𝑅 𝑑 ∨ 𝑑 = 𝑔 ) ) )
121 112 119 120 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) ∧ 𝑎 = 𝑔 ) → ( ( 𝑑 𝑅 𝑔 ∧ 𝑔 𝑅 𝑑 ) ∨ 𝑑 = 𝑔 ) )
122 2 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → 𝑅 Po 𝐴 )
123 38 adantl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → 𝑑 ∈ 𝐴 )
124 39 adantl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → 𝑔 ∈ 𝐴 )
125 po2nr ⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ) ) → ¬ ( 𝑑 𝑅 𝑔 ∧ 𝑔 𝑅 𝑑 ) )
126 122 123 124 125 syl12anc ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ¬ ( 𝑑 𝑅 𝑔 ∧ 𝑔 𝑅 𝑑 ) )
127 126 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) ∧ 𝑎 = 𝑔 ) → ¬ ( 𝑑 𝑅 𝑔 ∧ 𝑔 𝑅 𝑑 ) )
128 121 127 orcnd ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) ∧ 𝑎 = 𝑔 ) → 𝑑 = 𝑔 )
129 128 ex ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑎 = 𝑔 → 𝑑 = 𝑔 ) )
130 129 necon3d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑑 ≠ 𝑔 → 𝑎 ≠ 𝑔 ) )
131 83 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) ∧ 𝑏 = ℎ ) → ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) )
132 breq1 ⊢ ( 𝑏 = ℎ → ( 𝑏 𝑆 𝑒 ↔ ℎ 𝑆 𝑒 ) )
133 equequ1 ⊢ ( 𝑏 = ℎ → ( 𝑏 = 𝑒 ↔ ℎ = 𝑒 ) )
134 equcom ⊢ ( ℎ = 𝑒 ↔ 𝑒 = ℎ )
135 133 134 bitrdi ⊢ ( 𝑏 = ℎ → ( 𝑏 = 𝑒 ↔ 𝑒 = ℎ ) )
136 132 135 orbi12d ⊢ ( 𝑏 = ℎ → ( ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ↔ ( ℎ 𝑆 𝑒 ∨ 𝑒 = ℎ ) ) )
137 73 136 syl5ibcom ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑏 = ℎ → ( ℎ 𝑆 𝑒 ∨ 𝑒 = ℎ ) ) )
138 137 imp ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) ∧ 𝑏 = ℎ ) → ( ℎ 𝑆 𝑒 ∨ 𝑒 = ℎ ) )
139 ordir ⊢ ( ( ( 𝑒 𝑆 ℎ ∧ ℎ 𝑆 𝑒 ) ∨ 𝑒 = ℎ ) ↔ ( ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( ℎ 𝑆 𝑒 ∨ 𝑒 = ℎ ) ) )
140 131 138 139 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) ∧ 𝑏 = ℎ ) → ( ( 𝑒 𝑆 ℎ ∧ ℎ 𝑆 𝑒 ) ∨ 𝑒 = ℎ ) )
141 3 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → 𝑆 Po 𝐵 )
142 62 adantl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → 𝑒 ∈ 𝐵 )
143 63 adantl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ℎ ∈ 𝐵 )
144 po2nr ⊢ ( ( 𝑆 Po 𝐵 ∧ ( 𝑒 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ) ) → ¬ ( 𝑒 𝑆 ℎ ∧ ℎ 𝑆 𝑒 ) )
145 141 142 143 144 syl12anc ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ¬ ( 𝑒 𝑆 ℎ ∧ ℎ 𝑆 𝑒 ) )
146 145 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) ∧ 𝑏 = ℎ ) → ¬ ( 𝑒 𝑆 ℎ ∧ ℎ 𝑆 𝑒 ) )
147 140 146 orcnd ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) ∧ 𝑏 = ℎ ) → 𝑒 = ℎ )
148 147 ex ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑏 = ℎ → 𝑒 = ℎ ) )
149 148 necon3d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑒 ≠ ℎ → 𝑏 ≠ ℎ ) )
150 107 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) ∧ 𝑐 = 𝑖 ) → ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) )
151 breq1 ⊢ ( 𝑐 = 𝑖 → ( 𝑐 𝑇 𝑓 ↔ 𝑖 𝑇 𝑓 ) )
152 equequ1 ⊢ ( 𝑐 = 𝑖 → ( 𝑐 = 𝑓 ↔ 𝑖 = 𝑓 ) )
153 equcom ⊢ ( 𝑖 = 𝑓 ↔ 𝑓 = 𝑖 )
154 152 153 bitrdi ⊢ ( 𝑐 = 𝑖 → ( 𝑐 = 𝑓 ↔ 𝑓 = 𝑖 ) )
155 151 154 orbi12d ⊢ ( 𝑐 = 𝑖 → ( ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ↔ ( 𝑖 𝑇 𝑓 ∨ 𝑓 = 𝑖 ) ) )
156 97 155 syl5ibcom ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑐 = 𝑖 → ( 𝑖 𝑇 𝑓 ∨ 𝑓 = 𝑖 ) ) )
157 156 imp ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) ∧ 𝑐 = 𝑖 ) → ( 𝑖 𝑇 𝑓 ∨ 𝑓 = 𝑖 ) )
158 ordir ⊢ ( ( ( 𝑓 𝑇 𝑖 ∧ 𝑖 𝑇 𝑓 ) ∨ 𝑓 = 𝑖 ) ↔ ( ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ∧ ( 𝑖 𝑇 𝑓 ∨ 𝑓 = 𝑖 ) ) )
159 150 157 158 sylanbrc ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) ∧ 𝑐 = 𝑖 ) → ( ( 𝑓 𝑇 𝑖 ∧ 𝑖 𝑇 𝑓 ) ∨ 𝑓 = 𝑖 ) )
160 4 adantr ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → 𝑇 Po 𝐶 )
161 86 adantl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → 𝑓 ∈ 𝐶 )
162 87 adantl ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → 𝑖 ∈ 𝐶 )
163 po2nr ⊢ ( ( 𝑇 Po 𝐶 ∧ ( 𝑓 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶 ) ) → ¬ ( 𝑓 𝑇 𝑖 ∧ 𝑖 𝑇 𝑓 ) )
164 160 161 162 163 syl12anc ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ¬ ( 𝑓 𝑇 𝑖 ∧ 𝑖 𝑇 𝑓 ) )
165 164 adantr ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) ∧ 𝑐 = 𝑖 ) → ¬ ( 𝑓 𝑇 𝑖 ∧ 𝑖 𝑇 𝑓 ) )
166 159 165 orcnd ⊢ ( ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) ∧ 𝑐 = 𝑖 ) → 𝑓 = 𝑖 )
167 166 ex ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑐 = 𝑖 → 𝑓 = 𝑖 ) )
168 167 necon3d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑓 ≠ 𝑖 → 𝑐 ≠ 𝑖 ) )
169 130 149 168 3orim123d ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) → ( 𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖 ) ) )
170 111 169 mpd ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( 𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖 ) )
171 109 170 jca ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( ( ( 𝑎 𝑅 𝑔 ∨ 𝑎 = 𝑔 ) ∧ ( 𝑏 𝑆 ℎ ∨ 𝑏 = ℎ ) ∧ ( 𝑐 𝑇 𝑖 ∨ 𝑐 = 𝑖 ) ) ∧ ( 𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖 ) ) )
172 35 36 171 3jca ⊢ ( ( 𝜑 ∧ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑔 ∨ 𝑎 = 𝑔 ) ∧ ( 𝑏 𝑆 ℎ ∨ 𝑏 = ℎ ) ∧ ( 𝑐 𝑇 𝑖 ∨ 𝑐 = 𝑖 ) ) ∧ ( 𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖 ) ) ) )
173 172 ex ⊢ ( 𝜑 → ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑔 ∨ 𝑎 = 𝑔 ) ∧ ( 𝑏 𝑆 ℎ ∨ 𝑏 = ℎ ) ∧ ( 𝑐 𝑇 𝑖 ∨ 𝑐 = 𝑖 ) ) ∧ ( 𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖 ) ) ) ) )
174 breq12 ⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) → ( 𝑝 𝑈 𝑞 ↔ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ 𝑈 ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) )
175 174 3adant3 ⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( 𝑝 𝑈 𝑞 ↔ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ 𝑈 ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ) )
176 1 xpord3lem ⊢ ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ 𝑈 ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ) )
177 175 176 bitrdi ⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( 𝑝 𝑈 𝑞 ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ) ) )
178 breq12 ⊢ ( ( 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( 𝑞 𝑈 𝑟 ↔ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ 𝑈 ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) )
179 178 3adant1 ⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( 𝑞 𝑈 𝑟 ↔ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ 𝑈 ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) )
180 1 xpord3lem ⊢ ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ 𝑈 ⟨ 𝑔 , ℎ , 𝑖 ⟩ ↔ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) )
181 179 180 bitrdi ⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( 𝑞 𝑈 𝑟 ↔ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) )
182 177 181 anbi12d ⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( ( 𝑝 𝑈 𝑞 ∧ 𝑞 𝑈 𝑟 ) ↔ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) )
183 an6 ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ↔ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) )
184 182 183 bitrdi ⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( ( 𝑝 𝑈 𝑞 ∧ 𝑞 𝑈 𝑟 ) ↔ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) ) )
185 breq12 ⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( 𝑝 𝑈 𝑟 ↔ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ 𝑈 ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) )
186 185 3adant2 ⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( 𝑝 𝑈 𝑟 ↔ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ 𝑈 ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) )
187 1 xpord3lem ⊢ ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ 𝑈 ⟨ 𝑔 , ℎ , 𝑖 ⟩ ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑔 ∨ 𝑎 = 𝑔 ) ∧ ( 𝑏 𝑆 ℎ ∨ 𝑏 = ℎ ) ∧ ( 𝑐 𝑇 𝑖 ∨ 𝑐 = 𝑖 ) ) ∧ ( 𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖 ) ) ) )
188 186 187 bitrdi ⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( 𝑝 𝑈 𝑟 ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑔 ∨ 𝑎 = 𝑔 ) ∧ ( 𝑏 𝑆 ℎ ∨ 𝑏 = ℎ ) ∧ ( 𝑐 𝑇 𝑖 ∨ 𝑐 = 𝑖 ) ) ∧ ( 𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖 ) ) ) ) )
189 184 188 imbi12d ⊢ ( ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( ( ( 𝑝 𝑈 𝑞 ∧ 𝑞 𝑈 𝑟 ) → 𝑝 𝑈 𝑟 ) ↔ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ) ∧ ( ( ( ( 𝑎 𝑅 𝑑 ∨ 𝑎 = 𝑑 ) ∧ ( 𝑏 𝑆 𝑒 ∨ 𝑏 = 𝑒 ) ∧ ( 𝑐 𝑇 𝑓 ∨ 𝑐 = 𝑓 ) ) ∧ ( 𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓 ) ) ∧ ( ( ( 𝑑 𝑅 𝑔 ∨ 𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 ℎ ∨ 𝑒 = ℎ ) ∧ ( 𝑓 𝑇 𝑖 ∨ 𝑓 = 𝑖 ) ) ∧ ( 𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖 ) ) ) ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶 ) ∧ ( ( ( 𝑎 𝑅 𝑔 ∨ 𝑎 = 𝑔 ) ∧ ( 𝑏 𝑆 ℎ ∨ 𝑏 = ℎ ) ∧ ( 𝑐 𝑇 𝑖 ∨ 𝑐 = 𝑖 ) ) ∧ ( 𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖 ) ) ) ) ) )
190 173 189 syl5ibrcom ⊢ ( 𝜑 → ( ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( ( 𝑝 𝑈 𝑞 ∧ 𝑞 𝑈 𝑟 ) → 𝑝 𝑈 𝑟 ) ) )
191 190 rexlimdvw ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ 𝐶 ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( ( 𝑝 𝑈 𝑞 ∧ 𝑞 𝑈 𝑟 ) → 𝑝 𝑈 𝑟 ) ) )
192 191 rexlimdvw ⊢ ( 𝜑 → ( ∃ 𝑓 ∈ 𝐶 ∃ 𝑖 ∈ 𝐶 ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( ( 𝑝 𝑈 𝑞 ∧ 𝑞 𝑈 𝑟 ) → 𝑝 𝑈 𝑟 ) ) )
193 192 rexlimdvw ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ 𝐶 ∃ 𝑓 ∈ 𝐶 ∃ 𝑖 ∈ 𝐶 ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( ( 𝑝 𝑈 𝑞 ∧ 𝑞 𝑈 𝑟 ) → 𝑝 𝑈 𝑟 ) ) )
194 193 rexlimdvw ⊢ ( 𝜑 → ( ∃ ℎ ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑓 ∈ 𝐶 ∃ 𝑖 ∈ 𝐶 ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( ( 𝑝 𝑈 𝑞 ∧ 𝑞 𝑈 𝑟 ) → 𝑝 𝑈 𝑟 ) ) )
195 194 rexlimdvw ⊢ ( 𝜑 → ( ∃ 𝑒 ∈ 𝐵 ∃ ℎ ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑓 ∈ 𝐶 ∃ 𝑖 ∈ 𝐶 ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( ( 𝑝 𝑈 𝑞 ∧ 𝑞 𝑈 𝑟 ) → 𝑝 𝑈 𝑟 ) ) )
196 195 rexlimdvw ⊢ ( 𝜑 → ( ∃ 𝑏 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 ∃ ℎ ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑓 ∈ 𝐶 ∃ 𝑖 ∈ 𝐶 ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( ( 𝑝 𝑈 𝑞 ∧ 𝑞 𝑈 𝑟 ) → 𝑝 𝑈 𝑟 ) ) )
197 196 rexlimdvw ⊢ ( 𝜑 → ( ∃ 𝑔 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 ∃ ℎ ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑓 ∈ 𝐶 ∃ 𝑖 ∈ 𝐶 ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( ( 𝑝 𝑈 𝑞 ∧ 𝑞 𝑈 𝑟 ) → 𝑝 𝑈 𝑟 ) ) )
198 197 rexlimdvw ⊢ ( 𝜑 → ( ∃ 𝑑 ∈ 𝐴 ∃ 𝑔 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 ∃ ℎ ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑓 ∈ 𝐶 ∃ 𝑖 ∈ 𝐶 ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( ( 𝑝 𝑈 𝑞 ∧ 𝑞 𝑈 𝑟 ) → 𝑝 𝑈 𝑟 ) ) )
199 198 rexlimdvw ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝐴 ∃ 𝑑 ∈ 𝐴 ∃ 𝑔 ∈ 𝐴 ∃ 𝑏 ∈ 𝐵 ∃ 𝑒 ∈ 𝐵 ∃ ℎ ∈ 𝐵 ∃ 𝑐 ∈ 𝐶 ∃ 𝑓 ∈ 𝐶 ∃ 𝑖 ∈ 𝐶 ( 𝑝 = ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∧ 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∧ 𝑟 = ⟨ 𝑔 , ℎ , 𝑖 ⟩ ) → ( ( 𝑝 𝑈 𝑞 ∧ 𝑞 𝑈 𝑟 ) → 𝑝 𝑈 𝑟 ) ) )
200 34 199 biimtrid ⊢ ( 𝜑 → ( ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑟 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) → ( ( 𝑝 𝑈 𝑞 ∧ 𝑞 𝑈 𝑟 ) → 𝑝 𝑈 𝑟 ) ) )
201 200 imp ⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑟 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) ) → ( ( 𝑝 𝑈 𝑞 ∧ 𝑞 𝑈 𝑟 ) → 𝑝 𝑈 𝑟 ) )
202 22 201 ispod ⊢ ( 𝜑 → 𝑈 Po ( ( 𝐴 × 𝐵 ) × 𝐶 ) )