poxp3 - Mathbox for Scott Fenton

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

Theorem poxp3 33796

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

**Hypotheses**
Ref	Expression
xpord3.1	⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1^st ‘(1^st ‘𝑥))𝑅(1^st ‘(1^st ‘𝑦)) ∨ (1^st ‘(1^st ‘𝑥)) = (1^st ‘(1^st ‘𝑦))) ∧ ((2^nd ‘(1^st ‘𝑥))𝑆(2^nd ‘(1^st ‘𝑦)) ∨ (2^nd ‘(1^st ‘𝑥)) = (2^nd ‘(1^st ‘𝑦))) ∧ ((2^nd ‘𝑥)𝑇(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}
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.

Step	Hyp	Ref	Expression
1		elxpxp 33683	. . . 4 ⊢ (𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩)
2		neirr 2952	. . . . . . . . . . 11 ⊢ ¬ 𝑑 ≠ 𝑑
3		neirr 2952	. . . . . . . . . . 11 ⊢ ¬ 𝑒 ≠ 𝑒
4		neirr 2952	. . . . . . . . . . 11 ⊢ ¬ 𝑓 ≠ 𝑓
5	2, 3, 4	3pm3.2ni 33656	. . . . . . . . . 10 ⊢ ¬ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓)
6	5	intnan 487	. . . . . . . . 9 ⊢ ¬ (((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓))
7		simp3 1137	. . . . . . . . 9 ⊢ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓))) → (((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓)))
8	6, 7	mto 196	. . . . . . . 8 ⊢ ¬ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓)))
9		breq12 5079	. . . . . . . . . 10 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩) → (𝑎𝑈𝑎 ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩𝑈⟨⟨𝑑, 𝑒⟩, 𝑓⟩))
10	9	anidms 567	. . . . . . . . 9 ⊢ (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑎𝑈𝑎 ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩𝑈⟨⟨𝑑, 𝑒⟩, 𝑓⟩))
11		xpord3.1	. . . . . . . . . 10 ⊢ 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1^st ‘(1^st ‘𝑥))𝑅(1^st ‘(1^st ‘𝑦)) ∨ (1^st ‘(1^st ‘𝑥)) = (1^st ‘(1^st ‘𝑦))) ∧ ((2^nd ‘(1^st ‘𝑥))𝑆(2^nd ‘(1^st ‘𝑦)) ∨ (2^nd ‘(1^st ‘𝑥)) = (2^nd ‘(1^st ‘𝑦))) ∧ ((2^nd ‘𝑥)𝑇(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦))) ∧ 𝑥 ≠ 𝑦))}
12	11	xpord3lem 33795	. . . . . . . . 9 ⊢ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩𝑈⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓))))
13	10, 12	bitrdi 287	. . . . . . . 8 ⊢ (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑎𝑈𝑎 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓)))))
14	8, 13	mtbiri 327	. . . . . . 7 ⊢ (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ¬ 𝑎𝑈𝑎)
15	14	rexlimivw 3211	. . . . . 6 ⊢ (∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ¬ 𝑎𝑈𝑎)
16	15	a1i 11	. . . . 5 ⊢ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵) → (∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ¬ 𝑎𝑈𝑎))
17	16	rexlimivv 3221	. . . 4 ⊢ (∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ¬ 𝑎𝑈𝑎)
18	1, 17	sylbi 216	. . 3 ⊢ (𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) → ¬ 𝑎𝑈𝑎)
19	18	adantl 482	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ ((𝐴 × 𝐵) × 𝐶)) → ¬ 𝑎𝑈𝑎)
20		elxpxp 33683	. . . . . 6 ⊢ (𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩)
21		elxpxp 33683	. . . . . 6 ⊢ (𝑐 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑗 ∈ 𝐴 ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩)
22	1, 20, 21	3anbi123i 1154	. . . . 5 ⊢ ((𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑐 ∈ ((𝐴 × 𝐵) × 𝐶)) ↔ (∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑗 ∈ 𝐴 ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
23		3reeanv 3295	. . . . . . . . . . 11 ⊢ (∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ (∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
24	23	rexbii 3181	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ ∃𝑘 ∈ 𝐵 (∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
25	24	2rexbii 3182	. . . . . . . . 9 ⊢ (∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 (∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
26		3reeanv 3295	. . . . . . . . 9 ⊢ (∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 (∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ (∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
27	25, 26	bitri 274	. . . . . . . 8 ⊢ (∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ (∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
28	27	rexbii 3181	. . . . . . 7 ⊢ (∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ ∃𝑗 ∈ 𝐴 (∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
29	28	2rexbii 3182	. . . . . 6 ⊢ (∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ ∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 (∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
30		3reeanv 3295	. . . . . 6 ⊢ (∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 (∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ (∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑗 ∈ 𝐴 ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
31	29, 30	bitri 274	. . . . 5 ⊢ (∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ (∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑗 ∈ 𝐴 ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
32	22, 31	bitr4i 277	. . . 4 ⊢ ((𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑐 ∈ ((𝐴 × 𝐵) × 𝐶)) ↔ ∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
33		simprl1 1217	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶))
34		simprr2 1221	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶))
35		poxp3.1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑅 Po 𝐴)
36	35	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑅 Po 𝐴)
37		simpl11 1247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑑 ∈ 𝐴)
38	37	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑑 ∈ 𝐴)
39		simpr11 1256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑔 ∈ 𝐴)
40	39	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑔 ∈ 𝐴)
41		simpr21 1259	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑗 ∈ 𝐴)
42	41	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑗 ∈ 𝐴)
43		potr 5516	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 Po 𝐴 ∧ (𝑑 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴)) → ((𝑑𝑅𝑔 ∧ 𝑔𝑅𝑗) → 𝑑𝑅𝑗))
44	36, 38, 40, 42, 43	syl13anc 1371	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑑𝑅𝑔 ∧ 𝑔𝑅𝑗) → 𝑑𝑅𝑗))
45		orc 864	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑𝑅𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗))
46	44, 45	syl6 35	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑑𝑅𝑔 ∧ 𝑔𝑅𝑗) → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗)))
47	46	expd 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑𝑅𝑔 → (𝑔𝑅𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗))))
48		breq1 5077	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = 𝑔 → (𝑑𝑅𝑗 ↔ 𝑔𝑅𝑗))
49	48, 45	syl6bir 253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑔 → (𝑔𝑅𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗)))
50	49	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑 = 𝑔 → (𝑔𝑅𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗))))
51		simp3l1 1277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑑𝑅𝑔 ∨ 𝑑 = 𝑔))
52	51	ad2antrl 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑𝑅𝑔 ∨ 𝑑 = 𝑔))
53	47, 50, 52	mpjaod 857	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑔𝑅𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗)))
54		breq2 5078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑗 → (𝑑𝑅𝑔 ↔ 𝑑𝑅𝑗))
55		equequ2 2029	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑗 → (𝑑 = 𝑔 ↔ 𝑑 = 𝑗))
56	54, 55	orbi12d 916	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑗 → ((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ↔ (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗)))
57	52, 56	syl5ibcom 244	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑔 = 𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗)))
58		simp3l1 1277	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))) → (𝑔𝑅𝑗 ∨ 𝑔 = 𝑗))
59	58	ad2antll 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑔𝑅𝑗 ∨ 𝑔 = 𝑗))
60	53, 57, 59	mpjaod 857	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗))
61		poxp3.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑆 Po 𝐵)
62	61	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑆 Po 𝐵)
63		simpl12 1248	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑒 ∈ 𝐵)
64	63	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑒 ∈ 𝐵)
65		simpr12 1257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → ℎ ∈ 𝐵)
66	65	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ℎ ∈ 𝐵)
67		simpr22 1260	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑘 ∈ 𝐵)
68	67	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑘 ∈ 𝐵)
69		potr 5516	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 Po 𝐵 ∧ (𝑒 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ∧ 𝑘 ∈ 𝐵)) → ((𝑒𝑆ℎ ∧ ℎ𝑆𝑘) → 𝑒𝑆𝑘))
70	62, 64, 66, 68, 69	syl13anc 1371	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑒𝑆ℎ ∧ ℎ𝑆𝑘) → 𝑒𝑆𝑘))
71		orc 864	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒𝑆𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘))
72	70, 71	syl6 35	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑒𝑆ℎ ∧ ℎ𝑆𝑘) → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘)))
73	72	expd 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒𝑆ℎ → (ℎ𝑆𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘))))
74		breq1 5077	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒 = ℎ → (𝑒𝑆𝑘 ↔ ℎ𝑆𝑘))
75	74, 71	syl6bir 253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = ℎ → (ℎ𝑆𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘)))
76	75	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒 = ℎ → (ℎ𝑆𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘))))
77		simp3l2 1278	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑒𝑆ℎ ∨ 𝑒 = ℎ))
78	77	ad2antrl 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒𝑆ℎ ∨ 𝑒 = ℎ))
79	73, 76, 78	mpjaod 857	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (ℎ𝑆𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘)))
80		breq2 5078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ = 𝑘 → (𝑒𝑆ℎ ↔ 𝑒𝑆𝑘))
81		equequ2 2029	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ = 𝑘 → (𝑒 = ℎ ↔ 𝑒 = 𝑘))
82	80, 81	orbi12d 916	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = 𝑘 → ((𝑒𝑆ℎ ∨ 𝑒 = ℎ) ↔ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘)))
83	78, 82	syl5ibcom 244	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (ℎ = 𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘)))
84		simp3l2 1278	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))) → (ℎ𝑆𝑘 ∨ ℎ = 𝑘))
85	84	ad2antll 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (ℎ𝑆𝑘 ∨ ℎ = 𝑘))
86	79, 83, 85	mpjaod 857	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘))
87		poxp3.3	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑇 Po 𝐶)
88	87	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑇 Po 𝐶)
89		simpl13 1249	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑓 ∈ 𝐶)
90	89	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑓 ∈ 𝐶)
91		simpr13 1258	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑖 ∈ 𝐶)
92	91	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑖 ∈ 𝐶)
93		simpr23 1261	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑙 ∈ 𝐶)
94	93	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑙 ∈ 𝐶)
95		potr 5516	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑇 Po 𝐶 ∧ (𝑓 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶 ∧ 𝑙 ∈ 𝐶)) → ((𝑓𝑇𝑖 ∧ 𝑖𝑇𝑙) → 𝑓𝑇𝑙))
96	88, 90, 92, 94, 95	syl13anc 1371	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑓𝑇𝑖 ∧ 𝑖𝑇𝑙) → 𝑓𝑇𝑙))
97		orc 864	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓𝑇𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙))
98	96, 97	syl6 35	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑓𝑇𝑖 ∧ 𝑖𝑇𝑙) → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)))
99	98	expd 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓𝑇𝑖 → (𝑖𝑇𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙))))
100		breq1 5077	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑖 → (𝑓𝑇𝑙 ↔ 𝑖𝑇𝑙))
101	100, 97	syl6bir 253	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑖 → (𝑖𝑇𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)))
102	101	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓 = 𝑖 → (𝑖𝑇𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙))))
103		simp3l3 1279	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖))
104	103	ad2antrl 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖))
105	99, 102, 104	mpjaod 857	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑖𝑇𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)))
106		breq2 5078	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑙 → (𝑓𝑇𝑖 ↔ 𝑓𝑇𝑙))
107		equequ2 2029	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑙 → (𝑓 = 𝑖 ↔ 𝑓 = 𝑙))
108	106, 107	orbi12d 916	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑙 → ((𝑓𝑇𝑖 ∨ 𝑓 = 𝑖) ↔ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)))
109	104, 108	syl5ibcom 244	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑖 = 𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)))
110		simp3l3 1279	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))) → (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙))
111	110	ad2antll 726	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙))
112	105, 109, 111	mpjaod 857	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙))
113	60, 86, 112	3jca 1127	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)))
114		simpr3r 1234	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))
115	114	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))
116		df-ne 2944	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 ≠ 𝑗 ↔ ¬ 𝑔 = 𝑗)
117		df-ne 2944	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ ≠ 𝑘 ↔ ¬ ℎ = 𝑘)
118		df-ne 2944	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ≠ 𝑙 ↔ ¬ 𝑖 = 𝑙)
119	116, 117, 118	3orbi123i 1155	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙) ↔ (¬ 𝑔 = 𝑗 ∨ ¬ ℎ = 𝑘 ∨ ¬ 𝑖 = 𝑙))
120		3ianor 1106	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝑔 = 𝑗 ∧ ℎ = 𝑘 ∧ 𝑖 = 𝑙) ↔ (¬ 𝑔 = 𝑗 ∨ ¬ ℎ = 𝑘 ∨ ¬ 𝑖 = 𝑙))
121	119, 120	bitr4i 277	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙) ↔ ¬ (𝑔 = 𝑗 ∧ ℎ = 𝑘 ∧ 𝑖 = 𝑙))
122	115, 121	sylib 217	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ¬ (𝑔 = 𝑗 ∧ ℎ = 𝑘 ∧ 𝑖 = 𝑙))
123		df-ne 2944	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 ≠ 𝑗 ↔ ¬ 𝑑 = 𝑗)
124		df-ne 2944	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒 ≠ 𝑘 ↔ ¬ 𝑒 = 𝑘)
125		df-ne 2944	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 ≠ 𝑙 ↔ ¬ 𝑓 = 𝑙)
126	123, 124, 125	3orbi123i 1155	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙) ↔ (¬ 𝑑 = 𝑗 ∨ ¬ 𝑒 = 𝑘 ∨ ¬ 𝑓 = 𝑙))
127		3ianor 1106	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝑑 = 𝑗 ∧ 𝑒 = 𝑘 ∧ 𝑓 = 𝑙) ↔ (¬ 𝑑 = 𝑗 ∨ ¬ 𝑒 = 𝑘 ∨ ¬ 𝑓 = 𝑙))
128	126, 127	bitr4i 277	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙) ↔ ¬ (𝑑 = 𝑗 ∧ 𝑒 = 𝑘 ∧ 𝑓 = 𝑙))
129	128	con2bii 358	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑑 = 𝑗 ∧ 𝑒 = 𝑘 ∧ 𝑓 = 𝑙) ↔ ¬ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙))
130		breq1 5077	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = 𝑗 → (𝑑𝑅𝑔 ↔ 𝑗𝑅𝑔))
131		equequ1 2028	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 = 𝑗 → (𝑑 = 𝑔 ↔ 𝑗 = 𝑔))
132		equcom 2021	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 = 𝑔 ↔ 𝑔 = 𝑗)
133	131, 132	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = 𝑗 → (𝑑 = 𝑔 ↔ 𝑔 = 𝑗))
134	130, 133	orbi12d 916	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = 𝑗 → ((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ↔ (𝑗𝑅𝑔 ∨ 𝑔 = 𝑗)))
135	52, 134	syl5ibcom 244	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑 = 𝑗 → (𝑗𝑅𝑔 ∨ 𝑔 = 𝑗)))
136	135	imp 407	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑑 = 𝑗) → (𝑗𝑅𝑔 ∨ 𝑔 = 𝑗))
137	59	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑑 = 𝑗) → (𝑔𝑅𝑗 ∨ 𝑔 = 𝑗))
138		ordir 1004	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑗𝑅𝑔 ∧ 𝑔𝑅𝑗) ∨ 𝑔 = 𝑗) ↔ ((𝑗𝑅𝑔 ∨ 𝑔 = 𝑗) ∧ (𝑔𝑅𝑗 ∨ 𝑔 = 𝑗)))
139	136, 137, 138	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑑 = 𝑗) → ((𝑗𝑅𝑔 ∧ 𝑔𝑅𝑗) ∨ 𝑔 = 𝑗))
140		po2nr 5517	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Po 𝐴 ∧ (𝑗 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → ¬ (𝑗𝑅𝑔 ∧ 𝑔𝑅𝑗))
141	36, 42, 40, 140	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ¬ (𝑗𝑅𝑔 ∧ 𝑔𝑅𝑗))
142	141	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑑 = 𝑗) → ¬ (𝑗𝑅𝑔 ∧ 𝑔𝑅𝑗))
143	139, 142	orcnd 876	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑑 = 𝑗) → 𝑔 = 𝑗)
144	143	ex 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑 = 𝑗 → 𝑔 = 𝑗))
145		breq1 5077	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑒 = 𝑘 → (𝑒𝑆ℎ ↔ 𝑘𝑆ℎ))
146		equequ1 2028	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑒 = 𝑘 → (𝑒 = ℎ ↔ 𝑘 = ℎ))
147		equcom 2021	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = ℎ ↔ ℎ = 𝑘)
148	146, 147	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑒 = 𝑘 → (𝑒 = ℎ ↔ ℎ = 𝑘))
149	145, 148	orbi12d 916	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑒 = 𝑘 → ((𝑒𝑆ℎ ∨ 𝑒 = ℎ) ↔ (𝑘𝑆ℎ ∨ ℎ = 𝑘)))
150	78, 149	syl5ibcom 244	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒 = 𝑘 → (𝑘𝑆ℎ ∨ ℎ = 𝑘)))
151	150	imp 407	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑒 = 𝑘) → (𝑘𝑆ℎ ∨ ℎ = 𝑘))
152	85	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑒 = 𝑘) → (ℎ𝑆𝑘 ∨ ℎ = 𝑘))
153		ordir 1004	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑘𝑆ℎ ∧ ℎ𝑆𝑘) ∨ ℎ = 𝑘) ↔ ((𝑘𝑆ℎ ∨ ℎ = 𝑘) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘)))
154	151, 152, 153	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑒 = 𝑘) → ((𝑘𝑆ℎ ∧ ℎ𝑆𝑘) ∨ ℎ = 𝑘))
155		po2nr 5517	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 Po 𝐵 ∧ (𝑘 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ¬ (𝑘𝑆ℎ ∧ ℎ𝑆𝑘))
156	62, 68, 66, 155	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ¬ (𝑘𝑆ℎ ∧ ℎ𝑆𝑘))
157	156	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑒 = 𝑘) → ¬ (𝑘𝑆ℎ ∧ ℎ𝑆𝑘))
158	154, 157	orcnd 876	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑒 = 𝑘) → ℎ = 𝑘)
159	158	ex 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒 = 𝑘 → ℎ = 𝑘))
160		breq1 5077	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = 𝑙 → (𝑓𝑇𝑖 ↔ 𝑙𝑇𝑖))
161		equequ1 2028	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = 𝑙 → (𝑓 = 𝑖 ↔ 𝑙 = 𝑖))
162	160, 161	orbi12d 916	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑙 → ((𝑓𝑇𝑖 ∨ 𝑓 = 𝑖) ↔ (𝑙𝑇𝑖 ∨ 𝑙 = 𝑖)))
163	104, 162	syl5ibcom 244	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓 = 𝑙 → (𝑙𝑇𝑖 ∨ 𝑙 = 𝑖)))
164	163	imp 407	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → (𝑙𝑇𝑖 ∨ 𝑙 = 𝑖))
165		equcom 2021	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑙 = 𝑖 ↔ 𝑖 = 𝑙)
166	165	orbi2i 910	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑙𝑇𝑖 ∨ 𝑙 = 𝑖) ↔ (𝑙𝑇𝑖 ∨ 𝑖 = 𝑙))
167	164, 166	sylib 217	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → (𝑙𝑇𝑖 ∨ 𝑖 = 𝑙))
168	111	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙))
169		ordir 1004	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑙𝑇𝑖 ∧ 𝑖𝑇𝑙) ∨ 𝑖 = 𝑙) ↔ ((𝑙𝑇𝑖 ∨ 𝑖 = 𝑙) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)))
170	167, 168, 169	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → ((𝑙𝑇𝑖 ∧ 𝑖𝑇𝑙) ∨ 𝑖 = 𝑙))
171		po2nr 5517	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑇 Po 𝐶 ∧ (𝑙 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶)) → ¬ (𝑙𝑇𝑖 ∧ 𝑖𝑇𝑙))
172	88, 94, 92, 171	syl12anc 834	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ¬ (𝑙𝑇𝑖 ∧ 𝑖𝑇𝑙))
173	172	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → ¬ (𝑙𝑇𝑖 ∧ 𝑖𝑇𝑙))
174	170, 173	orcnd 876	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → 𝑖 = 𝑙)
175	174	ex 413	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓 = 𝑙 → 𝑖 = 𝑙))
176	144, 159, 175	3anim123d 1442	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑑 = 𝑗 ∧ 𝑒 = 𝑘 ∧ 𝑓 = 𝑙) → (𝑔 = 𝑗 ∧ ℎ = 𝑘 ∧ 𝑖 = 𝑙)))
177	129, 176	syl5bir 242	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (¬ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙) → (𝑔 = 𝑗 ∧ ℎ = 𝑘 ∧ 𝑖 = 𝑙)))
178	122, 177	mt3d 148	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙))
179	113, 178	jca 512	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙)))
180	33, 34, 179	3jca 1127	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙))))
181	180	ex 413	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙)))))
182		breq12 5079	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩) → (𝑎𝑈𝑏 ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩𝑈⟨⟨𝑔, ℎ⟩, 𝑖⟩))
183	182	3adant3 1131	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑎𝑈𝑏 ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩𝑈⟨⟨𝑔, ℎ⟩, 𝑖⟩))
184	11	xpord3lem 33795	. . . . . . . . . . . . . . . . 17 ⊢ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩𝑈⟨⟨𝑔, ℎ⟩, 𝑖⟩ ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))
185	183, 184	bitrdi 287	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑎𝑈𝑏 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))))
186		breq12 5079	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑏𝑈𝑐 ↔ ⟨⟨𝑔, ℎ⟩, 𝑖⟩𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
187	186	3adant1 1129	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑏𝑈𝑐 ↔ ⟨⟨𝑔, ℎ⟩, 𝑖⟩𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
188	11	xpord3lem 33795	. . . . . . . . . . . . . . . . 17 ⊢ (⟨⟨𝑔, ℎ⟩, 𝑖⟩𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩ ↔ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))
189	187, 188	bitrdi 287	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑏𝑈𝑐 ↔ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))))
190	185, 189	anbi12d 631	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))))
191		breq12 5079	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑎𝑈𝑐 ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
192	191	3adant2 1130	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑎𝑈𝑐 ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
193	11	xpord3lem 33795	. . . . . . . . . . . . . . . 16 ⊢ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩ ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙))))
194	192, 193	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑎𝑈𝑐 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙)))))
195	190, 194	imbi12d 345	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙))))))
196	181, 195	syl5ibrcom 246	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
197	196	rexlimdvw 3219	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
198	197	a1d 25	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑓 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶) → (∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐))))
199	198	rexlimdvv 3222	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
200	199	rexlimdvw 3219	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
201	200	a1d 25	. . . . . . . 8 ⊢ (𝜑 → ((𝑒 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → (∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐))))
202	201	rexlimdvv 3222	. . . . . . 7 ⊢ (𝜑 → (∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
203	202	rexlimdvw 3219	. . . . . 6 ⊢ (𝜑 → (∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
204	203	a1d 25	. . . . 5 ⊢ (𝜑 → ((𝑑 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐))))
205	204	rexlimdvv 3222	. . . 4 ⊢ (𝜑 → (∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
206	32, 205	syl5bi 241	. . 3 ⊢ (𝜑 → ((𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑐 ∈ ((𝐴 × 𝐵) × 𝐶)) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
207	206	imp 407	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑐 ∈ ((𝐴 × 𝐵) × 𝐶))) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐))
208	19, 207	ispod 5512	1 ⊢ (𝜑 → 𝑈 Po ((𝐴 × 𝐵) × 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 ∨ w3o 1085 ∧ w3a 1086 = wceq 1539 ∈ wcel 2106 ≠ wne 2943 ∃wrex 3065 ⟨cop 4567 class class class wbr 5074 {copab 5136 Po wpo 5501 × cxp 5587 ‘cfv 6433 1^st c1st 7829 2^nd c2nd 7830

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pr 5352 ax-un 7588

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ne 2944 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-sbc 3717 df-csb 3833 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-iun 4926 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5489 df-po 5503 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-iota 6391 df-fun 6435 df-fv 6441 df-1st 7831 df-2nd 7832

This theorem is referenced by: xpord3ind 33800

W3C validator