Metamath Proof Explorer


Theorem poxp3

Description: Triple cross 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 elxpxp ( 𝑎 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ∃ 𝑑𝐴𝑒𝐵𝑓𝐶 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ )
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 a1i ( ( 𝑑𝐴𝑒𝐵 ) → ( ∃ 𝑓𝐶 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ¬ 𝑎 𝑈 𝑎 ) )
20 19 rexlimivv ( ∃ 𝑑𝐴𝑒𝐵𝑓𝐶 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ¬ 𝑎 𝑈 𝑎 )
21 5 20 sylbi ( 𝑎 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ¬ 𝑎 𝑈 𝑎 )
22 21 adantl ( ( 𝜑𝑎 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) → ¬ 𝑎 𝑈 𝑎 )
23 elxpxp ( 𝑏 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ∃ 𝑔𝐴𝐵𝑖𝐶 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ )
24 elxpxp ( 𝑐 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ∃ 𝑗𝐴𝑘𝐵𝑙𝐶 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ )
25 5 23 24 3anbi123i ( ( 𝑎 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑏 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑐 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) ↔ ( ∃ 𝑑𝐴𝑒𝐵𝑓𝐶 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ ∃ 𝑔𝐴𝐵𝑖𝐶 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ ∃ 𝑗𝐴𝑘𝐵𝑙𝐶 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) )
26 3reeanv ( ∃ 𝑓𝐶𝑖𝐶𝑙𝐶 ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) ↔ ( ∃ 𝑓𝐶 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ ∃ 𝑖𝐶 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ ∃ 𝑙𝐶 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) )
27 26 rexbii ( ∃ 𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) ↔ ∃ 𝑘𝐵 ( ∃ 𝑓𝐶 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ ∃ 𝑖𝐶 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ ∃ 𝑙𝐶 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) )
28 27 2rexbii ( ∃ 𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) ↔ ∃ 𝑒𝐵𝐵𝑘𝐵 ( ∃ 𝑓𝐶 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ ∃ 𝑖𝐶 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ ∃ 𝑙𝐶 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) )
29 3reeanv ( ∃ 𝑒𝐵𝐵𝑘𝐵 ( ∃ 𝑓𝐶 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ ∃ 𝑖𝐶 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ ∃ 𝑙𝐶 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) ↔ ( ∃ 𝑒𝐵𝑓𝐶 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ ∃ 𝐵𝑖𝐶 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ ∃ 𝑘𝐵𝑙𝐶 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) )
30 28 29 bitri ( ∃ 𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) ↔ ( ∃ 𝑒𝐵𝑓𝐶 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ ∃ 𝐵𝑖𝐶 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ ∃ 𝑘𝐵𝑙𝐶 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) )
31 30 rexbii ( ∃ 𝑗𝐴𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) ↔ ∃ 𝑗𝐴 ( ∃ 𝑒𝐵𝑓𝐶 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ ∃ 𝐵𝑖𝐶 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ ∃ 𝑘𝐵𝑙𝐶 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) )
32 31 2rexbii ( ∃ 𝑑𝐴𝑔𝐴𝑗𝐴𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) ↔ ∃ 𝑑𝐴𝑔𝐴𝑗𝐴 ( ∃ 𝑒𝐵𝑓𝐶 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ ∃ 𝐵𝑖𝐶 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ ∃ 𝑘𝐵𝑙𝐶 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) )
33 3reeanv ( ∃ 𝑑𝐴𝑔𝐴𝑗𝐴 ( ∃ 𝑒𝐵𝑓𝐶 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ ∃ 𝐵𝑖𝐶 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ ∃ 𝑘𝐵𝑙𝐶 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) ↔ ( ∃ 𝑑𝐴𝑒𝐵𝑓𝐶 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ ∃ 𝑔𝐴𝐵𝑖𝐶 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ ∃ 𝑗𝐴𝑘𝐵𝑙𝐶 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) )
34 32 33 bitri ( ∃ 𝑑𝐴𝑔𝐴𝑗𝐴𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) ↔ ( ∃ 𝑑𝐴𝑒𝐵𝑓𝐶 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ ∃ 𝑔𝐴𝐵𝑖𝐶 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ ∃ 𝑗𝐴𝑘𝐵𝑙𝐶 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) )
35 25 34 bitr4i ( ( 𝑎 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑏 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑐 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) ↔ ∃ 𝑑𝐴𝑔𝐴𝑗𝐴𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) )
36 simprl1 ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) )
37 simprr2 ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) )
38 2 adantr ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → 𝑅 Po 𝐴 )
39 simpl11 ( ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) → 𝑑𝐴 )
40 39 adantl ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → 𝑑𝐴 )
41 simpr11 ( ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) → 𝑔𝐴 )
42 41 adantl ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → 𝑔𝐴 )
43 simpr21 ( ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) → 𝑗𝐴 )
44 43 adantl ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → 𝑗𝐴 )
45 potr ( ( 𝑅 Po 𝐴 ∧ ( 𝑑𝐴𝑔𝐴𝑗𝐴 ) ) → ( ( 𝑑 𝑅 𝑔𝑔 𝑅 𝑗 ) → 𝑑 𝑅 𝑗 ) )
46 38 40 42 44 45 syl13anc ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( ( 𝑑 𝑅 𝑔𝑔 𝑅 𝑗 ) → 𝑑 𝑅 𝑗 ) )
47 orc ( 𝑑 𝑅 𝑗 → ( 𝑑 𝑅 𝑗𝑑 = 𝑗 ) )
48 46 47 syl6 ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( ( 𝑑 𝑅 𝑔𝑔 𝑅 𝑗 ) → ( 𝑑 𝑅 𝑗𝑑 = 𝑗 ) ) )
49 48 expd ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑑 𝑅 𝑔 → ( 𝑔 𝑅 𝑗 → ( 𝑑 𝑅 𝑗𝑑 = 𝑗 ) ) ) )
50 breq1 ( 𝑑 = 𝑔 → ( 𝑑 𝑅 𝑗𝑔 𝑅 𝑗 ) )
51 50 47 syl6bir ( 𝑑 = 𝑔 → ( 𝑔 𝑅 𝑗 → ( 𝑑 𝑅 𝑗𝑑 = 𝑗 ) ) )
52 51 a1i ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑑 = 𝑔 → ( 𝑔 𝑅 𝑗 → ( 𝑑 𝑅 𝑗𝑑 = 𝑗 ) ) ) )
53 simp3l1 ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) → ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) )
54 53 ad2antrl ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) )
55 49 52 54 mpjaod ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑔 𝑅 𝑗 → ( 𝑑 𝑅 𝑗𝑑 = 𝑗 ) ) )
56 breq2 ( 𝑔 = 𝑗 → ( 𝑑 𝑅 𝑔𝑑 𝑅 𝑗 ) )
57 equequ2 ( 𝑔 = 𝑗 → ( 𝑑 = 𝑔𝑑 = 𝑗 ) )
58 56 57 orbi12d ( 𝑔 = 𝑗 → ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ↔ ( 𝑑 𝑅 𝑗𝑑 = 𝑗 ) ) )
59 54 58 syl5ibcom ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑔 = 𝑗 → ( 𝑑 𝑅 𝑗𝑑 = 𝑗 ) ) )
60 simp3l1 ( ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) → ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) )
61 60 ad2antll ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) )
62 55 59 61 mpjaod ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑑 𝑅 𝑗𝑑 = 𝑗 ) )
63 3 adantr ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → 𝑆 Po 𝐵 )
64 simpl12 ( ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) → 𝑒𝐵 )
65 64 adantl ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → 𝑒𝐵 )
66 simpr12 ( ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) → 𝐵 )
67 66 adantl ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → 𝐵 )
68 simpr22 ( ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) → 𝑘𝐵 )
69 68 adantl ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → 𝑘𝐵 )
70 potr ( ( 𝑆 Po 𝐵 ∧ ( 𝑒𝐵𝐵𝑘𝐵 ) ) → ( ( 𝑒 𝑆 𝑆 𝑘 ) → 𝑒 𝑆 𝑘 ) )
71 63 65 67 69 70 syl13anc ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( ( 𝑒 𝑆 𝑆 𝑘 ) → 𝑒 𝑆 𝑘 ) )
72 orc ( 𝑒 𝑆 𝑘 → ( 𝑒 𝑆 𝑘𝑒 = 𝑘 ) )
73 71 72 syl6 ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( ( 𝑒 𝑆 𝑆 𝑘 ) → ( 𝑒 𝑆 𝑘𝑒 = 𝑘 ) ) )
74 73 expd ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑒 𝑆 → ( 𝑆 𝑘 → ( 𝑒 𝑆 𝑘𝑒 = 𝑘 ) ) ) )
75 breq1 ( 𝑒 = → ( 𝑒 𝑆 𝑘 𝑆 𝑘 ) )
76 75 72 syl6bir ( 𝑒 = → ( 𝑆 𝑘 → ( 𝑒 𝑆 𝑘𝑒 = 𝑘 ) ) )
77 76 a1i ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑒 = → ( 𝑆 𝑘 → ( 𝑒 𝑆 𝑘𝑒 = 𝑘 ) ) ) )
78 simp3l2 ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) → ( 𝑒 𝑆 𝑒 = ) )
79 78 ad2antrl ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑒 𝑆 𝑒 = ) )
80 74 77 79 mpjaod ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑆 𝑘 → ( 𝑒 𝑆 𝑘𝑒 = 𝑘 ) ) )
81 breq2 ( = 𝑘 → ( 𝑒 𝑆 𝑒 𝑆 𝑘 ) )
82 equequ2 ( = 𝑘 → ( 𝑒 = 𝑒 = 𝑘 ) )
83 81 82 orbi12d ( = 𝑘 → ( ( 𝑒 𝑆 𝑒 = ) ↔ ( 𝑒 𝑆 𝑘𝑒 = 𝑘 ) ) )
84 79 83 syl5ibcom ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( = 𝑘 → ( 𝑒 𝑆 𝑘𝑒 = 𝑘 ) ) )
85 simp3l2 ( ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) → ( 𝑆 𝑘 = 𝑘 ) )
86 85 ad2antll ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑆 𝑘 = 𝑘 ) )
87 80 84 86 mpjaod ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑒 𝑆 𝑘𝑒 = 𝑘 ) )
88 4 adantr ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → 𝑇 Po 𝐶 )
89 simpl13 ( ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) → 𝑓𝐶 )
90 89 adantl ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → 𝑓𝐶 )
91 simpr13 ( ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) → 𝑖𝐶 )
92 91 adantl ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → 𝑖𝐶 )
93 simpr23 ( ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) → 𝑙𝐶 )
94 93 adantl ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → 𝑙𝐶 )
95 potr ( ( 𝑇 Po 𝐶 ∧ ( 𝑓𝐶𝑖𝐶𝑙𝐶 ) ) → ( ( 𝑓 𝑇 𝑖𝑖 𝑇 𝑙 ) → 𝑓 𝑇 𝑙 ) )
96 88 90 92 94 95 syl13anc ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( ( 𝑓 𝑇 𝑖𝑖 𝑇 𝑙 ) → 𝑓 𝑇 𝑙 ) )
97 orc ( 𝑓 𝑇 𝑙 → ( 𝑓 𝑇 𝑙𝑓 = 𝑙 ) )
98 96 97 syl6 ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( ( 𝑓 𝑇 𝑖𝑖 𝑇 𝑙 ) → ( 𝑓 𝑇 𝑙𝑓 = 𝑙 ) ) )
99 98 expd ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑓 𝑇 𝑖 → ( 𝑖 𝑇 𝑙 → ( 𝑓 𝑇 𝑙𝑓 = 𝑙 ) ) ) )
100 breq1 ( 𝑓 = 𝑖 → ( 𝑓 𝑇 𝑙𝑖 𝑇 𝑙 ) )
101 100 97 syl6bir ( 𝑓 = 𝑖 → ( 𝑖 𝑇 𝑙 → ( 𝑓 𝑇 𝑙𝑓 = 𝑙 ) ) )
102 101 a1i ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑓 = 𝑖 → ( 𝑖 𝑇 𝑙 → ( 𝑓 𝑇 𝑙𝑓 = 𝑙 ) ) ) )
103 simp3l3 ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) → ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) )
104 103 ad2antrl ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) )
105 99 102 104 mpjaod ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑖 𝑇 𝑙 → ( 𝑓 𝑇 𝑙𝑓 = 𝑙 ) ) )
106 breq2 ( 𝑖 = 𝑙 → ( 𝑓 𝑇 𝑖𝑓 𝑇 𝑙 ) )
107 equequ2 ( 𝑖 = 𝑙 → ( 𝑓 = 𝑖𝑓 = 𝑙 ) )
108 106 107 orbi12d ( 𝑖 = 𝑙 → ( ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ↔ ( 𝑓 𝑇 𝑙𝑓 = 𝑙 ) ) )
109 104 108 syl5ibcom ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑖 = 𝑙 → ( 𝑓 𝑇 𝑙𝑓 = 𝑙 ) ) )
110 simp3l3 ( ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) → ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) )
111 110 ad2antll ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) )
112 105 109 111 mpjaod ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑓 𝑇 𝑙𝑓 = 𝑙 ) )
113 62 87 112 3jca ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( ( 𝑑 𝑅 𝑗𝑑 = 𝑗 ) ∧ ( 𝑒 𝑆 𝑘𝑒 = 𝑘 ) ∧ ( 𝑓 𝑇 𝑙𝑓 = 𝑙 ) ) )
114 simpr3r ( ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) → ( 𝑔𝑗𝑘𝑖𝑙 ) )
115 114 adantl ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑔𝑗𝑘𝑖𝑙 ) )
116 df-ne ( 𝑔𝑗 ↔ ¬ 𝑔 = 𝑗 )
117 df-ne ( 𝑘 ↔ ¬ = 𝑘 )
118 df-ne ( 𝑖𝑙 ↔ ¬ 𝑖 = 𝑙 )
119 116 117 118 3orbi123i ( ( 𝑔𝑗𝑘𝑖𝑙 ) ↔ ( ¬ 𝑔 = 𝑗 ∨ ¬ = 𝑘 ∨ ¬ 𝑖 = 𝑙 ) )
120 3ianor ( ¬ ( 𝑔 = 𝑗 = 𝑘𝑖 = 𝑙 ) ↔ ( ¬ 𝑔 = 𝑗 ∨ ¬ = 𝑘 ∨ ¬ 𝑖 = 𝑙 ) )
121 119 120 bitr4i ( ( 𝑔𝑗𝑘𝑖𝑙 ) ↔ ¬ ( 𝑔 = 𝑗 = 𝑘𝑖 = 𝑙 ) )
122 115 121 sylib ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ¬ ( 𝑔 = 𝑗 = 𝑘𝑖 = 𝑙 ) )
123 df-ne ( 𝑑𝑗 ↔ ¬ 𝑑 = 𝑗 )
124 df-ne ( 𝑒𝑘 ↔ ¬ 𝑒 = 𝑘 )
125 df-ne ( 𝑓𝑙 ↔ ¬ 𝑓 = 𝑙 )
126 123 124 125 3orbi123i ( ( 𝑑𝑗𝑒𝑘𝑓𝑙 ) ↔ ( ¬ 𝑑 = 𝑗 ∨ ¬ 𝑒 = 𝑘 ∨ ¬ 𝑓 = 𝑙 ) )
127 3ianor ( ¬ ( 𝑑 = 𝑗𝑒 = 𝑘𝑓 = 𝑙 ) ↔ ( ¬ 𝑑 = 𝑗 ∨ ¬ 𝑒 = 𝑘 ∨ ¬ 𝑓 = 𝑙 ) )
128 126 127 bitr4i ( ( 𝑑𝑗𝑒𝑘𝑓𝑙 ) ↔ ¬ ( 𝑑 = 𝑗𝑒 = 𝑘𝑓 = 𝑙 ) )
129 128 con2bii ( ( 𝑑 = 𝑗𝑒 = 𝑘𝑓 = 𝑙 ) ↔ ¬ ( 𝑑𝑗𝑒𝑘𝑓𝑙 ) )
130 breq1 ( 𝑑 = 𝑗 → ( 𝑑 𝑅 𝑔𝑗 𝑅 𝑔 ) )
131 equequ1 ( 𝑑 = 𝑗 → ( 𝑑 = 𝑔𝑗 = 𝑔 ) )
132 equcom ( 𝑗 = 𝑔𝑔 = 𝑗 )
133 131 132 bitrdi ( 𝑑 = 𝑗 → ( 𝑑 = 𝑔𝑔 = 𝑗 ) )
134 130 133 orbi12d ( 𝑑 = 𝑗 → ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ↔ ( 𝑗 𝑅 𝑔𝑔 = 𝑗 ) ) )
135 54 134 syl5ibcom ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑑 = 𝑗 → ( 𝑗 𝑅 𝑔𝑔 = 𝑗 ) ) )
136 135 imp ( ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) ∧ 𝑑 = 𝑗 ) → ( 𝑗 𝑅 𝑔𝑔 = 𝑗 ) )
137 61 adantr ( ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) ∧ 𝑑 = 𝑗 ) → ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) )
138 ordir ( ( ( 𝑗 𝑅 𝑔𝑔 𝑅 𝑗 ) ∨ 𝑔 = 𝑗 ) ↔ ( ( 𝑗 𝑅 𝑔𝑔 = 𝑗 ) ∧ ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ) )
139 136 137 138 sylanbrc ( ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) ∧ 𝑑 = 𝑗 ) → ( ( 𝑗 𝑅 𝑔𝑔 𝑅 𝑗 ) ∨ 𝑔 = 𝑗 ) )
140 po2nr ( ( 𝑅 Po 𝐴 ∧ ( 𝑗𝐴𝑔𝐴 ) ) → ¬ ( 𝑗 𝑅 𝑔𝑔 𝑅 𝑗 ) )
141 38 44 42 140 syl12anc ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ¬ ( 𝑗 𝑅 𝑔𝑔 𝑅 𝑗 ) )
142 141 adantr ( ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) ∧ 𝑑 = 𝑗 ) → ¬ ( 𝑗 𝑅 𝑔𝑔 𝑅 𝑗 ) )
143 139 142 orcnd ( ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) ∧ 𝑑 = 𝑗 ) → 𝑔 = 𝑗 )
144 143 ex ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑑 = 𝑗𝑔 = 𝑗 ) )
145 breq1 ( 𝑒 = 𝑘 → ( 𝑒 𝑆 𝑘 𝑆 ) )
146 equequ1 ( 𝑒 = 𝑘 → ( 𝑒 = 𝑘 = ) )
147 equcom ( 𝑘 = = 𝑘 )
148 146 147 bitrdi ( 𝑒 = 𝑘 → ( 𝑒 = = 𝑘 ) )
149 145 148 orbi12d ( 𝑒 = 𝑘 → ( ( 𝑒 𝑆 𝑒 = ) ↔ ( 𝑘 𝑆 = 𝑘 ) ) )
150 79 149 syl5ibcom ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑒 = 𝑘 → ( 𝑘 𝑆 = 𝑘 ) ) )
151 150 imp ( ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) ∧ 𝑒 = 𝑘 ) → ( 𝑘 𝑆 = 𝑘 ) )
152 86 adantr ( ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) ∧ 𝑒 = 𝑘 ) → ( 𝑆 𝑘 = 𝑘 ) )
153 ordir ( ( ( 𝑘 𝑆 𝑆 𝑘 ) ∨ = 𝑘 ) ↔ ( ( 𝑘 𝑆 = 𝑘 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ) )
154 151 152 153 sylanbrc ( ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) ∧ 𝑒 = 𝑘 ) → ( ( 𝑘 𝑆 𝑆 𝑘 ) ∨ = 𝑘 ) )
155 po2nr ( ( 𝑆 Po 𝐵 ∧ ( 𝑘𝐵𝐵 ) ) → ¬ ( 𝑘 𝑆 𝑆 𝑘 ) )
156 63 69 67 155 syl12anc ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ¬ ( 𝑘 𝑆 𝑆 𝑘 ) )
157 156 adantr ( ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) ∧ 𝑒 = 𝑘 ) → ¬ ( 𝑘 𝑆 𝑆 𝑘 ) )
158 154 157 orcnd ( ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) ∧ 𝑒 = 𝑘 ) → = 𝑘 )
159 158 ex ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑒 = 𝑘 = 𝑘 ) )
160 breq1 ( 𝑓 = 𝑙 → ( 𝑓 𝑇 𝑖𝑙 𝑇 𝑖 ) )
161 equequ1 ( 𝑓 = 𝑙 → ( 𝑓 = 𝑖𝑙 = 𝑖 ) )
162 160 161 orbi12d ( 𝑓 = 𝑙 → ( ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ↔ ( 𝑙 𝑇 𝑖𝑙 = 𝑖 ) ) )
163 104 162 syl5ibcom ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑓 = 𝑙 → ( 𝑙 𝑇 𝑖𝑙 = 𝑖 ) ) )
164 163 imp ( ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) ∧ 𝑓 = 𝑙 ) → ( 𝑙 𝑇 𝑖𝑙 = 𝑖 ) )
165 equcom ( 𝑙 = 𝑖𝑖 = 𝑙 )
166 165 orbi2i ( ( 𝑙 𝑇 𝑖𝑙 = 𝑖 ) ↔ ( 𝑙 𝑇 𝑖𝑖 = 𝑙 ) )
167 164 166 sylib ( ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) ∧ 𝑓 = 𝑙 ) → ( 𝑙 𝑇 𝑖𝑖 = 𝑙 ) )
168 111 adantr ( ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) ∧ 𝑓 = 𝑙 ) → ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) )
169 ordir ( ( ( 𝑙 𝑇 𝑖𝑖 𝑇 𝑙 ) ∨ 𝑖 = 𝑙 ) ↔ ( ( 𝑙 𝑇 𝑖𝑖 = 𝑙 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) )
170 167 168 169 sylanbrc ( ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) ∧ 𝑓 = 𝑙 ) → ( ( 𝑙 𝑇 𝑖𝑖 𝑇 𝑙 ) ∨ 𝑖 = 𝑙 ) )
171 po2nr ( ( 𝑇 Po 𝐶 ∧ ( 𝑙𝐶𝑖𝐶 ) ) → ¬ ( 𝑙 𝑇 𝑖𝑖 𝑇 𝑙 ) )
172 88 94 92 171 syl12anc ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ¬ ( 𝑙 𝑇 𝑖𝑖 𝑇 𝑙 ) )
173 172 adantr ( ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) ∧ 𝑓 = 𝑙 ) → ¬ ( 𝑙 𝑇 𝑖𝑖 𝑇 𝑙 ) )
174 170 173 orcnd ( ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) ∧ 𝑓 = 𝑙 ) → 𝑖 = 𝑙 )
175 174 ex ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑓 = 𝑙𝑖 = 𝑙 ) )
176 144 159 175 3anim123d ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( ( 𝑑 = 𝑗𝑒 = 𝑘𝑓 = 𝑙 ) → ( 𝑔 = 𝑗 = 𝑘𝑖 = 𝑙 ) ) )
177 129 176 syl5bir ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( ¬ ( 𝑑𝑗𝑒𝑘𝑓𝑙 ) → ( 𝑔 = 𝑗 = 𝑘𝑖 = 𝑙 ) ) )
178 122 177 mt3d ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( 𝑑𝑗𝑒𝑘𝑓𝑙 ) )
179 113 178 jca ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( ( ( 𝑑 𝑅 𝑗𝑑 = 𝑗 ) ∧ ( 𝑒 𝑆 𝑘𝑒 = 𝑘 ) ∧ ( 𝑓 𝑇 𝑙𝑓 = 𝑙 ) ) ∧ ( 𝑑𝑗𝑒𝑘𝑓𝑙 ) ) )
180 36 37 179 3jca ( ( 𝜑 ∧ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) → ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑗𝑑 = 𝑗 ) ∧ ( 𝑒 𝑆 𝑘𝑒 = 𝑘 ) ∧ ( 𝑓 𝑇 𝑙𝑓 = 𝑙 ) ) ∧ ( 𝑑𝑗𝑒𝑘𝑓𝑙 ) ) ) )
181 180 ex ( 𝜑 → ( ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) → ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑗𝑑 = 𝑗 ) ∧ ( 𝑒 𝑆 𝑘𝑒 = 𝑘 ) ∧ ( 𝑓 𝑇 𝑙𝑓 = 𝑙 ) ) ∧ ( 𝑑𝑗𝑒𝑘𝑓𝑙 ) ) ) ) )
182 breq12 ( ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ) → ( 𝑎 𝑈 𝑏 ↔ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓𝑈 ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ) )
183 182 3adant3 ( ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( 𝑎 𝑈 𝑏 ↔ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓𝑈 ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ) )
184 1 xpord3lem ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓𝑈 ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ↔ ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) )
185 183 184 bitrdi ( ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( 𝑎 𝑈 𝑏 ↔ ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ) )
186 breq12 ( ( 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( 𝑏 𝑈 𝑐 ↔ ⟨ ⟨ 𝑔 , ⟩ , 𝑖𝑈 ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) )
187 186 3adant1 ( ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( 𝑏 𝑈 𝑐 ↔ ⟨ ⟨ 𝑔 , ⟩ , 𝑖𝑈 ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) )
188 1 xpord3lem ( ⟨ ⟨ 𝑔 , ⟩ , 𝑖𝑈 ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ↔ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) )
189 187 188 bitrdi ( ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( 𝑏 𝑈 𝑐 ↔ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) )
190 185 189 anbi12d ( ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( ( 𝑎 𝑈 𝑏𝑏 𝑈 𝑐 ) ↔ ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) ) )
191 breq12 ( ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( 𝑎 𝑈 𝑐 ↔ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓𝑈 ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) )
192 191 3adant2 ( ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( 𝑎 𝑈 𝑐 ↔ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓𝑈 ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) )
193 1 xpord3lem ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓𝑈 ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ↔ ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑗𝑑 = 𝑗 ) ∧ ( 𝑒 𝑆 𝑘𝑒 = 𝑘 ) ∧ ( 𝑓 𝑇 𝑙𝑓 = 𝑙 ) ) ∧ ( 𝑑𝑗𝑒𝑘𝑓𝑙 ) ) ) )
194 192 193 bitrdi ( ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( 𝑎 𝑈 𝑐 ↔ ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑗𝑑 = 𝑗 ) ∧ ( 𝑒 𝑆 𝑘𝑒 = 𝑘 ) ∧ ( 𝑓 𝑇 𝑙𝑓 = 𝑙 ) ) ∧ ( 𝑑𝑗𝑒𝑘𝑓𝑙 ) ) ) ) )
195 190 194 imbi12d ( ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( ( ( 𝑎 𝑈 𝑏𝑏 𝑈 𝑐 ) → 𝑎 𝑈 𝑐 ) ↔ ( ( ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑔𝑑 = 𝑔 ) ∧ ( 𝑒 𝑆 𝑒 = ) ∧ ( 𝑓 𝑇 𝑖𝑓 = 𝑖 ) ) ∧ ( 𝑑𝑔𝑒𝑓𝑖 ) ) ) ∧ ( ( 𝑔𝐴𝐵𝑖𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑔 𝑅 𝑗𝑔 = 𝑗 ) ∧ ( 𝑆 𝑘 = 𝑘 ) ∧ ( 𝑖 𝑇 𝑙𝑖 = 𝑙 ) ) ∧ ( 𝑔𝑗𝑘𝑖𝑙 ) ) ) ) → ( ( 𝑑𝐴𝑒𝐵𝑓𝐶 ) ∧ ( 𝑗𝐴𝑘𝐵𝑙𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑗𝑑 = 𝑗 ) ∧ ( 𝑒 𝑆 𝑘𝑒 = 𝑘 ) ∧ ( 𝑓 𝑇 𝑙𝑓 = 𝑙 ) ) ∧ ( 𝑑𝑗𝑒𝑘𝑓𝑙 ) ) ) ) ) )
196 181 195 syl5ibrcom ( 𝜑 → ( ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( ( 𝑎 𝑈 𝑏𝑏 𝑈 𝑐 ) → 𝑎 𝑈 𝑐 ) ) )
197 196 rexlimdvw ( 𝜑 → ( ∃ 𝑙𝐶 ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( ( 𝑎 𝑈 𝑏𝑏 𝑈 𝑐 ) → 𝑎 𝑈 𝑐 ) ) )
198 197 a1d ( 𝜑 → ( ( 𝑓𝐶𝑖𝐶 ) → ( ∃ 𝑙𝐶 ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( ( 𝑎 𝑈 𝑏𝑏 𝑈 𝑐 ) → 𝑎 𝑈 𝑐 ) ) ) )
199 198 rexlimdvv ( 𝜑 → ( ∃ 𝑓𝐶𝑖𝐶𝑙𝐶 ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( ( 𝑎 𝑈 𝑏𝑏 𝑈 𝑐 ) → 𝑎 𝑈 𝑐 ) ) )
200 199 rexlimdvw ( 𝜑 → ( ∃ 𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( ( 𝑎 𝑈 𝑏𝑏 𝑈 𝑐 ) → 𝑎 𝑈 𝑐 ) ) )
201 200 a1d ( 𝜑 → ( ( 𝑒𝐵𝐵 ) → ( ∃ 𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( ( 𝑎 𝑈 𝑏𝑏 𝑈 𝑐 ) → 𝑎 𝑈 𝑐 ) ) ) )
202 201 rexlimdvv ( 𝜑 → ( ∃ 𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( ( 𝑎 𝑈 𝑏𝑏 𝑈 𝑐 ) → 𝑎 𝑈 𝑐 ) ) )
203 202 rexlimdvw ( 𝜑 → ( ∃ 𝑗𝐴𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( ( 𝑎 𝑈 𝑏𝑏 𝑈 𝑐 ) → 𝑎 𝑈 𝑐 ) ) )
204 203 a1d ( 𝜑 → ( ( 𝑑𝐴𝑔𝐴 ) → ( ∃ 𝑗𝐴𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( ( 𝑎 𝑈 𝑏𝑏 𝑈 𝑐 ) → 𝑎 𝑈 𝑐 ) ) ) )
205 204 rexlimdvv ( 𝜑 → ( ∃ 𝑑𝐴𝑔𝐴𝑗𝐴𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 ( 𝑎 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∧ 𝑏 = ⟨ ⟨ 𝑔 , ⟩ , 𝑖 ⟩ ∧ 𝑐 = ⟨ ⟨ 𝑗 , 𝑘 ⟩ , 𝑙 ⟩ ) → ( ( 𝑎 𝑈 𝑏𝑏 𝑈 𝑐 ) → 𝑎 𝑈 𝑐 ) ) )
206 35 205 syl5bi ( 𝜑 → ( ( 𝑎 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑏 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑐 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) → ( ( 𝑎 𝑈 𝑏𝑏 𝑈 𝑐 ) → 𝑎 𝑈 𝑐 ) ) )
207 206 imp ( ( 𝜑 ∧ ( 𝑎 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑏 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑐 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) ) → ( ( 𝑎 𝑈 𝑏𝑏 𝑈 𝑐 ) → 𝑎 𝑈 𝑐 ) )
208 22 207 ispod ( 𝜑𝑈 Po ( ( 𝐴 × 𝐵 ) × 𝐶 ) )