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 33363

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 33214	. . . 4 ⊢ (𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩)
2		neirr 2960	. . . . . . . . . . 11 ⊢ ¬ 𝑑 ≠ 𝑑
3		neirr 2960	. . . . . . . . . . 11 ⊢ ¬ 𝑒 ≠ 𝑒
4		neirr 2960	. . . . . . . . . . 11 ⊢ ¬ 𝑓 ≠ 𝑓
5	2, 3, 4	3pm3.2ni 33186	. . . . . . . . . 10 ⊢ ¬ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓)
6	5	intnan 490	. . . . . . . . 9 ⊢ ¬ (((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓))
7		simp3 1135	. . . . . . . . 9 ⊢ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓))) → (((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓)))
8	6, 7	mto 200	. . . . . . . 8 ⊢ ¬ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓)))
9		breq12 5041	. . . . . . . . . 10 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩) → (𝑎𝑈𝑎 ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩𝑈⟨⟨𝑑, 𝑒⟩, 𝑓⟩))
10	9	anidms 570	. . . . . . . . 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 33362	. . . . . . . . 9 ⊢ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩𝑈⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓))))
13	10, 12	bitrdi 290	. . . . . . . 8 ⊢ (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑎𝑈𝑎 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑑𝑅𝑑 ∨ 𝑑 = 𝑑) ∧ (𝑒𝑆𝑒 ∨ 𝑒 = 𝑒) ∧ (𝑓𝑇𝑓 ∨ 𝑓 = 𝑓)) ∧ (𝑑 ≠ 𝑑 ∨ 𝑒 ≠ 𝑒 ∨ 𝑓 ≠ 𝑓)))))
14	8, 13	mtbiri 330	. . . . . . 7 ⊢ (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ¬ 𝑎𝑈𝑎)
15	14	rexlimivw 3206	. . . . . 6 ⊢ (∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ¬ 𝑎𝑈𝑎)
16	15	a1i 11	. . . . 5 ⊢ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵) → (∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ¬ 𝑎𝑈𝑎))
17	16	rexlimivv 3216	. . . 4 ⊢ (∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ¬ 𝑎𝑈𝑎)
18	1, 17	sylbi 220	. . 3 ⊢ (𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) → ¬ 𝑎𝑈𝑎)
19	18	adantl 485	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ ((𝐴 × 𝐵) × 𝐶)) → ¬ 𝑎𝑈𝑎)
20		elxpxp 33214	. . . . . 6 ⊢ (𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩)
21		elxpxp 33214	. . . . . 6 ⊢ (𝑐 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑗 ∈ 𝐴 ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩)
22	1, 20, 21	3anbi123i 1152	. . . . 5 ⊢ ((𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑐 ∈ ((𝐴 × 𝐵) × 𝐶)) ↔ (∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑗 ∈ 𝐴 ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
23		3reeanv 3286	. . . . . . . . . . 11 ⊢ (∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ (∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
24	23	rexbii 3175	. . . . . . . . . 10 ⊢ (∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ ∃𝑘 ∈ 𝐵 (∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
25	24	2rexbii 3176	. . . . . . . . 9 ⊢ (∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 (∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
26		3reeanv 3286	. . . . . . . . 9 ⊢ (∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 (∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ (∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
27	25, 26	bitri 278	. . . . . . . 8 ⊢ (∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ (∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
28	27	rexbii 3175	. . . . . . 7 ⊢ (∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ ∃𝑗 ∈ 𝐴 (∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
29	28	2rexbii 3176	. . . . . 6 ⊢ (∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ ∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 (∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
30		3reeanv 3286	. . . . . 6 ⊢ (∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 (∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ (∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑗 ∈ 𝐴 ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
31	29, 30	bitri 278	. . . . 5 ⊢ (∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) ↔ (∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ ∃𝑗 ∈ 𝐴 ∃𝑘 ∈ 𝐵 ∃𝑙 ∈ 𝐶 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
32	22, 31	bitr4i 281	. . . 4 ⊢ ((𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑐 ∈ ((𝐴 × 𝐵) × 𝐶)) ↔ ∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
33		simprl1 1215	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶))
34		simprr2 1219	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶))
35		poxp3.1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑅 Po 𝐴)
36	35	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑅 Po 𝐴)
37		simpl11 1245	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑑 ∈ 𝐴)
38	37	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑑 ∈ 𝐴)
39		simpr11 1254	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑔 ∈ 𝐴)
40	39	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑔 ∈ 𝐴)
41		simpr21 1257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑗 ∈ 𝐴)
42	41	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑗 ∈ 𝐴)
43		potr 5459	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 Po 𝐴 ∧ (𝑑 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴 ∧ 𝑗 ∈ 𝐴)) → ((𝑑𝑅𝑔 ∧ 𝑔𝑅𝑗) → 𝑑𝑅𝑗))
44	36, 38, 40, 42, 43	syl13anc 1369	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑑𝑅𝑔 ∧ 𝑔𝑅𝑗) → 𝑑𝑅𝑗))
45		orc 864	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑𝑅𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗))
46	44, 45	syl6 35	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑑𝑅𝑔 ∧ 𝑔𝑅𝑗) → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗)))
47	46	expd 419	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑𝑅𝑔 → (𝑔𝑅𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗))))
48		breq1 5039	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = 𝑔 → (𝑑𝑅𝑗 ↔ 𝑔𝑅𝑗))
49	48, 45	syl6bir 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑔 → (𝑔𝑅𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗)))
50	49	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑 = 𝑔 → (𝑔𝑅𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗))))
51		simp3l1 1275	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑑𝑅𝑔 ∨ 𝑑 = 𝑔))
52	51	ad2antrl 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑𝑅𝑔 ∨ 𝑑 = 𝑔))
53	47, 50, 52	mpjaod 857	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑔𝑅𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗)))
54		breq2 5040	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑗 → (𝑑𝑅𝑔 ↔ 𝑑𝑅𝑗))
55		equequ2 2033	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 = 𝑗 → (𝑑 = 𝑔 ↔ 𝑑 = 𝑗))
56	54, 55	orbi12d 916	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 = 𝑗 → ((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ↔ (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗)))
57	52, 56	syl5ibcom 248	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑔 = 𝑗 → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗)))
58		simp3l1 1275	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))) → (𝑔𝑅𝑗 ∨ 𝑔 = 𝑗))
59	58	ad2antll 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑔𝑅𝑗 ∨ 𝑔 = 𝑗))
60	53, 57, 59	mpjaod 857	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑𝑅𝑗 ∨ 𝑑 = 𝑗))
61		poxp3.2	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑆 Po 𝐵)
62	61	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑆 Po 𝐵)
63		simpl12 1246	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑒 ∈ 𝐵)
64	63	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑒 ∈ 𝐵)
65		simpr12 1255	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → ℎ ∈ 𝐵)
66	65	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ℎ ∈ 𝐵)
67		simpr22 1258	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑘 ∈ 𝐵)
68	67	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑘 ∈ 𝐵)
69		potr 5459	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 Po 𝐵 ∧ (𝑒 ∈ 𝐵 ∧ ℎ ∈ 𝐵 ∧ 𝑘 ∈ 𝐵)) → ((𝑒𝑆ℎ ∧ ℎ𝑆𝑘) → 𝑒𝑆𝑘))
70	62, 64, 66, 68, 69	syl13anc 1369	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑒𝑆ℎ ∧ ℎ𝑆𝑘) → 𝑒𝑆𝑘))
71		orc 864	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒𝑆𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘))
72	70, 71	syl6 35	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑒𝑆ℎ ∧ ℎ𝑆𝑘) → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘)))
73	72	expd 419	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒𝑆ℎ → (ℎ𝑆𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘))))
74		breq1 5039	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒 = ℎ → (𝑒𝑆𝑘 ↔ ℎ𝑆𝑘))
75	74, 71	syl6bir 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = ℎ → (ℎ𝑆𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘)))
76	75	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒 = ℎ → (ℎ𝑆𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘))))
77		simp3l2 1276	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑒𝑆ℎ ∨ 𝑒 = ℎ))
78	77	ad2antrl 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒𝑆ℎ ∨ 𝑒 = ℎ))
79	73, 76, 78	mpjaod 857	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (ℎ𝑆𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘)))
80		breq2 5040	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ = 𝑘 → (𝑒𝑆ℎ ↔ 𝑒𝑆𝑘))
81		equequ2 2033	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ = 𝑘 → (𝑒 = ℎ ↔ 𝑒 = 𝑘))
82	80, 81	orbi12d 916	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ = 𝑘 → ((𝑒𝑆ℎ ∨ 𝑒 = ℎ) ↔ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘)))
83	78, 82	syl5ibcom 248	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (ℎ = 𝑘 → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘)))
84		simp3l2 1276	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))) → (ℎ𝑆𝑘 ∨ ℎ = 𝑘))
85	84	ad2antll 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (ℎ𝑆𝑘 ∨ ℎ = 𝑘))
86	79, 83, 85	mpjaod 857	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘))
87		poxp3.3	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → 𝑇 Po 𝐶)
88	87	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑇 Po 𝐶)
89		simpl13 1247	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑓 ∈ 𝐶)
90	89	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑓 ∈ 𝐶)
91		simpr13 1256	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑖 ∈ 𝐶)
92	91	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑖 ∈ 𝐶)
93		simpr23 1259	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → 𝑙 ∈ 𝐶)
94	93	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → 𝑙 ∈ 𝐶)
95		potr 5459	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑇 Po 𝐶 ∧ (𝑓 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶 ∧ 𝑙 ∈ 𝐶)) → ((𝑓𝑇𝑖 ∧ 𝑖𝑇𝑙) → 𝑓𝑇𝑙))
96	88, 90, 92, 94, 95	syl13anc 1369	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑓𝑇𝑖 ∧ 𝑖𝑇𝑙) → 𝑓𝑇𝑙))
97		orc 864	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓𝑇𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙))
98	96, 97	syl6 35	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑓𝑇𝑖 ∧ 𝑖𝑇𝑙) → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)))
99	98	expd 419	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓𝑇𝑖 → (𝑖𝑇𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙))))
100		breq1 5039	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 = 𝑖 → (𝑓𝑇𝑙 ↔ 𝑖𝑇𝑙))
101	100, 97	syl6bir 257	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑖 → (𝑖𝑇𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)))
102	101	a1i 11	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓 = 𝑖 → (𝑖𝑇𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙))))
103		simp3l3 1277	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖))
104	103	ad2antrl 727	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖))
105	99, 102, 104	mpjaod 857	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑖𝑇𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)))
106		breq2 5040	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑙 → (𝑓𝑇𝑖 ↔ 𝑓𝑇𝑙))
107		equequ2 2033	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 = 𝑙 → (𝑓 = 𝑖 ↔ 𝑓 = 𝑙))
108	106, 107	orbi12d 916	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑖 = 𝑙 → ((𝑓𝑇𝑖 ∨ 𝑓 = 𝑖) ↔ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)))
109	104, 108	syl5ibcom 248	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑖 = 𝑙 → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)))
110		simp3l3 1277	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))) → (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙))
111	110	ad2antll 728	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙))
112	105, 109, 111	mpjaod 857	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙))
113	60, 86, 112	3jca 1125	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)))
114		simpr3r 1232	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))
115	114	adantl 485	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))
116		df-ne 2952	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 ≠ 𝑗 ↔ ¬ 𝑔 = 𝑗)
117		df-ne 2952	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ ≠ 𝑘 ↔ ¬ ℎ = 𝑘)
118		df-ne 2952	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑖 ≠ 𝑙 ↔ ¬ 𝑖 = 𝑙)
119	116, 117, 118	3orbi123i 1153	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙) ↔ (¬ 𝑔 = 𝑗 ∨ ¬ ℎ = 𝑘 ∨ ¬ 𝑖 = 𝑙))
120		3ianor 1104	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ (𝑔 = 𝑗 ∧ ℎ = 𝑘 ∧ 𝑖 = 𝑙) ↔ (¬ 𝑔 = 𝑗 ∨ ¬ ℎ = 𝑘 ∨ ¬ 𝑖 = 𝑙))
121	119, 120	bitr4i 281	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙) ↔ ¬ (𝑔 = 𝑗 ∧ ℎ = 𝑘 ∧ 𝑖 = 𝑙))
122	115, 121	sylib 221	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ¬ (𝑔 = 𝑗 ∧ ℎ = 𝑘 ∧ 𝑖 = 𝑙))
123		df-ne 2952	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 ≠ 𝑗 ↔ ¬ 𝑑 = 𝑗)
124		df-ne 2952	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑒 ≠ 𝑘 ↔ ¬ 𝑒 = 𝑘)
125		df-ne 2952	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑓 ≠ 𝑙 ↔ ¬ 𝑓 = 𝑙)
126	123, 124, 125	3orbi123i 1153	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙) ↔ (¬ 𝑑 = 𝑗 ∨ ¬ 𝑒 = 𝑘 ∨ ¬ 𝑓 = 𝑙))
127		3ianor 1104	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝑑 = 𝑗 ∧ 𝑒 = 𝑘 ∧ 𝑓 = 𝑙) ↔ (¬ 𝑑 = 𝑗 ∨ ¬ 𝑒 = 𝑘 ∨ ¬ 𝑓 = 𝑙))
128	126, 127	bitr4i 281	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙) ↔ ¬ (𝑑 = 𝑗 ∧ 𝑒 = 𝑘 ∧ 𝑓 = 𝑙))
129	128	con2bii 361	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑑 = 𝑗 ∧ 𝑒 = 𝑘 ∧ 𝑓 = 𝑙) ↔ ¬ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙))
130		breq1 5039	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = 𝑗 → (𝑑𝑅𝑔 ↔ 𝑗𝑅𝑔))
131		equequ1 2032	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 = 𝑗 → (𝑑 = 𝑔 ↔ 𝑗 = 𝑔))
132		equcom 2025	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 = 𝑔 ↔ 𝑔 = 𝑗)
133	131, 132	bitrdi 290	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = 𝑗 → (𝑑 = 𝑔 ↔ 𝑔 = 𝑗))
134	130, 133	orbi12d 916	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = 𝑗 → ((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ↔ (𝑗𝑅𝑔 ∨ 𝑔 = 𝑗)))
135	52, 134	syl5ibcom 248	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑 = 𝑗 → (𝑗𝑅𝑔 ∨ 𝑔 = 𝑗)))
136	135	imp 410	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑑 = 𝑗) → (𝑗𝑅𝑔 ∨ 𝑔 = 𝑗))
137	59	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑑 = 𝑗) → (𝑔𝑅𝑗 ∨ 𝑔 = 𝑗))
138		ordir 1004	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑗𝑅𝑔 ∧ 𝑔𝑅𝑗) ∨ 𝑔 = 𝑗) ↔ ((𝑗𝑅𝑔 ∨ 𝑔 = 𝑗) ∧ (𝑔𝑅𝑗 ∨ 𝑔 = 𝑗)))
139	136, 137, 138	sylanbrc 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑑 = 𝑗) → ((𝑗𝑅𝑔 ∧ 𝑔𝑅𝑗) ∨ 𝑔 = 𝑗))
140		po2nr 5460	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Po 𝐴 ∧ (𝑗 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → ¬ (𝑗𝑅𝑔 ∧ 𝑔𝑅𝑗))
141	36, 42, 40, 140	syl12anc 835	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ¬ (𝑗𝑅𝑔 ∧ 𝑔𝑅𝑗))
142	141	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑑 = 𝑗) → ¬ (𝑗𝑅𝑔 ∧ 𝑔𝑅𝑗))
143	139, 142	orcnd 876	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑑 = 𝑗) → 𝑔 = 𝑗)
144	143	ex 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑 = 𝑗 → 𝑔 = 𝑗))
145		breq1 5039	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑒 = 𝑘 → (𝑒𝑆ℎ ↔ 𝑘𝑆ℎ))
146		equequ1 2032	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑒 = 𝑘 → (𝑒 = ℎ ↔ 𝑘 = ℎ))
147		equcom 2025	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑘 = ℎ ↔ ℎ = 𝑘)
148	146, 147	bitrdi 290	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑒 = 𝑘 → (𝑒 = ℎ ↔ ℎ = 𝑘))
149	145, 148	orbi12d 916	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑒 = 𝑘 → ((𝑒𝑆ℎ ∨ 𝑒 = ℎ) ↔ (𝑘𝑆ℎ ∨ ℎ = 𝑘)))
150	78, 149	syl5ibcom 248	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒 = 𝑘 → (𝑘𝑆ℎ ∨ ℎ = 𝑘)))
151	150	imp 410	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑒 = 𝑘) → (𝑘𝑆ℎ ∨ ℎ = 𝑘))
152	85	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑒 = 𝑘) → (ℎ𝑆𝑘 ∨ ℎ = 𝑘))
153		ordir 1004	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑘𝑆ℎ ∧ ℎ𝑆𝑘) ∨ ℎ = 𝑘) ↔ ((𝑘𝑆ℎ ∨ ℎ = 𝑘) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘)))
154	151, 152, 153	sylanbrc 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑒 = 𝑘) → ((𝑘𝑆ℎ ∧ ℎ𝑆𝑘) ∨ ℎ = 𝑘))
155		po2nr 5460	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 Po 𝐵 ∧ (𝑘 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ¬ (𝑘𝑆ℎ ∧ ℎ𝑆𝑘))
156	62, 68, 66, 155	syl12anc 835	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ¬ (𝑘𝑆ℎ ∧ ℎ𝑆𝑘))
157	156	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑒 = 𝑘) → ¬ (𝑘𝑆ℎ ∧ ℎ𝑆𝑘))
158	154, 157	orcnd 876	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑒 = 𝑘) → ℎ = 𝑘)
159	158	ex 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑒 = 𝑘 → ℎ = 𝑘))
160		breq1 5039	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = 𝑙 → (𝑓𝑇𝑖 ↔ 𝑙𝑇𝑖))
161		equequ1 2032	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑓 = 𝑙 → (𝑓 = 𝑖 ↔ 𝑙 = 𝑖))
162	160, 161	orbi12d 916	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑓 = 𝑙 → ((𝑓𝑇𝑖 ∨ 𝑓 = 𝑖) ↔ (𝑙𝑇𝑖 ∨ 𝑙 = 𝑖)))
163	104, 162	syl5ibcom 248	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓 = 𝑙 → (𝑙𝑇𝑖 ∨ 𝑙 = 𝑖)))
164	163	imp 410	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → (𝑙𝑇𝑖 ∨ 𝑙 = 𝑖))
165		equcom 2025	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑙 = 𝑖 ↔ 𝑖 = 𝑙)
166	165	orbi2i 910	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑙𝑇𝑖 ∨ 𝑙 = 𝑖) ↔ (𝑙𝑇𝑖 ∨ 𝑖 = 𝑙))
167	164, 166	sylib 221	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → (𝑙𝑇𝑖 ∨ 𝑖 = 𝑙))
168	111	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙))
169		ordir 1004	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑙𝑇𝑖 ∧ 𝑖𝑇𝑙) ∨ 𝑖 = 𝑙) ↔ ((𝑙𝑇𝑖 ∨ 𝑖 = 𝑙) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)))
170	167, 168, 169	sylanbrc 586	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → ((𝑙𝑇𝑖 ∧ 𝑖𝑇𝑙) ∨ 𝑖 = 𝑙))
171		po2nr 5460	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑇 Po 𝐶 ∧ (𝑙 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶)) → ¬ (𝑙𝑇𝑖 ∧ 𝑖𝑇𝑙))
172	88, 94, 92, 171	syl12anc 835	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ¬ (𝑙𝑇𝑖 ∧ 𝑖𝑇𝑙))
173	172	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → ¬ (𝑙𝑇𝑖 ∧ 𝑖𝑇𝑙))
174	170, 173	orcnd 876	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) ∧ 𝑓 = 𝑙) → 𝑖 = 𝑙)
175	174	ex 416	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑓 = 𝑙 → 𝑖 = 𝑙))
176	144, 159, 175	3anim123d 1440	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑑 = 𝑗 ∧ 𝑒 = 𝑘 ∧ 𝑓 = 𝑙) → (𝑔 = 𝑗 ∧ ℎ = 𝑘 ∧ 𝑖 = 𝑙)))
177	129, 176	syl5bir 246	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (¬ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙) → (𝑔 = 𝑗 ∧ ℎ = 𝑘 ∧ 𝑖 = 𝑙)))
178	122, 177	mt3d 150	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙))
179	113, 178	jca 515	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙)))
180	33, 34, 179	3jca 1125	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))) → ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙))))
181	180	ex 416	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙)))))
182		breq12 5041	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩) → (𝑎𝑈𝑏 ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩𝑈⟨⟨𝑔, ℎ⟩, 𝑖⟩))
183	182	3adant3 1129	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑎𝑈𝑏 ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩𝑈⟨⟨𝑔, ℎ⟩, 𝑖⟩))
184	11	xpord3lem 33362	. . . . . . . . . . . . . . . . 17 ⊢ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩𝑈⟨⟨𝑔, ℎ⟩, 𝑖⟩ ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))
185	183, 184	bitrdi 290	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑎𝑈𝑏 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))))
186		breq12 5041	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑏𝑈𝑐 ↔ ⟨⟨𝑔, ℎ⟩, 𝑖⟩𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
187	186	3adant1 1127	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑏𝑈𝑐 ↔ ⟨⟨𝑔, ℎ⟩, 𝑖⟩𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
188	11	xpord3lem 33362	. . . . . . . . . . . . . . . . 17 ⊢ (⟨⟨𝑔, ℎ⟩, 𝑖⟩𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩ ↔ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))
189	187, 188	bitrdi 290	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑏𝑈𝑐 ↔ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))))
190	185, 189	anbi12d 633	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) ↔ (((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙))))))
191		breq12 5041	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑎𝑈𝑐 ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
192	191	3adant2 1128	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑎𝑈𝑐 ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩))
193	11	xpord3lem 33362	. . . . . . . . . . . . . . . 16 ⊢ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩𝑈⟨⟨𝑗, 𝑘⟩, 𝑙⟩ ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙))))
194	192, 193	bitrdi 290	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (𝑎𝑈𝑐 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙)))))
195	190, 194	imbi12d 348	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → (((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐) ↔ ((((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) ∧ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑔𝑅𝑗 ∨ 𝑔 = 𝑗) ∧ (ℎ𝑆𝑘 ∨ ℎ = 𝑘) ∧ (𝑖𝑇𝑙 ∨ 𝑖 = 𝑙)) ∧ (𝑔 ≠ 𝑗 ∨ ℎ ≠ 𝑘 ∨ 𝑖 ≠ 𝑙)))) → ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ∧ 𝑙 ∈ 𝐶) ∧ (((𝑑𝑅𝑗 ∨ 𝑑 = 𝑗) ∧ (𝑒𝑆𝑘 ∨ 𝑒 = 𝑘) ∧ (𝑓𝑇𝑙 ∨ 𝑓 = 𝑙)) ∧ (𝑑 ≠ 𝑗 ∨ 𝑒 ≠ 𝑘 ∨ 𝑓 ≠ 𝑙))))))
196	181, 195	syl5ibrcom 250	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
197	196	rexlimdvw 3214	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
198	197	a1d 25	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝑓 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶) → (∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐))))
199	198	rexlimdvv 3217	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
200	199	rexlimdvw 3214	. . . . . . . . 9 ⊢ (𝜑 → (∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
201	200	a1d 25	. . . . . . . 8 ⊢ (𝜑 → ((𝑒 ∈ 𝐵 ∧ ℎ ∈ 𝐵) → (∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐))))
202	201	rexlimdvv 3217	. . . . . . 7 ⊢ (𝜑 → (∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
203	202	rexlimdvw 3214	. . . . . 6 ⊢ (𝜑 → (∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
204	203	a1d 25	. . . . 5 ⊢ (𝜑 → ((𝑑 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐))))
205	204	rexlimdvv 3217	. . . 4 ⊢ (𝜑 → (∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑗 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑘 ∈ 𝐵 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 ∃𝑙 ∈ 𝐶 (𝑎 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∧ 𝑏 = ⟨⟨𝑔, ℎ⟩, 𝑖⟩ ∧ 𝑐 = ⟨⟨𝑗, 𝑘⟩, 𝑙⟩) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
206	32, 205	syl5bi 245	. . 3 ⊢ (𝜑 → ((𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑐 ∈ ((𝐴 × 𝐵) × 𝐶)) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐)))
207	206	imp 410	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑏 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑐 ∈ ((𝐴 × 𝐵) × 𝐶))) → ((𝑎𝑈𝑏 ∧ 𝑏𝑈𝑐) → 𝑎𝑈𝑐))
208	19, 207	ispod 5455	1 ⊢ (𝜑 → 𝑈 Po ((𝐴 × 𝐵) × 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 ∨ w3o 1083 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ≠ wne 2951 ∃wrex 3071 ⟨cop 4531 class class class wbr 5036 {copab 5098 Po wpo 5445 × cxp 5526 ‘cfv 6340 1^st c1st 7697 2^nd c2nd 7698

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-sep 5173 ax-nul 5180 ax-pr 5302 ax-un 7465

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-ral 3075 df-rex 3076 df-rab 3079 df-v 3411 df-sbc 3699 df-csb 3808 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-nul 4228 df-if 4424 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4802 df-iun 4888 df-br 5037 df-opab 5099 df-mpt 5117 df-id 5434 df-po 5447 df-xp 5534 df-rel 5535 df-cnv 5536 df-co 5537 df-dm 5538 df-rn 5539 df-iota 6299 df-fun 6342 df-fv 6348 df-1st 7699 df-2nd 7700

This theorem is referenced by: xpord3ind 33367 no3indslem 33697

W3C validator