poxp3 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > poxp3		Structured version Visualization version GIF version

Theorem poxp3 8160

Description: Triple Cartesian 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		el2xptp 5820	. . . 4 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩)
2		neirr 2965	. . . . . . . . . . 11 ⊢ ¬ 𝑎 ≠ 𝑎
3		neirr 2965	. . . . . . . . . . 11 ⊢ ¬ 𝑏 ≠ 𝑏
4		neirr 2965	. . . . . . . . . . 11 ⊢ ¬ 𝑐 ≠ 𝑐
5	2, 3, 4	3pm3.2ni 1519	. . . . . . . . . 10 ⊢ ¬ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)
6	5	intnan 492	. . . . . . . . 9 ⊢ ¬ (((𝑎𝑅𝑎 ∨ 𝑎 = 𝑎) ∧ (𝑏𝑆𝑏 ∨ 𝑏 = 𝑏) ∧ (𝑐𝑇𝑐 ∨ 𝑐 = 𝑐)) ∧ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))
7		simp3 1156	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑎𝑅𝑎 ∨ 𝑎 = 𝑎) ∧ (𝑏𝑆𝑏 ∨ 𝑏 = 𝑏) ∧ (𝑐𝑇𝑐 ∨ 𝑐 = 𝑐)) ∧ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))) → (((𝑎𝑅𝑎 ∨ 𝑎 = 𝑎) ∧ (𝑏𝑆𝑏 ∨ 𝑏 = 𝑏) ∧ (𝑐𝑇𝑐 ∨ 𝑐 = 𝑐)) ∧ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))
8	6, 7	mto 200	. . . . . . . 8 ⊢ ¬ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑎𝑅𝑎 ∨ 𝑎 = 𝑎) ∧ (𝑏𝑆𝑏 ∨ 𝑏 = 𝑏) ∧ (𝑐𝑇𝑐 ∨ 𝑐 = 𝑐)) ∧ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))
9		breq12 5108	. . . . . . . . . 10 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩) → (𝑝𝑈𝑝 ↔ ⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑎, 𝑏, 𝑐⟩))
10	9	anidms 577	. . . . . . . . 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 8159	. . . . . . . . 9 ⊢ (⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑎𝑅𝑎 ∨ 𝑎 = 𝑎) ∧ (𝑏𝑆𝑏 ∨ 𝑏 = 𝑏) ∧ (𝑐𝑇𝑐 ∨ 𝑐 = 𝑐)) ∧ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))))
13	10, 12	bitrdi 290	. . . . . . . 8 ⊢ (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → (𝑝𝑈𝑝 ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑎𝑅𝑎 ∨ 𝑎 = 𝑎) ∧ (𝑏𝑆𝑏 ∨ 𝑏 = 𝑏) ∧ (𝑐𝑇𝑐 ∨ 𝑐 = 𝑐)) ∧ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))))
14	8, 13	mtbiri 330	. . . . . . 7 ⊢ (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → ¬ 𝑝𝑈𝑝)
15	14	rexlimivw 3160	. . . . . 6 ⊢ (∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → ¬ 𝑝𝑈𝑝)
16	15	rexlimivw 3160	. . . . 5 ⊢ (∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → ¬ 𝑝𝑈𝑝)
17	16	rexlimivw 3160	. . . 4 ⊢ (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → ¬ 𝑝𝑈𝑝)
18	1, 17	sylbi 220	. . 3 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) → ¬ 𝑝𝑈𝑝)
19	18	adantl 487	. 2 ⊢ ((𝜑 ∧ 𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)) → ¬ 𝑝𝑈𝑝)
20		3reeanv 3236	. . . . 5 ⊢ (∃𝑎 ∈ 𝐴 ∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 (∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) ↔ (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
21		3reeanv 3236	. . . . . . . . . 10 ⊢ (∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) ↔ (∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
22	21	rexbii 3110	. . . . . . . . 9 ⊢ (∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) ↔ ∃ℎ ∈ 𝐵 (∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
23	22	2rexbii 3139	. . . . . . . 8 ⊢ (∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) ↔ ∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 (∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
24		3reeanv 3236	. . . . . . . 8 ⊢ (∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 (∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) ↔ (∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
25	23, 24	bitri 278	. . . . . . 7 ⊢ (∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) ↔ (∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
26	25	rexbii 3110	. . . . . 6 ⊢ (∃𝑔 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) ↔ ∃𝑔 ∈ 𝐴 (∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
27	26	2rexbii 3139	. . . . 5 ⊢ (∃𝑎 ∈ 𝐴 ∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) ↔ ∃𝑎 ∈ 𝐴 ∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 (∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
28		el2xptp 5820	. . . . . 6 ⊢ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩)
29		el2xptp 5820	. . . . . 6 ⊢ (𝑟 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩)
30	1, 28, 29	3anbi123i 1173	. . . . 5 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑟 ∈ ((𝐴 × 𝐵) × 𝐶)) ↔ (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
31	20, 27, 30	3bitr4ri 307	. . . 4 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑟 ∈ ((𝐴 × 𝐵) × 𝐶)) ↔ ∃𝑎 ∈ 𝐴 ∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
32		simpr1l 1249	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))
33		simpr2r 1252	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶))
34		poxp3.1	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑅 Po 𝐴)
35		simp1l1 1285	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → 𝑎 ∈ 𝐴)
36		simp2l1 1291	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → 𝑑 ∈ 𝐴)
37		simp2r1 1294	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → 𝑔 ∈ 𝐴)
38	35, 36, 37	3jca 1146	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑎 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴))
39		potr 5572	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → ((𝑎𝑅𝑑 ∧ 𝑑𝑅𝑔) → 𝑎𝑅𝑔))
40	34, 38, 39	syl2an 608	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ((𝑎𝑅𝑑 ∧ 𝑑𝑅𝑔) → 𝑎𝑅𝑔))
41	40	expd 421	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑎𝑅𝑑 → (𝑑𝑅𝑔 → 𝑎𝑅𝑔)))
42		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑑 → (𝑎𝑅𝑔 ↔ 𝑑𝑅𝑔))
43	42	biimprd 251	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑑 → (𝑑𝑅𝑔 → 𝑎𝑅𝑔))
44	43	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑎 = 𝑑 → (𝑑𝑅𝑔 → 𝑎𝑅𝑔)))
45		simpll1 1231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑎𝑅𝑑 ∨ 𝑎 = 𝑑))
46	45	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑎𝑅𝑑 ∨ 𝑎 = 𝑑))
47	46	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑎𝑅𝑑 ∨ 𝑎 = 𝑑))
48	41, 44, 47	mpjaod 874	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑑𝑅𝑔 → 𝑎𝑅𝑔))
49		orc 881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎𝑅𝑔 → (𝑎𝑅𝑔 ∨ 𝑎 = 𝑔))
50	48, 49	syl6 36	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑑𝑅𝑔 → (𝑎𝑅𝑔 ∨ 𝑎 = 𝑔)))
51		breq2 5107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑔 → (𝑎𝑅𝑑 ↔ 𝑎𝑅𝑔))
52		equequ2 2059	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑔 → (𝑎 = 𝑑 ↔ 𝑎 = 𝑔))
53	51, 52	orbi12d 932	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑔 → ((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ↔ (𝑎𝑅𝑔 ∨ 𝑎 = 𝑔)))
54	47, 53	syl5ibcom 248	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑑 = 𝑔 → (𝑎𝑅𝑔 ∨ 𝑎 = 𝑔)))
55		simprl1 1237	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑑𝑅𝑔 ∨ 𝑑 = 𝑔))
56	55	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑑𝑅𝑔 ∨ 𝑑 = 𝑔))
57	56	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑑𝑅𝑔 ∨ 𝑑 = 𝑔))
58	50, 54, 57	mpjaod 874	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑎𝑅𝑔 ∨ 𝑎 = 𝑔))
59		poxp3.2	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑆 Po 𝐵)
60		simp1l2 1286	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → 𝑏 ∈ 𝐵)
61		simp2l2 1292	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → 𝑒 ∈ 𝐵)
62		simp2r2 1295	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → ℎ ∈ 𝐵)
63	60, 61, 62	3jca 1146	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑏 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ∧ ℎ ∈ 𝐵))
64		potr 5572	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑏𝑆𝑒 ∧ 𝑒𝑆ℎ) → 𝑏𝑆ℎ))
65	59, 63, 64	syl2an 608	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ((𝑏𝑆𝑒 ∧ 𝑒𝑆ℎ) → 𝑏𝑆ℎ))
66	65	expd 421	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑏𝑆𝑒 → (𝑒𝑆ℎ → 𝑏𝑆ℎ)))
67		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = 𝑒 → (𝑏𝑆ℎ ↔ 𝑒𝑆ℎ))
68	67	biimprd 251	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = 𝑒 → (𝑒𝑆ℎ → 𝑏𝑆ℎ))
69	68	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑏 = 𝑒 → (𝑒𝑆ℎ → 𝑏𝑆ℎ)))
70		simpll2 1232	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒))
71	70	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒))
72	71	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒))
73	66, 69, 72	mpjaod 874	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑒𝑆ℎ → 𝑏𝑆ℎ))
74		orc 881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏𝑆ℎ → (𝑏𝑆ℎ ∨ 𝑏 = ℎ))
75	73, 74	syl6 36	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑒𝑆ℎ → (𝑏𝑆ℎ ∨ 𝑏 = ℎ)))
76		breq2 5107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = ℎ → (𝑏𝑆𝑒 ↔ 𝑏𝑆ℎ))
77		equequ2 2059	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = ℎ → (𝑏 = 𝑒 ↔ 𝑏 = ℎ))
78	76, 77	orbi12d 932	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = ℎ → ((𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ↔ (𝑏𝑆ℎ ∨ 𝑏 = ℎ)))
79	72, 78	syl5ibcom 248	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑒 = ℎ → (𝑏𝑆ℎ ∨ 𝑏 = ℎ)))
80		simprl2 1238	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑒𝑆ℎ ∨ 𝑒 = ℎ))
81	80	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑒𝑆ℎ ∨ 𝑒 = ℎ))
82	81	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑒𝑆ℎ ∨ 𝑒 = ℎ))
83	75, 79, 82	mpjaod 874	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑏𝑆ℎ ∨ 𝑏 = ℎ))
84		poxp3.3	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑇 Po 𝐶)
85		simp1l3 1287	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → 𝑐 ∈ 𝐶)
86		simp2l3 1293	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → 𝑓 ∈ 𝐶)
87		simp2r3 1296	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → 𝑖 ∈ 𝐶)
88	85, 86, 87	3jca 1146	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑐 ∈ 𝐶 ∧ 𝑓 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶))
89		potr 5572	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑇 Po 𝐶 ∧ (𝑐 ∈ 𝐶 ∧ 𝑓 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶)) → ((𝑐𝑇𝑓 ∧ 𝑓𝑇𝑖) → 𝑐𝑇𝑖))
90	84, 88, 89	syl2an 608	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ((𝑐𝑇𝑓 ∧ 𝑓𝑇𝑖) → 𝑐𝑇𝑖))
91	90	expd 421	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑐𝑇𝑓 → (𝑓𝑇𝑖 → 𝑐𝑇𝑖)))
92		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = 𝑓 → (𝑐𝑇𝑖 ↔ 𝑓𝑇𝑖))
93	92	biimprd 251	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 = 𝑓 → (𝑓𝑇𝑖 → 𝑐𝑇𝑖))
94	93	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑐 = 𝑓 → (𝑓𝑇𝑖 → 𝑐𝑇𝑖)))
95		simpll3 1233	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓))
96	95	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓))
97	96	adantl 487	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓))
98	91, 94, 97	mpjaod 874	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑓𝑇𝑖 → 𝑐𝑇𝑖))
99		orc 881	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐𝑇𝑖 → (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖))
100	98, 99	syl6 36	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑓𝑇𝑖 → (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)))
101		breq2 5107	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑖 → (𝑐𝑇𝑓 ↔ 𝑐𝑇𝑖))
102		equequ2 2059	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑖 → (𝑐 = 𝑓 ↔ 𝑐 = 𝑖))
103	101, 102	orbi12d 932	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑖 → ((𝑐𝑇𝑓 ∨ 𝑐 = 𝑓) ↔ (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)))
104	97, 103	syl5ibcom 248	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑓 = 𝑖 → (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)))
105		simprl3 1239	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖))
106	105	3ad2ant3 1153	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖))
107	106	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖))
108	100, 104, 107	mpjaod 874	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖))
109	58, 83, 108	3jca 1146	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ((𝑎𝑅𝑔 ∨ 𝑎 = 𝑔) ∧ (𝑏𝑆ℎ ∨ 𝑏 = ℎ) ∧ (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)))
110		simp3rr 1266	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))
111	110	adantl 487	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))
112	57	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑎 = 𝑔) → (𝑑𝑅𝑔 ∨ 𝑑 = 𝑔))
113		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑔 → (𝑎𝑅𝑑 ↔ 𝑔𝑅𝑑))
114		equequ1 2058	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑔 → (𝑎 = 𝑑 ↔ 𝑔 = 𝑑))
115		equcom 2051	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔 = 𝑑 ↔ 𝑑 = 𝑔)
116	114, 115	bitrdi 290	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑔 → (𝑎 = 𝑑 ↔ 𝑑 = 𝑔))
117	113, 116	orbi12d 932	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑔 → ((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ↔ (𝑔𝑅𝑑 ∨ 𝑑 = 𝑔)))
118	47, 117	syl5ibcom 248	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑎 = 𝑔 → (𝑔𝑅𝑑 ∨ 𝑑 = 𝑔)))
119	118	imp 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑎 = 𝑔) → (𝑔𝑅𝑑 ∨ 𝑑 = 𝑔))
120		ordir 1024	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑑𝑅𝑔 ∧ 𝑔𝑅𝑑) ∨ 𝑑 = 𝑔) ↔ ((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑔𝑅𝑑 ∨ 𝑑 = 𝑔)))
121	112, 119, 120	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑎 = 𝑔) → ((𝑑𝑅𝑔 ∧ 𝑔𝑅𝑑) ∨ 𝑑 = 𝑔))
122	34	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → 𝑅 Po 𝐴)
123	36	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → 𝑑 ∈ 𝐴)
124	37	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → 𝑔 ∈ 𝐴)
125		po2nr 5573	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Po 𝐴 ∧ (𝑑 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → ¬ (𝑑𝑅𝑔 ∧ 𝑔𝑅𝑑))
126	122, 123, 124, 125	syl12anc 850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ¬ (𝑑𝑅𝑔 ∧ 𝑔𝑅𝑑))
127	126	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑎 = 𝑔) → ¬ (𝑑𝑅𝑔 ∧ 𝑔𝑅𝑑))
128	121, 127	orcnd 892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑎 = 𝑔) → 𝑑 = 𝑔)
129	128	ex 418	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑎 = 𝑔 → 𝑑 = 𝑔))
130	129	necon3d 2977	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑑 ≠ 𝑔 → 𝑎 ≠ 𝑔))
131	82	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑏 = ℎ) → (𝑒𝑆ℎ ∨ 𝑒 = ℎ))
132		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 = ℎ → (𝑏𝑆𝑒 ↔ ℎ𝑆𝑒))
133		equequ1 2058	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 = ℎ → (𝑏 = 𝑒 ↔ ℎ = 𝑒))
134		equcom 2051	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = 𝑒 ↔ 𝑒 = ℎ)
135	133, 134	bitrdi 290	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 = ℎ → (𝑏 = 𝑒 ↔ 𝑒 = ℎ))
136	132, 135	orbi12d 932	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = ℎ → ((𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ↔ (ℎ𝑆𝑒 ∨ 𝑒 = ℎ)))
137	72, 136	syl5ibcom 248	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑏 = ℎ → (ℎ𝑆𝑒 ∨ 𝑒 = ℎ)))
138	137	imp 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑏 = ℎ) → (ℎ𝑆𝑒 ∨ 𝑒 = ℎ))
139		ordir 1024	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑒𝑆ℎ ∧ ℎ𝑆𝑒) ∨ 𝑒 = ℎ) ↔ ((𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (ℎ𝑆𝑒 ∨ 𝑒 = ℎ)))
140	131, 138, 139	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑏 = ℎ) → ((𝑒𝑆ℎ ∧ ℎ𝑆𝑒) ∨ 𝑒 = ℎ))
141	59	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → 𝑆 Po 𝐵)
142	61	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → 𝑒 ∈ 𝐵)
143	62	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ℎ ∈ 𝐵)
144		po2nr 5573	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 Po 𝐵 ∧ (𝑒 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ¬ (𝑒𝑆ℎ ∧ ℎ𝑆𝑒))
145	141, 142, 143, 144	syl12anc 850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ¬ (𝑒𝑆ℎ ∧ ℎ𝑆𝑒))
146	145	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑏 = ℎ) → ¬ (𝑒𝑆ℎ ∧ ℎ𝑆𝑒))
147	140, 146	orcnd 892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑏 = ℎ) → 𝑒 = ℎ)
148	147	ex 418	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑏 = ℎ → 𝑒 = ℎ))
149	148	necon3d 2977	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑒 ≠ ℎ → 𝑏 ≠ ℎ))
150	107	adantr 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑐 = 𝑖) → (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖))
151		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = 𝑖 → (𝑐𝑇𝑓 ↔ 𝑖𝑇𝑓))
152		equequ1 2058	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 = 𝑖 → (𝑐 = 𝑓 ↔ 𝑖 = 𝑓))
153		equcom 2051	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = 𝑓 ↔ 𝑓 = 𝑖)
154	152, 153	bitrdi 290	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = 𝑖 → (𝑐 = 𝑓 ↔ 𝑓 = 𝑖))
155	151, 154	orbi12d 932	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑖 → ((𝑐𝑇𝑓 ∨ 𝑐 = 𝑓) ↔ (𝑖𝑇𝑓 ∨ 𝑓 = 𝑖)))
156	97, 155	syl5ibcom 248	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑐 = 𝑖 → (𝑖𝑇𝑓 ∨ 𝑓 = 𝑖)))
157	156	imp 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑐 = 𝑖) → (𝑖𝑇𝑓 ∨ 𝑓 = 𝑖))
158		ordir 1024	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑓𝑇𝑖 ∧ 𝑖𝑇𝑓) ∨ 𝑓 = 𝑖) ↔ ((𝑓𝑇𝑖 ∨ 𝑓 = 𝑖) ∧ (𝑖𝑇𝑓 ∨ 𝑓 = 𝑖)))
159	150, 157, 158	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑐 = 𝑖) → ((𝑓𝑇𝑖 ∧ 𝑖𝑇𝑓) ∨ 𝑓 = 𝑖))
160	84	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → 𝑇 Po 𝐶)
161	86	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → 𝑓 ∈ 𝐶)
162	87	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → 𝑖 ∈ 𝐶)
163		po2nr 5573	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑇 Po 𝐶 ∧ (𝑓 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶)) → ¬ (𝑓𝑇𝑖 ∧ 𝑖𝑇𝑓))
164	160, 161, 162, 163	syl12anc 850	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ¬ (𝑓𝑇𝑖 ∧ 𝑖𝑇𝑓))
165	164	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑐 = 𝑖) → ¬ (𝑓𝑇𝑖 ∧ 𝑖𝑇𝑓))
166	159, 165	orcnd 892	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑐 = 𝑖) → 𝑓 = 𝑖)
167	166	ex 418	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑐 = 𝑖 → 𝑓 = 𝑖))
168	167	necon3d 2977	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑓 ≠ 𝑖 → 𝑐 ≠ 𝑖))
169	130, 149, 168	3orim123d 1472	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ((𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖) → (𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖)))
170	111, 169	mpd 16	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖))
171	109, 170	jca 521	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (((𝑎𝑅𝑔 ∨ 𝑎 = 𝑔) ∧ (𝑏𝑆ℎ ∨ 𝑏 = ℎ) ∧ (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)) ∧ (𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖)))
172	32, 33, 171	3jca 1146	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑎𝑅𝑔 ∨ 𝑎 = 𝑔) ∧ (𝑏𝑆ℎ ∨ 𝑏 = ℎ) ∧ (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)) ∧ (𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖))))
173	172	ex 418	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑎𝑅𝑔 ∨ 𝑎 = 𝑔) ∧ (𝑏𝑆ℎ ∨ 𝑏 = ℎ) ∧ (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)) ∧ (𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖)))))
174		breq12 5108	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩) → (𝑝𝑈𝑞 ↔ ⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩))
175	174	3adant3 1150	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (𝑝𝑈𝑞 ↔ ⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩))
176	11	xpord3lem 8159	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))
177	175, 176	bitrdi 290	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (𝑝𝑈𝑞 ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)))))
178		breq12 5108	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (𝑞𝑈𝑟 ↔ ⟨𝑑, 𝑒, 𝑓⟩𝑈⟨𝑔, ℎ, 𝑖⟩))
179	178	3adant1 1148	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (𝑞𝑈𝑟 ↔ ⟨𝑑, 𝑒, 𝑓⟩𝑈⟨𝑔, ℎ, 𝑖⟩))
180	11	xpord3lem 8159	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑑, 𝑒, 𝑓⟩𝑈⟨𝑔, ℎ, 𝑖⟩ ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))
181	179, 180	bitrdi 290	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (𝑞𝑈𝑟 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))))
182	177, 181	anbi12d 644	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) ↔ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))))
183		an6 1474	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) ↔ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))))
184	182, 183	bitrdi 290	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) ↔ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))))
185		breq12 5108	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (𝑝𝑈𝑟 ↔ ⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑔, ℎ, 𝑖⟩))
186	185	3adant2 1149	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (𝑝𝑈𝑟 ↔ ⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑔, ℎ, 𝑖⟩))
187	11	xpord3lem 8159	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑔, ℎ, 𝑖⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑎𝑅𝑔 ∨ 𝑎 = 𝑔) ∧ (𝑏𝑆ℎ ∨ 𝑏 = ℎ) ∧ (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)) ∧ (𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖))))
188	186, 187	bitrdi 290	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (𝑝𝑈𝑟 ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑎𝑅𝑔 ∨ 𝑎 = 𝑔) ∧ (𝑏𝑆ℎ ∨ 𝑏 = ℎ) ∧ (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)) ∧ (𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖)))))
189	184, 188	imbi12d 347	. . . . . . . . . . . . . 14 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑎𝑅𝑔 ∨ 𝑎 = 𝑔) ∧ (𝑏𝑆ℎ ∨ 𝑏 = ℎ) ∧ (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)) ∧ (𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖))))))
190	173, 189	syl5ibrcom 250	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
191	190	rexlimdvw 3169	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
192	191	rexlimdvw 3169	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
193	192	rexlimdvw 3169	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
194	193	rexlimdvw 3169	. . . . . . . . 9 ⊢ (𝜑 → (∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
195	194	rexlimdvw 3169	. . . . . . . 8 ⊢ (𝜑 → (∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
196	195	rexlimdvw 3169	. . . . . . 7 ⊢ (𝜑 → (∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
197	196	rexlimdvw 3169	. . . . . 6 ⊢ (𝜑 → (∃𝑔 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
198	197	rexlimdvw 3169	. . . . 5 ⊢ (𝜑 → (∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
199	198	rexlimdvw 3169	. . . 4 ⊢ (𝜑 → (∃𝑎 ∈ 𝐴 ∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
200	31, 199	biimtrid 245	. . 3 ⊢ (𝜑 → ((𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑟 ∈ ((𝐴 × 𝐵) × 𝐶)) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
201	200	imp 412	. 2 ⊢ ((𝜑 ∧ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑟 ∈ ((𝐴 × 𝐵) × 𝐶))) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟))
202	19, 201	ispod 5568	1 ⊢ (𝜑 → 𝑈 Po ((𝐴 × 𝐵) × 𝐶))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∨ w3o 1102 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ≠ wne 2956 ∃wrex 3087 ⟨cotp 4592 class class class wbr 5103 {copab 5167 Po wpo 5557 × cxp 5649 ‘cfv 6537 1^st c1st 7997 2^nd c2nd 7998

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pr 5391 ax-un 7749

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-rab 3414 df-v 3453 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-sn 4585 df-pr 4587 df-op 4591 df-ot 4593 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5546 df-po 5559 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-iota 6493 df-fun 6539 df-fv 6545 df-1st 7999 df-2nd 8000

This theorem is used by: xpord3inddlem 8164

W3C validator