Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poxp3 Structured version   Visualization version   GIF version

Theorem poxp3 33399
Description: Triple cross product partial ordering. (Contributed by Scott Fenton, 21-Aug-2024.)
Hypotheses
Ref Expression
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
Ref Expression
poxp3 (𝜑𝑈 Po ((𝐴 × 𝐵) × 𝐶))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝑅,𝑦   𝑥,𝑆,𝑦   𝑥,𝑇,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑈(𝑥,𝑦)

Proof of Theorem poxp3
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑔 𝑖 𝑗 𝑘 𝑙 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxpxp 33249 . . . 4 (𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑑𝐴𝑒𝐵𝑓𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩)
2 neirr 2943 . . . . . . . . . . 11 ¬ 𝑑𝑑
3 neirr 2943 . . . . . . . . . . 11 ¬ 𝑒𝑒
4 neirr 2943 . . . . . . . . . . 11 ¬ 𝑓𝑓
52, 3, 43pm3.2ni 33221 . . . . . . . . . 10 ¬ (𝑑𝑑𝑒𝑒𝑓𝑓)
65intnan 490 . . . . . . . . 9 ¬ (((𝑑𝑅𝑑𝑑 = 𝑑) ∧ (𝑒𝑆𝑒𝑒 = 𝑒) ∧ (𝑓𝑇𝑓𝑓 = 𝑓)) ∧ (𝑑𝑑𝑒𝑒𝑓𝑓))
7 simp3 1139 . . . . . . . . 9 (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (((𝑑𝑅𝑑𝑑 = 𝑑) ∧ (𝑒𝑆𝑒𝑒 = 𝑒) ∧ (𝑓𝑇𝑓𝑓 = 𝑓)) ∧ (𝑑𝑑𝑒𝑒𝑓𝑓))) → (((𝑑𝑅𝑑𝑑 = 𝑑) ∧ (𝑒𝑆𝑒𝑒 = 𝑒) ∧ (𝑓𝑇𝑓𝑓 = 𝑓)) ∧ (𝑑𝑑𝑒𝑒𝑓𝑓)))
86, 7mto 200 . . . . . . . 8 ¬ ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (((𝑑𝑅𝑑𝑑 = 𝑑) ∧ (𝑒𝑆𝑒𝑒 = 𝑒) ∧ (𝑓𝑇𝑓𝑓 = 𝑓)) ∧ (𝑑𝑑𝑒𝑒𝑓𝑓)))
9 breq12 5032 . . . . . . . . . 10 ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩) → (𝑎𝑈𝑎 ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓𝑈⟨⟨𝑑, 𝑒⟩, 𝑓⟩))
109anidms 570 . . . . . . . . 9 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑎𝑈𝑎 ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓𝑈⟨⟨𝑑, 𝑒⟩, 𝑓⟩))
11 xpord3.1 . . . . . . . . . 10 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st𝑥))𝑅(1st ‘(1st𝑦)) ∨ (1st ‘(1st𝑥)) = (1st ‘(1st𝑦))) ∧ ((2nd ‘(1st𝑥))𝑆(2nd ‘(1st𝑦)) ∨ (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦))) ∧ ((2nd𝑥)𝑇(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦))) ∧ 𝑥𝑦))}
1211xpord3lem 33398 . . . . . . . . 9 (⟨⟨𝑑, 𝑒⟩, 𝑓𝑈⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ↔ ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (((𝑑𝑅𝑑𝑑 = 𝑑) ∧ (𝑒𝑆𝑒𝑒 = 𝑒) ∧ (𝑓𝑇𝑓𝑓 = 𝑓)) ∧ (𝑑𝑑𝑒𝑒𝑓𝑓))))
1310, 12bitrdi 290 . . . . . . . 8 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑎𝑈𝑎 ↔ ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (((𝑑𝑅𝑑𝑑 = 𝑑) ∧ (𝑒𝑆𝑒𝑒 = 𝑒) ∧ (𝑓𝑇𝑓𝑓 = 𝑓)) ∧ (𝑑𝑑𝑒𝑒𝑓𝑓)))))
148, 13mtbiri 330 . . . . . . 7 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ¬ 𝑎𝑈𝑎)
1514rexlimivw 3191 . . . . . 6 (∃𝑓𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ¬ 𝑎𝑈𝑎)
1615a1i 11 . . . . 5 ((𝑑𝐴𝑒𝐵) → (∃𝑓𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ¬ 𝑎𝑈𝑎))
1716rexlimivv 3201 . . . 4 (∃𝑑𝐴𝑒𝐵𝑓𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ¬ 𝑎𝑈𝑎)
181, 17sylbi 220 . . 3 (𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) → ¬ 𝑎𝑈𝑎)
1918adantl 485 . 2 ((𝜑𝑎 ∈ ((𝐴 × 𝐵) × 𝐶)) → ¬ 𝑎𝑈𝑎)
20 elxpxp 33249 . . . . . 6 (𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑔𝐴𝐵𝑖𝐶 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩)
21 elxpxp 33249 . . . . . 6 (𝑐 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑗𝐴𝑘𝐵𝑙𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩)
221, 20, 213anbi123i 1156 . . . . 5 ((𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑐 ∈ ((𝐴 × 𝐵) × 𝐶)) ↔ (∃𝑑𝐴𝑒𝐵𝑓𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑔𝐴𝐵𝑖𝐶 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ ∃𝑗𝐴𝑘𝐵𝑙𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
23 3reeanv 3270 . . . . . . . . . . 11 (∃𝑓𝐶𝑖𝐶𝑙𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ (∃𝑓𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑖𝐶 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ ∃𝑙𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
2423rexbii 3160 . . . . . . . . . 10 (∃𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ ∃𝑘𝐵 (∃𝑓𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑖𝐶 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ ∃𝑙𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
25242rexbii 3161 . . . . . . . . 9 (∃𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ ∃𝑒𝐵𝐵𝑘𝐵 (∃𝑓𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑖𝐶 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ ∃𝑙𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
26 3reeanv 3270 . . . . . . . . 9 (∃𝑒𝐵𝐵𝑘𝐵 (∃𝑓𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑖𝐶 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ ∃𝑙𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ (∃𝑒𝐵𝑓𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝐵𝑖𝐶 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ ∃𝑘𝐵𝑙𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
2725, 26bitri 278 . . . . . . . 8 (∃𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ (∃𝑒𝐵𝑓𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝐵𝑖𝐶 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ ∃𝑘𝐵𝑙𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
2827rexbii 3160 . . . . . . 7 (∃𝑗𝐴𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ ∃𝑗𝐴 (∃𝑒𝐵𝑓𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝐵𝑖𝐶 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ ∃𝑘𝐵𝑙𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
29282rexbii 3161 . . . . . 6 (∃𝑑𝐴𝑔𝐴𝑗𝐴𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ ∃𝑑𝐴𝑔𝐴𝑗𝐴 (∃𝑒𝐵𝑓𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝐵𝑖𝐶 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ ∃𝑘𝐵𝑙𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
30 3reeanv 3270 . . . . . 6 (∃𝑑𝐴𝑔𝐴𝑗𝐴 (∃𝑒𝐵𝑓𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝐵𝑖𝐶 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ ∃𝑘𝐵𝑙𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ (∃𝑑𝐴𝑒𝐵𝑓𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑔𝐴𝐵𝑖𝐶 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ ∃𝑗𝐴𝑘𝐵𝑙𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
3129, 30bitri 278 . . . . 5 (∃𝑑𝐴𝑔𝐴𝑗𝐴𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ (∃𝑑𝐴𝑒𝐵𝑓𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑔𝐴𝐵𝑖𝐶 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ ∃𝑗𝐴𝑘𝐵𝑙𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
3222, 31bitr4i 281 . . . 4 ((𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑐 ∈ ((𝐴 × 𝐵) × 𝐶)) ↔ ∃𝑑𝐴𝑔𝐴𝑗𝐴𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
33 simprl1 1219 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑑𝐴𝑒𝐵𝑓𝐶))
34 simprr2 1223 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑗𝐴𝑘𝐵𝑙𝐶))
35 poxp3.1 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑅 Po 𝐴)
3635adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → 𝑅 Po 𝐴)
37 simpl11 1249 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙)))) → 𝑑𝐴)
3837adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → 𝑑𝐴)
39 simpr11 1258 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙)))) → 𝑔𝐴)
4039adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → 𝑔𝐴)
41 simpr21 1261 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙)))) → 𝑗𝐴)
4241adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → 𝑗𝐴)
43 potr 5450 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑅 Po 𝐴 ∧ (𝑑𝐴𝑔𝐴𝑗𝐴)) → ((𝑑𝑅𝑔𝑔𝑅𝑗) → 𝑑𝑅𝑗))
4436, 38, 40, 42, 43syl13anc 1373 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → ((𝑑𝑅𝑔𝑔𝑅𝑗) → 𝑑𝑅𝑗))
45 orc 866 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑𝑅𝑗 → (𝑑𝑅𝑗𝑑 = 𝑗))
4644, 45syl6 35 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → ((𝑑𝑅𝑔𝑔𝑅𝑗) → (𝑑𝑅𝑗𝑑 = 𝑗)))
4746expd 419 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑑𝑅𝑔 → (𝑔𝑅𝑗 → (𝑑𝑅𝑗𝑑 = 𝑗))))
48 breq1 5030 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 = 𝑔 → (𝑑𝑅𝑗𝑔𝑅𝑗))
4948, 45syl6bir 257 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 = 𝑔 → (𝑔𝑅𝑗 → (𝑑𝑅𝑗𝑑 = 𝑗)))
5049a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑑 = 𝑔 → (𝑔𝑅𝑗 → (𝑑𝑅𝑗𝑑 = 𝑗))))
51 simp3l1 1279 . . . . . . . . . . . . . . . . . . . . 21 (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) → (𝑑𝑅𝑔𝑑 = 𝑔))
5251ad2antrl 728 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑑𝑅𝑔𝑑 = 𝑔))
5347, 50, 52mpjaod 859 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑔𝑅𝑗 → (𝑑𝑅𝑗𝑑 = 𝑗)))
54 breq2 5031 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑗 → (𝑑𝑅𝑔𝑑𝑅𝑗))
55 equequ2 2037 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑗 → (𝑑 = 𝑔𝑑 = 𝑗))
5654, 55orbi12d 918 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑗 → ((𝑑𝑅𝑔𝑑 = 𝑔) ↔ (𝑑𝑅𝑗𝑑 = 𝑗)))
5752, 56syl5ibcom 248 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑔 = 𝑗 → (𝑑𝑅𝑗𝑑 = 𝑗)))
58 simp3l1 1279 . . . . . . . . . . . . . . . . . . . 20 (((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))) → (𝑔𝑅𝑗𝑔 = 𝑗))
5958ad2antll 729 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑔𝑅𝑗𝑔 = 𝑗))
6053, 57, 59mpjaod 859 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑑𝑅𝑗𝑑 = 𝑗))
61 poxp3.2 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑆 Po 𝐵)
6261adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → 𝑆 Po 𝐵)
63 simpl12 1250 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙)))) → 𝑒𝐵)
6463adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → 𝑒𝐵)
65 simpr12 1259 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙)))) → 𝐵)
6665adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → 𝐵)
67 simpr22 1262 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙)))) → 𝑘𝐵)
6867adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → 𝑘𝐵)
69 potr 5450 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑆 Po 𝐵 ∧ (𝑒𝐵𝐵𝑘𝐵)) → ((𝑒𝑆𝑆𝑘) → 𝑒𝑆𝑘))
7062, 64, 66, 68, 69syl13anc 1373 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → ((𝑒𝑆𝑆𝑘) → 𝑒𝑆𝑘))
71 orc 866 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒𝑆𝑘 → (𝑒𝑆𝑘𝑒 = 𝑘))
7270, 71syl6 35 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → ((𝑒𝑆𝑆𝑘) → (𝑒𝑆𝑘𝑒 = 𝑘)))
7372expd 419 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑒𝑆 → (𝑆𝑘 → (𝑒𝑆𝑘𝑒 = 𝑘))))
74 breq1 5030 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 = → (𝑒𝑆𝑘𝑆𝑘))
7574, 71syl6bir 257 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 = → (𝑆𝑘 → (𝑒𝑆𝑘𝑒 = 𝑘)))
7675a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑒 = → (𝑆𝑘 → (𝑒𝑆𝑘𝑒 = 𝑘))))
77 simp3l2 1280 . . . . . . . . . . . . . . . . . . . . 21 (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) → (𝑒𝑆𝑒 = ))
7877ad2antrl 728 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑒𝑆𝑒 = ))
7973, 76, 78mpjaod 859 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑆𝑘 → (𝑒𝑆𝑘𝑒 = 𝑘)))
80 breq2 5031 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑘 → (𝑒𝑆𝑒𝑆𝑘))
81 equequ2 2037 . . . . . . . . . . . . . . . . . . . . 21 ( = 𝑘 → (𝑒 = 𝑒 = 𝑘))
8280, 81orbi12d 918 . . . . . . . . . . . . . . . . . . . 20 ( = 𝑘 → ((𝑒𝑆𝑒 = ) ↔ (𝑒𝑆𝑘𝑒 = 𝑘)))
8378, 82syl5ibcom 248 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → ( = 𝑘 → (𝑒𝑆𝑘𝑒 = 𝑘)))
84 simp3l2 1280 . . . . . . . . . . . . . . . . . . . 20 (((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))) → (𝑆𝑘 = 𝑘))
8584ad2antll 729 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑆𝑘 = 𝑘))
8679, 83, 85mpjaod 859 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑒𝑆𝑘𝑒 = 𝑘))
87 poxp3.3 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑇 Po 𝐶)
8887adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → 𝑇 Po 𝐶)
89 simpl13 1251 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙)))) → 𝑓𝐶)
9089adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → 𝑓𝐶)
91 simpr13 1260 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙)))) → 𝑖𝐶)
9291adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → 𝑖𝐶)
93 simpr23 1263 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙)))) → 𝑙𝐶)
9493adantl 485 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → 𝑙𝐶)
95 potr 5450 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑇 Po 𝐶 ∧ (𝑓𝐶𝑖𝐶𝑙𝐶)) → ((𝑓𝑇𝑖𝑖𝑇𝑙) → 𝑓𝑇𝑙))
9688, 90, 92, 94, 95syl13anc 1373 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → ((𝑓𝑇𝑖𝑖𝑇𝑙) → 𝑓𝑇𝑙))
97 orc 866 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓𝑇𝑙 → (𝑓𝑇𝑙𝑓 = 𝑙))
9896, 97syl6 35 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → ((𝑓𝑇𝑖𝑖𝑇𝑙) → (𝑓𝑇𝑙𝑓 = 𝑙)))
9998expd 419 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑓𝑇𝑖 → (𝑖𝑇𝑙 → (𝑓𝑇𝑙𝑓 = 𝑙))))
100 breq1 5030 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 = 𝑖 → (𝑓𝑇𝑙𝑖𝑇𝑙))
101100, 97syl6bir 257 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 = 𝑖 → (𝑖𝑇𝑙 → (𝑓𝑇𝑙𝑓 = 𝑙)))
102101a1i 11 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑓 = 𝑖 → (𝑖𝑇𝑙 → (𝑓𝑇𝑙𝑓 = 𝑙))))
103 simp3l3 1281 . . . . . . . . . . . . . . . . . . . . 21 (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) → (𝑓𝑇𝑖𝑓 = 𝑖))
104103ad2antrl 728 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑓𝑇𝑖𝑓 = 𝑖))
10599, 102, 104mpjaod 859 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑖𝑇𝑙 → (𝑓𝑇𝑙𝑓 = 𝑙)))
106 breq2 5031 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑙 → (𝑓𝑇𝑖𝑓𝑇𝑙))
107 equequ2 2037 . . . . . . . . . . . . . . . . . . . . 21 (𝑖 = 𝑙 → (𝑓 = 𝑖𝑓 = 𝑙))
108106, 107orbi12d 918 . . . . . . . . . . . . . . . . . . . 20 (𝑖 = 𝑙 → ((𝑓𝑇𝑖𝑓 = 𝑖) ↔ (𝑓𝑇𝑙𝑓 = 𝑙)))
109104, 108syl5ibcom 248 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑖 = 𝑙 → (𝑓𝑇𝑙𝑓 = 𝑙)))
110 simp3l3 1281 . . . . . . . . . . . . . . . . . . . 20 (((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))) → (𝑖𝑇𝑙𝑖 = 𝑙))
111110ad2antll 729 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑖𝑇𝑙𝑖 = 𝑙))
112105, 109, 111mpjaod 859 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑓𝑇𝑙𝑓 = 𝑙))
11360, 86, 1123jca 1129 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → ((𝑑𝑅𝑗𝑑 = 𝑗) ∧ (𝑒𝑆𝑘𝑒 = 𝑘) ∧ (𝑓𝑇𝑙𝑓 = 𝑙)))
114 simpr3r 1236 . . . . . . . . . . . . . . . . . . . 20 ((((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙)))) → (𝑔𝑗𝑘𝑖𝑙))
115114adantl 485 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑔𝑗𝑘𝑖𝑙))
116 df-ne 2935 . . . . . . . . . . . . . . . . . . . . 21 (𝑔𝑗 ↔ ¬ 𝑔 = 𝑗)
117 df-ne 2935 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 ↔ ¬ = 𝑘)
118 df-ne 2935 . . . . . . . . . . . . . . . . . . . . 21 (𝑖𝑙 ↔ ¬ 𝑖 = 𝑙)
119116, 117, 1183orbi123i 1157 . . . . . . . . . . . . . . . . . . . 20 ((𝑔𝑗𝑘𝑖𝑙) ↔ (¬ 𝑔 = 𝑗 ∨ ¬ = 𝑘 ∨ ¬ 𝑖 = 𝑙))
120 3ianor 1108 . . . . . . . . . . . . . . . . . . . 20 (¬ (𝑔 = 𝑗 = 𝑘𝑖 = 𝑙) ↔ (¬ 𝑔 = 𝑗 ∨ ¬ = 𝑘 ∨ ¬ 𝑖 = 𝑙))
121119, 120bitr4i 281 . . . . . . . . . . . . . . . . . . 19 ((𝑔𝑗𝑘𝑖𝑙) ↔ ¬ (𝑔 = 𝑗 = 𝑘𝑖 = 𝑙))
122115, 121sylib 221 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → ¬ (𝑔 = 𝑗 = 𝑘𝑖 = 𝑙))
123 df-ne 2935 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑𝑗 ↔ ¬ 𝑑 = 𝑗)
124 df-ne 2935 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒𝑘 ↔ ¬ 𝑒 = 𝑘)
125 df-ne 2935 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓𝑙 ↔ ¬ 𝑓 = 𝑙)
126123, 124, 1253orbi123i 1157 . . . . . . . . . . . . . . . . . . . . 21 ((𝑑𝑗𝑒𝑘𝑓𝑙) ↔ (¬ 𝑑 = 𝑗 ∨ ¬ 𝑒 = 𝑘 ∨ ¬ 𝑓 = 𝑙))
127 3ianor 1108 . . . . . . . . . . . . . . . . . . . . 21 (¬ (𝑑 = 𝑗𝑒 = 𝑘𝑓 = 𝑙) ↔ (¬ 𝑑 = 𝑗 ∨ ¬ 𝑒 = 𝑘 ∨ ¬ 𝑓 = 𝑙))
128126, 127bitr4i 281 . . . . . . . . . . . . . . . . . . . 20 ((𝑑𝑗𝑒𝑘𝑓𝑙) ↔ ¬ (𝑑 = 𝑗𝑒 = 𝑘𝑓 = 𝑙))
129128con2bii 361 . . . . . . . . . . . . . . . . . . 19 ((𝑑 = 𝑗𝑒 = 𝑘𝑓 = 𝑙) ↔ ¬ (𝑑𝑗𝑒𝑘𝑓𝑙))
130 breq1 5030 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = 𝑗 → (𝑑𝑅𝑔𝑗𝑅𝑔))
131 equequ1 2036 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑑 = 𝑗 → (𝑑 = 𝑔𝑗 = 𝑔))
132 equcom 2029 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑗 = 𝑔𝑔 = 𝑗)
133131, 132bitrdi 290 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = 𝑗 → (𝑑 = 𝑔𝑔 = 𝑗))
134130, 133orbi12d 918 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = 𝑗 → ((𝑑𝑅𝑔𝑑 = 𝑔) ↔ (𝑗𝑅𝑔𝑔 = 𝑗)))
13552, 134syl5ibcom 248 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑑 = 𝑗 → (𝑗𝑅𝑔𝑔 = 𝑗)))
136135imp 410 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) ∧ 𝑑 = 𝑗) → (𝑗𝑅𝑔𝑔 = 𝑗))
13759adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) ∧ 𝑑 = 𝑗) → (𝑔𝑅𝑗𝑔 = 𝑗))
138 ordir 1006 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑗𝑅𝑔𝑔𝑅𝑗) ∨ 𝑔 = 𝑗) ↔ ((𝑗𝑅𝑔𝑔 = 𝑗) ∧ (𝑔𝑅𝑗𝑔 = 𝑗)))
139136, 137, 138sylanbrc 586 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) ∧ 𝑑 = 𝑗) → ((𝑗𝑅𝑔𝑔𝑅𝑗) ∨ 𝑔 = 𝑗))
140 po2nr 5451 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑅 Po 𝐴 ∧ (𝑗𝐴𝑔𝐴)) → ¬ (𝑗𝑅𝑔𝑔𝑅𝑗))
14136, 42, 40, 140syl12anc 836 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → ¬ (𝑗𝑅𝑔𝑔𝑅𝑗))
142141adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) ∧ 𝑑 = 𝑗) → ¬ (𝑗𝑅𝑔𝑔𝑅𝑗))
143139, 142orcnd 878 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) ∧ 𝑑 = 𝑗) → 𝑔 = 𝑗)
144143ex 416 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑑 = 𝑗𝑔 = 𝑗))
145 breq1 5030 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑒 = 𝑘 → (𝑒𝑆𝑘𝑆))
146 equequ1 2036 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑒 = 𝑘 → (𝑒 = 𝑘 = ))
147 equcom 2029 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑘 = = 𝑘)
148146, 147bitrdi 290 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑒 = 𝑘 → (𝑒 = = 𝑘))
149145, 148orbi12d 918 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑒 = 𝑘 → ((𝑒𝑆𝑒 = ) ↔ (𝑘𝑆 = 𝑘)))
15078, 149syl5ibcom 248 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑒 = 𝑘 → (𝑘𝑆 = 𝑘)))
151150imp 410 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) ∧ 𝑒 = 𝑘) → (𝑘𝑆 = 𝑘))
15285adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) ∧ 𝑒 = 𝑘) → (𝑆𝑘 = 𝑘))
153 ordir 1006 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑘𝑆𝑆𝑘) ∨ = 𝑘) ↔ ((𝑘𝑆 = 𝑘) ∧ (𝑆𝑘 = 𝑘)))
154151, 152, 153sylanbrc 586 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) ∧ 𝑒 = 𝑘) → ((𝑘𝑆𝑆𝑘) ∨ = 𝑘))
155 po2nr 5451 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑆 Po 𝐵 ∧ (𝑘𝐵𝐵)) → ¬ (𝑘𝑆𝑆𝑘))
15662, 68, 66, 155syl12anc 836 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → ¬ (𝑘𝑆𝑆𝑘))
157156adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) ∧ 𝑒 = 𝑘) → ¬ (𝑘𝑆𝑆𝑘))
158154, 157orcnd 878 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) ∧ 𝑒 = 𝑘) → = 𝑘)
159158ex 416 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑒 = 𝑘 = 𝑘))
160 breq1 5030 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = 𝑙 → (𝑓𝑇𝑖𝑙𝑇𝑖))
161 equequ1 2036 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑓 = 𝑙 → (𝑓 = 𝑖𝑙 = 𝑖))
162160, 161orbi12d 918 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑓 = 𝑙 → ((𝑓𝑇𝑖𝑓 = 𝑖) ↔ (𝑙𝑇𝑖𝑙 = 𝑖)))
163104, 162syl5ibcom 248 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑓 = 𝑙 → (𝑙𝑇𝑖𝑙 = 𝑖)))
164163imp 410 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) ∧ 𝑓 = 𝑙) → (𝑙𝑇𝑖𝑙 = 𝑖))
165 equcom 2029 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑙 = 𝑖𝑖 = 𝑙)
166165orbi2i 912 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑙𝑇𝑖𝑙 = 𝑖) ↔ (𝑙𝑇𝑖𝑖 = 𝑙))
167164, 166sylib 221 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) ∧ 𝑓 = 𝑙) → (𝑙𝑇𝑖𝑖 = 𝑙))
168111adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) ∧ 𝑓 = 𝑙) → (𝑖𝑇𝑙𝑖 = 𝑙))
169 ordir 1006 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑙𝑇𝑖𝑖𝑇𝑙) ∨ 𝑖 = 𝑙) ↔ ((𝑙𝑇𝑖𝑖 = 𝑙) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)))
170167, 168, 169sylanbrc 586 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) ∧ 𝑓 = 𝑙) → ((𝑙𝑇𝑖𝑖𝑇𝑙) ∨ 𝑖 = 𝑙))
171 po2nr 5451 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑇 Po 𝐶 ∧ (𝑙𝐶𝑖𝐶)) → ¬ (𝑙𝑇𝑖𝑖𝑇𝑙))
17288, 94, 92, 171syl12anc 836 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → ¬ (𝑙𝑇𝑖𝑖𝑇𝑙))
173172adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) ∧ 𝑓 = 𝑙) → ¬ (𝑙𝑇𝑖𝑖𝑇𝑙))
174170, 173orcnd 878 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) ∧ 𝑓 = 𝑙) → 𝑖 = 𝑙)
175174ex 416 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑓 = 𝑙𝑖 = 𝑙))
176144, 159, 1753anim123d 1444 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → ((𝑑 = 𝑗𝑒 = 𝑘𝑓 = 𝑙) → (𝑔 = 𝑗 = 𝑘𝑖 = 𝑙)))
177129, 176syl5bir 246 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (¬ (𝑑𝑗𝑒𝑘𝑓𝑙) → (𝑔 = 𝑗 = 𝑘𝑖 = 𝑙)))
178122, 177mt3d 150 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (𝑑𝑗𝑒𝑘𝑓𝑙))
179113, 178jca 515 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → (((𝑑𝑅𝑗𝑑 = 𝑗) ∧ (𝑒𝑆𝑘𝑒 = 𝑘) ∧ (𝑓𝑇𝑙𝑓 = 𝑙)) ∧ (𝑑𝑗𝑒𝑘𝑓𝑙)))
18033, 34, 1793jca 1129 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))) → ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑑𝑅𝑗𝑑 = 𝑗) ∧ (𝑒𝑆𝑘𝑒 = 𝑘) ∧ (𝑓𝑇𝑙𝑓 = 𝑙)) ∧ (𝑑𝑗𝑒𝑘𝑓𝑙))))
181180ex 416 . . . . . . . . . . . . . 14 (𝜑 → ((((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙)))) → ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑑𝑅𝑗𝑑 = 𝑗) ∧ (𝑒𝑆𝑘𝑒 = 𝑘) ∧ (𝑓𝑇𝑙𝑓 = 𝑙)) ∧ (𝑑𝑗𝑒𝑘𝑓𝑙)))))
182 breq12 5032 . . . . . . . . . . . . . . . . . 18 ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩) → (𝑎𝑈𝑏 ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓𝑈⟨⟨𝑔, ⟩, 𝑖⟩))
1831823adant3 1133 . . . . . . . . . . . . . . . . 17 ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑎𝑈𝑏 ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓𝑈⟨⟨𝑔, ⟩, 𝑖⟩))
18411xpord3lem 33398 . . . . . . . . . . . . . . . . 17 (⟨⟨𝑑, 𝑒⟩, 𝑓𝑈⟨⟨𝑔, ⟩, 𝑖⟩ ↔ ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))))
185183, 184bitrdi 290 . . . . . . . . . . . . . . . 16 ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑎𝑈𝑏 ↔ ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖)))))
186 breq12 5032 . . . . . . . . . . . . . . . . . 18 ((𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑏𝑈𝑐 ↔ ⟨⟨𝑔, ⟩, 𝑖𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
1871863adant1 1131 . . . . . . . . . . . . . . . . 17 ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑏𝑈𝑐 ↔ ⟨⟨𝑔, ⟩, 𝑖𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
18811xpord3lem 33398 . . . . . . . . . . . . . . . . 17 (⟨⟨𝑔, ⟩, 𝑖𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩ ↔ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))
189187, 188bitrdi 290 . . . . . . . . . . . . . . . 16 ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑏𝑈𝑐 ↔ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙)))))
190185, 189anbi12d 634 . . . . . . . . . . . . . . 15 ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏𝑏𝑈𝑐) ↔ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙))))))
191 breq12 5032 . . . . . . . . . . . . . . . . 17 ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑎𝑈𝑐 ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
1921913adant2 1132 . . . . . . . . . . . . . . . 16 ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑎𝑈𝑐 ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
19311xpord3lem 33398 . . . . . . . . . . . . . . . 16 (⟨⟨𝑑, 𝑒⟩, 𝑓𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩ ↔ ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑑𝑅𝑗𝑑 = 𝑗) ∧ (𝑒𝑆𝑘𝑒 = 𝑘) ∧ (𝑓𝑇𝑙𝑓 = 𝑙)) ∧ (𝑑𝑗𝑒𝑘𝑓𝑙))))
194192, 193bitrdi 290 . . . . . . . . . . . . . . 15 ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑎𝑈𝑐 ↔ ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑑𝑅𝑗𝑑 = 𝑗) ∧ (𝑒𝑆𝑘𝑒 = 𝑘) ∧ (𝑓𝑇𝑙𝑓 = 𝑙)) ∧ (𝑑𝑗𝑒𝑘𝑓𝑙)))))
195190, 194imbi12d 348 . . . . . . . . . . . . . 14 ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (((𝑎𝑈𝑏𝑏𝑈𝑐) → 𝑎𝑈𝑐) ↔ ((((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑔𝐴𝐵𝑖𝐶) ∧ (((𝑑𝑅𝑔𝑑 = 𝑔) ∧ (𝑒𝑆𝑒 = ) ∧ (𝑓𝑇𝑖𝑓 = 𝑖)) ∧ (𝑑𝑔𝑒𝑓𝑖))) ∧ ((𝑔𝐴𝐵𝑖𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑔𝑅𝑗𝑔 = 𝑗) ∧ (𝑆𝑘 = 𝑘) ∧ (𝑖𝑇𝑙𝑖 = 𝑙)) ∧ (𝑔𝑗𝑘𝑖𝑙)))) → ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑗𝐴𝑘𝐵𝑙𝐶) ∧ (((𝑑𝑅𝑗𝑑 = 𝑗) ∧ (𝑒𝑆𝑘𝑒 = 𝑘) ∧ (𝑓𝑇𝑙𝑓 = 𝑙)) ∧ (𝑑𝑗𝑒𝑘𝑓𝑙))))))
196181, 195syl5ibrcom 250 . . . . . . . . . . . . 13 (𝜑 → ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
197196rexlimdvw 3199 . . . . . . . . . . . 12 (𝜑 → (∃𝑙𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
198197a1d 25 . . . . . . . . . . 11 (𝜑 → ((𝑓𝐶𝑖𝐶) → (∃𝑙𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏𝑏𝑈𝑐) → 𝑎𝑈𝑐))))
199198rexlimdvv 3202 . . . . . . . . . 10 (𝜑 → (∃𝑓𝐶𝑖𝐶𝑙𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
200199rexlimdvw 3199 . . . . . . . . 9 (𝜑 → (∃𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
201200a1d 25 . . . . . . . 8 (𝜑 → ((𝑒𝐵𝐵) → (∃𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏𝑏𝑈𝑐) → 𝑎𝑈𝑐))))
202201rexlimdvv 3202 . . . . . . 7 (𝜑 → (∃𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
203202rexlimdvw 3199 . . . . . 6 (𝜑 → (∃𝑗𝐴𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
204203a1d 25 . . . . 5 (𝜑 → ((𝑑𝐴𝑔𝐴) → (∃𝑗𝐴𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏𝑏𝑈𝑐) → 𝑎𝑈𝑐))))
205204rexlimdvv 3202 . . . 4 (𝜑 → (∃𝑑𝐴𝑔𝐴𝑗𝐴𝑒𝐵𝐵𝑘𝐵𝑓𝐶𝑖𝐶𝑙𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
20632, 205syl5bi 245 . . 3 (𝜑 → ((𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑐 ∈ ((𝐴 × 𝐵) × 𝐶)) → ((𝑎𝑈𝑏𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
207206imp 410 . 2 ((𝜑 ∧ (𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑐 ∈ ((𝐴 × 𝐵) × 𝐶))) → ((𝑎𝑈𝑏𝑏𝑈𝑐) → 𝑎𝑈𝑐))
20819, 207ispod 5446 1 (𝜑𝑈 Po ((𝐴 × 𝐵) × 𝐶))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 846  w3o 1087  w3a 1088   = wceq 1542  wcel 2113  wne 2934  wrex 3054  cop 4519   class class class wbr 5027  {copab 5089   Po wpo 5436   × cxp 5517  cfv 6333  1st c1st 7705  2nd c2nd 7706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2161  ax-12 2178  ax-ext 2710  ax-sep 5164  ax-nul 5171  ax-pr 5293  ax-un 7473
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3399  df-sbc 3680  df-csb 3789  df-dif 3844  df-un 3846  df-in 3848  df-ss 3858  df-nul 4210  df-if 4412  df-sn 4514  df-pr 4516  df-op 4520  df-uni 4794  df-iun 4880  df-br 5028  df-opab 5090  df-mpt 5108  df-id 5425  df-po 5438  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-iota 6291  df-fun 6335  df-fv 6341  df-1st 7707  df-2nd 7708
This theorem is referenced by:  xpord3ind  33403  no3indslem  33744
  Copyright terms: Public domain W3C validator