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 8175

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 8060	. . . 4 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩)
2		neirr 2949	. . . . . . . . . . 11 ⊢ ¬ 𝑎 ≠ 𝑎
3		neirr 2949	. . . . . . . . . . 11 ⊢ ¬ 𝑏 ≠ 𝑏
4		neirr 2949	. . . . . . . . . . 11 ⊢ ¬ 𝑐 ≠ 𝑐
5	2, 3, 4	3pm3.2ni 1490	. . . . . . . . . 10 ⊢ ¬ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)
6	5	intnan 486	. . . . . . . . 9 ⊢ ¬ (((𝑎𝑅𝑎 ∨ 𝑎 = 𝑎) ∧ (𝑏𝑆𝑏 ∨ 𝑏 = 𝑏) ∧ (𝑐𝑇𝑐 ∨ 𝑐 = 𝑐)) ∧ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))
7		simp3 1139	. . . . . . . . 9 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑎𝑅𝑎 ∨ 𝑎 = 𝑎) ∧ (𝑏𝑆𝑏 ∨ 𝑏 = 𝑏) ∧ (𝑐𝑇𝑐 ∨ 𝑐 = 𝑐)) ∧ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))) → (((𝑎𝑅𝑎 ∨ 𝑎 = 𝑎) ∧ (𝑏𝑆𝑏 ∨ 𝑏 = 𝑏) ∧ (𝑐𝑇𝑐 ∨ 𝑐 = 𝑐)) ∧ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))
8	6, 7	mto 197	. . . . . . . 8 ⊢ ¬ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑎𝑅𝑎 ∨ 𝑎 = 𝑎) ∧ (𝑏𝑆𝑏 ∨ 𝑏 = 𝑏) ∧ (𝑐𝑇𝑐 ∨ 𝑐 = 𝑐)) ∧ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))
9		breq12 5148	. . . . . . . . . 10 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩) → (𝑝𝑈𝑝 ↔ ⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑎, 𝑏, 𝑐⟩))
10	9	anidms 566	. . . . . . . . 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 8174	. . . . . . . . 9 ⊢ (⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑎, 𝑏, 𝑐⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑎𝑅𝑎 ∨ 𝑎 = 𝑎) ∧ (𝑏𝑆𝑏 ∨ 𝑏 = 𝑏) ∧ (𝑐𝑇𝑐 ∨ 𝑐 = 𝑐)) ∧ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐))))
13	10, 12	bitrdi 287	. . . . . . . 8 ⊢ (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → (𝑝𝑈𝑝 ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (((𝑎𝑅𝑎 ∨ 𝑎 = 𝑎) ∧ (𝑏𝑆𝑏 ∨ 𝑏 = 𝑏) ∧ (𝑐𝑇𝑐 ∨ 𝑐 = 𝑐)) ∧ (𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐)))))
14	8, 13	mtbiri 327	. . . . . . 7 ⊢ (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → ¬ 𝑝𝑈𝑝)
15	14	rexlimivw 3151	. . . . . 6 ⊢ (∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → ¬ 𝑝𝑈𝑝)
16	15	rexlimivw 3151	. . . . 5 ⊢ (∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → ¬ 𝑝𝑈𝑝)
17	16	rexlimivw 3151	. . . 4 ⊢ (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ → ¬ 𝑝𝑈𝑝)
18	1, 17	sylbi 217	. . 3 ⊢ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) → ¬ 𝑝𝑈𝑝)
19	18	adantl 481	. 2 ⊢ ((𝜑 ∧ 𝑝 ∈ ((𝐴 × 𝐵) × 𝐶)) → ¬ 𝑝𝑈𝑝)
20		3reeanv 3230	. . . . 5 ⊢ (∃𝑎 ∈ 𝐴 ∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 (∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) ↔ (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
21		3reeanv 3230	. . . . . . . . . 10 ⊢ (∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) ↔ (∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
22	21	rexbii 3094	. . . . . . . . 9 ⊢ (∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) ↔ ∃ℎ ∈ 𝐵 (∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
23	22	2rexbii 3129	. . . . . . . 8 ⊢ (∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) ↔ ∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 (∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
24		3reeanv 3230	. . . . . . . 8 ⊢ (∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 (∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) ↔ (∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
25	23, 24	bitri 275	. . . . . . 7 ⊢ (∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) ↔ (∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
26	25	rexbii 3094	. . . . . 6 ⊢ (∃𝑔 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) ↔ ∃𝑔 ∈ 𝐴 (∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
27	26	2rexbii 3129	. . . . 5 ⊢ (∃𝑎 ∈ 𝐴 ∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) ↔ ∃𝑎 ∈ 𝐴 ∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 (∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
28		el2xptp 8060	. . . . . 6 ⊢ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩)
29		el2xptp 8060	. . . . . 6 ⊢ (𝑟 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩)
30	1, 28, 29	3anbi123i 1156	. . . . 5 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑟 ∈ ((𝐴 × 𝐵) × 𝐶)) ↔ (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑐 ∈ 𝐶 𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ ∃𝑑 ∈ 𝐴 ∃𝑒 ∈ 𝐵 ∃𝑓 ∈ 𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ ∃𝑔 ∈ 𝐴 ∃ℎ ∈ 𝐵 ∃𝑖 ∈ 𝐶 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
31	20, 27, 30	3bitr4ri 304	. . . 4 ⊢ ((𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑟 ∈ ((𝐴 × 𝐵) × 𝐶)) ↔ ∃𝑎 ∈ 𝐴 ∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩))
32		simpr1l 1231	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶))
33		simpr2r 1234	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶))
34		poxp3.1	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑅 Po 𝐴)
35		simp1l1 1267	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → 𝑎 ∈ 𝐴)
36		simp2l1 1273	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → 𝑑 ∈ 𝐴)
37		simp2r1 1276	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → 𝑔 ∈ 𝐴)
38	35, 36, 37	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑎 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴))
39		potr 5605	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → ((𝑎𝑅𝑑 ∧ 𝑑𝑅𝑔) → 𝑎𝑅𝑔))
40	34, 38, 39	syl2an 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ((𝑎𝑅𝑑 ∧ 𝑑𝑅𝑔) → 𝑎𝑅𝑔))
41	40	expd 415	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑎𝑅𝑑 → (𝑑𝑅𝑔 → 𝑎𝑅𝑔)))
42		breq1 5146	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = 𝑑 → (𝑎𝑅𝑔 ↔ 𝑑𝑅𝑔))
43	42	biimprd 248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = 𝑑 → (𝑑𝑅𝑔 → 𝑎𝑅𝑔))
44	43	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑎 = 𝑑 → (𝑑𝑅𝑔 → 𝑎𝑅𝑔)))
45		simpll1 1213	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑎𝑅𝑑 ∨ 𝑎 = 𝑑))
46	45	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑎𝑅𝑑 ∨ 𝑎 = 𝑑))
47	46	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑎𝑅𝑑 ∨ 𝑎 = 𝑑))
48	41, 44, 47	mpjaod 861	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑑𝑅𝑔 → 𝑎𝑅𝑔))
49		orc 868	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎𝑅𝑔 → (𝑎𝑅𝑔 ∨ 𝑎 = 𝑔))
50	48, 49	syl6 35	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑑𝑅𝑔 → (𝑎𝑅𝑔 ∨ 𝑎 = 𝑔)))
51		breq2 5147	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑔 → (𝑎𝑅𝑑 ↔ 𝑎𝑅𝑔))
52		equequ2 2025	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 = 𝑔 → (𝑎 = 𝑑 ↔ 𝑎 = 𝑔))
53	51, 52	orbi12d 919	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 = 𝑔 → ((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ↔ (𝑎𝑅𝑔 ∨ 𝑎 = 𝑔)))
54	47, 53	syl5ibcom 245	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑑 = 𝑔 → (𝑎𝑅𝑔 ∨ 𝑎 = 𝑔)))
55		simprl1 1219	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑑𝑅𝑔 ∨ 𝑑 = 𝑔))
56	55	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑑𝑅𝑔 ∨ 𝑑 = 𝑔))
57	56	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑑𝑅𝑔 ∨ 𝑑 = 𝑔))
58	50, 54, 57	mpjaod 861	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑎𝑅𝑔 ∨ 𝑎 = 𝑔))
59		poxp3.2	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑆 Po 𝐵)
60		simp1l2 1268	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → 𝑏 ∈ 𝐵)
61		simp2l2 1274	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → 𝑒 ∈ 𝐵)
62		simp2r2 1277	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → ℎ ∈ 𝐵)
63	60, 61, 62	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑏 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ∧ ℎ ∈ 𝐵))
64		potr 5605	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑒 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ((𝑏𝑆𝑒 ∧ 𝑒𝑆ℎ) → 𝑏𝑆ℎ))
65	59, 63, 64	syl2an 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ((𝑏𝑆𝑒 ∧ 𝑒𝑆ℎ) → 𝑏𝑆ℎ))
66	65	expd 415	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑏𝑆𝑒 → (𝑒𝑆ℎ → 𝑏𝑆ℎ)))
67		breq1 5146	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑏 = 𝑒 → (𝑏𝑆ℎ ↔ 𝑒𝑆ℎ))
68	67	biimprd 248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑏 = 𝑒 → (𝑒𝑆ℎ → 𝑏𝑆ℎ))
69	68	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑏 = 𝑒 → (𝑒𝑆ℎ → 𝑏𝑆ℎ)))
70		simpll2 1214	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒))
71	70	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒))
72	71	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒))
73	66, 69, 72	mpjaod 861	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑒𝑆ℎ → 𝑏𝑆ℎ))
74		orc 868	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏𝑆ℎ → (𝑏𝑆ℎ ∨ 𝑏 = ℎ))
75	73, 74	syl6 35	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑒𝑆ℎ → (𝑏𝑆ℎ ∨ 𝑏 = ℎ)))
76		breq2 5147	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = ℎ → (𝑏𝑆𝑒 ↔ 𝑏𝑆ℎ))
77		equequ2 2025	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = ℎ → (𝑏 = 𝑒 ↔ 𝑏 = ℎ))
78	76, 77	orbi12d 919	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑒 = ℎ → ((𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ↔ (𝑏𝑆ℎ ∨ 𝑏 = ℎ)))
79	72, 78	syl5ibcom 245	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑒 = ℎ → (𝑏𝑆ℎ ∨ 𝑏 = ℎ)))
80		simprl2 1220	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑒𝑆ℎ ∨ 𝑒 = ℎ))
81	80	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑒𝑆ℎ ∨ 𝑒 = ℎ))
82	81	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑒𝑆ℎ ∨ 𝑒 = ℎ))
83	75, 79, 82	mpjaod 861	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑏𝑆ℎ ∨ 𝑏 = ℎ))
84		poxp3.3	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 𝑇 Po 𝐶)
85		simp1l3 1269	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → 𝑐 ∈ 𝐶)
86		simp2l3 1275	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → 𝑓 ∈ 𝐶)
87		simp2r3 1278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → 𝑖 ∈ 𝐶)
88	85, 86, 87	3jca 1129	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑐 ∈ 𝐶 ∧ 𝑓 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶))
89		potr 5605	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑇 Po 𝐶 ∧ (𝑐 ∈ 𝐶 ∧ 𝑓 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶)) → ((𝑐𝑇𝑓 ∧ 𝑓𝑇𝑖) → 𝑐𝑇𝑖))
90	84, 88, 89	syl2an 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ((𝑐𝑇𝑓 ∧ 𝑓𝑇𝑖) → 𝑐𝑇𝑖))
91	90	expd 415	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑐𝑇𝑓 → (𝑓𝑇𝑖 → 𝑐𝑇𝑖)))
92		breq1 5146	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = 𝑓 → (𝑐𝑇𝑖 ↔ 𝑓𝑇𝑖))
93	92	biimprd 248	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 = 𝑓 → (𝑓𝑇𝑖 → 𝑐𝑇𝑖))
94	93	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑐 = 𝑓 → (𝑓𝑇𝑖 → 𝑐𝑇𝑖)))
95		simpll3 1215	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓))
96	95	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓))
97	96	adantl 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓))
98	91, 94, 97	mpjaod 861	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑓𝑇𝑖 → 𝑐𝑇𝑖))
99		orc 868	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐𝑇𝑖 → (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖))
100	98, 99	syl6 35	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑓𝑇𝑖 → (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)))
101		breq2 5147	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑖 → (𝑐𝑇𝑓 ↔ 𝑐𝑇𝑖))
102		equequ2 2025	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑓 = 𝑖 → (𝑐 = 𝑓 ↔ 𝑐 = 𝑖))
103	101, 102	orbi12d 919	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑓 = 𝑖 → ((𝑐𝑇𝑓 ∨ 𝑐 = 𝑓) ↔ (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)))
104	97, 103	syl5ibcom 245	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑓 = 𝑖 → (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)))
105		simprl3 1221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))) → (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖))
106	105	3ad2ant3 1136	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖))
107	106	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖))
108	100, 104, 107	mpjaod 861	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖))
109	58, 83, 108	3jca 1129	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ((𝑎𝑅𝑔 ∨ 𝑎 = 𝑔) ∧ (𝑏𝑆ℎ ∨ 𝑏 = ℎ) ∧ (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)))
110		simp3rr 1248	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))
111	110	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))
112	57	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑎 = 𝑔) → (𝑑𝑅𝑔 ∨ 𝑑 = 𝑔))
113		breq1 5146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑔 → (𝑎𝑅𝑑 ↔ 𝑔𝑅𝑑))
114		equequ1 2024	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = 𝑔 → (𝑎 = 𝑑 ↔ 𝑔 = 𝑑))
115		equcom 2017	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑔 = 𝑑 ↔ 𝑑 = 𝑔)
116	114, 115	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = 𝑔 → (𝑎 = 𝑑 ↔ 𝑑 = 𝑔))
117	113, 116	orbi12d 919	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = 𝑔 → ((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ↔ (𝑔𝑅𝑑 ∨ 𝑑 = 𝑔)))
118	47, 117	syl5ibcom 245	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑎 = 𝑔 → (𝑔𝑅𝑑 ∨ 𝑑 = 𝑔)))
119	118	imp 406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑎 = 𝑔) → (𝑔𝑅𝑑 ∨ 𝑑 = 𝑔))
120		ordir 1009	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑑𝑅𝑔 ∧ 𝑔𝑅𝑑) ∨ 𝑑 = 𝑔) ↔ ((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑔𝑅𝑑 ∨ 𝑑 = 𝑔)))
121	112, 119, 120	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑎 = 𝑔) → ((𝑑𝑅𝑔 ∧ 𝑔𝑅𝑑) ∨ 𝑑 = 𝑔))
122	34	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → 𝑅 Po 𝐴)
123	36	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → 𝑑 ∈ 𝐴)
124	37	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → 𝑔 ∈ 𝐴)
125		po2nr 5606	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Po 𝐴 ∧ (𝑑 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴)) → ¬ (𝑑𝑅𝑔 ∧ 𝑔𝑅𝑑))
126	122, 123, 124, 125	syl12anc 837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ¬ (𝑑𝑅𝑔 ∧ 𝑔𝑅𝑑))
127	126	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑎 = 𝑔) → ¬ (𝑑𝑅𝑔 ∧ 𝑔𝑅𝑑))
128	121, 127	orcnd 879	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑎 = 𝑔) → 𝑑 = 𝑔)
129	128	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑎 = 𝑔 → 𝑑 = 𝑔))
130	129	necon3d 2961	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑑 ≠ 𝑔 → 𝑎 ≠ 𝑔))
131	82	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑏 = ℎ) → (𝑒𝑆ℎ ∨ 𝑒 = ℎ))
132		breq1 5146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 = ℎ → (𝑏𝑆𝑒 ↔ ℎ𝑆𝑒))
133		equequ1 2024	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑏 = ℎ → (𝑏 = 𝑒 ↔ ℎ = 𝑒))
134		equcom 2017	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ = 𝑒 ↔ 𝑒 = ℎ)
135	133, 134	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑏 = ℎ → (𝑏 = 𝑒 ↔ 𝑒 = ℎ))
136	132, 135	orbi12d 919	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 = ℎ → ((𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ↔ (ℎ𝑆𝑒 ∨ 𝑒 = ℎ)))
137	72, 136	syl5ibcom 245	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑏 = ℎ → (ℎ𝑆𝑒 ∨ 𝑒 = ℎ)))
138	137	imp 406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑏 = ℎ) → (ℎ𝑆𝑒 ∨ 𝑒 = ℎ))
139		ordir 1009	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑒𝑆ℎ ∧ ℎ𝑆𝑒) ∨ 𝑒 = ℎ) ↔ ((𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (ℎ𝑆𝑒 ∨ 𝑒 = ℎ)))
140	131, 138, 139	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑏 = ℎ) → ((𝑒𝑆ℎ ∧ ℎ𝑆𝑒) ∨ 𝑒 = ℎ))
141	59	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → 𝑆 Po 𝐵)
142	61	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → 𝑒 ∈ 𝐵)
143	62	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ℎ ∈ 𝐵)
144		po2nr 5606	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑆 Po 𝐵 ∧ (𝑒 ∈ 𝐵 ∧ ℎ ∈ 𝐵)) → ¬ (𝑒𝑆ℎ ∧ ℎ𝑆𝑒))
145	141, 142, 143, 144	syl12anc 837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ¬ (𝑒𝑆ℎ ∧ ℎ𝑆𝑒))
146	145	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑏 = ℎ) → ¬ (𝑒𝑆ℎ ∧ ℎ𝑆𝑒))
147	140, 146	orcnd 879	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑏 = ℎ) → 𝑒 = ℎ)
148	147	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑏 = ℎ → 𝑒 = ℎ))
149	148	necon3d 2961	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑒 ≠ ℎ → 𝑏 ≠ ℎ))
150	107	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑐 = 𝑖) → (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖))
151		breq1 5146	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = 𝑖 → (𝑐𝑇𝑓 ↔ 𝑖𝑇𝑓))
152		equequ1 2024	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 = 𝑖 → (𝑐 = 𝑓 ↔ 𝑖 = 𝑓))
153		equcom 2017	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 = 𝑓 ↔ 𝑓 = 𝑖)
154	152, 153	bitrdi 287	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = 𝑖 → (𝑐 = 𝑓 ↔ 𝑓 = 𝑖))
155	151, 154	orbi12d 919	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑖 → ((𝑐𝑇𝑓 ∨ 𝑐 = 𝑓) ↔ (𝑖𝑇𝑓 ∨ 𝑓 = 𝑖)))
156	97, 155	syl5ibcom 245	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑐 = 𝑖 → (𝑖𝑇𝑓 ∨ 𝑓 = 𝑖)))
157	156	imp 406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑐 = 𝑖) → (𝑖𝑇𝑓 ∨ 𝑓 = 𝑖))
158		ordir 1009	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑓𝑇𝑖 ∧ 𝑖𝑇𝑓) ∨ 𝑓 = 𝑖) ↔ ((𝑓𝑇𝑖 ∨ 𝑓 = 𝑖) ∧ (𝑖𝑇𝑓 ∨ 𝑓 = 𝑖)))
159	150, 157, 158	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑐 = 𝑖) → ((𝑓𝑇𝑖 ∧ 𝑖𝑇𝑓) ∨ 𝑓 = 𝑖))
160	84	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → 𝑇 Po 𝐶)
161	86	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → 𝑓 ∈ 𝐶)
162	87	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → 𝑖 ∈ 𝐶)
163		po2nr 5606	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑇 Po 𝐶 ∧ (𝑓 ∈ 𝐶 ∧ 𝑖 ∈ 𝐶)) → ¬ (𝑓𝑇𝑖 ∧ 𝑖𝑇𝑓))
164	160, 161, 162, 163	syl12anc 837	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ¬ (𝑓𝑇𝑖 ∧ 𝑖𝑇𝑓))
165	164	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑐 = 𝑖) → ¬ (𝑓𝑇𝑖 ∧ 𝑖𝑇𝑓))
166	159, 165	orcnd 879	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) ∧ 𝑐 = 𝑖) → 𝑓 = 𝑖)
167	166	ex 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑐 = 𝑖 → 𝑓 = 𝑖))
168	167	necon3d 2961	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑓 ≠ 𝑖 → 𝑐 ≠ 𝑖))
169	130, 149, 168	3orim123d 1446	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ((𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖) → (𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖)))
170	111, 169	mpd 15	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖))
171	109, 170	jca 511	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → (((𝑎𝑅𝑔 ∨ 𝑎 = 𝑔) ∧ (𝑏𝑆ℎ ∨ 𝑏 = ℎ) ∧ (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)) ∧ (𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖)))
172	32, 33, 171	3jca 1129	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑎𝑅𝑔 ∨ 𝑎 = 𝑔) ∧ (𝑏𝑆ℎ ∨ 𝑏 = ℎ) ∧ (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)) ∧ (𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖))))
173	172	ex 412	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑎𝑅𝑔 ∨ 𝑎 = 𝑔) ∧ (𝑏𝑆ℎ ∨ 𝑏 = ℎ) ∧ (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)) ∧ (𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖)))))
174		breq12 5148	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩) → (𝑝𝑈𝑞 ↔ ⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩))
175	174	3adant3 1133	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (𝑝𝑈𝑞 ↔ ⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩))
176	11	xpord3lem 8174	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑑, 𝑒, 𝑓⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))))
177	175, 176	bitrdi 287	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (𝑝𝑈𝑞 ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)))))
178		breq12 5148	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (𝑞𝑈𝑟 ↔ ⟨𝑑, 𝑒, 𝑓⟩𝑈⟨𝑔, ℎ, 𝑖⟩))
179	178	3adant1 1131	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (𝑞𝑈𝑟 ↔ ⟨𝑑, 𝑒, 𝑓⟩𝑈⟨𝑔, ℎ, 𝑖⟩))
180	11	xpord3lem 8174	. . . . . . . . . . . . . . . . . 18 ⊢ (⟨𝑑, 𝑒, 𝑓⟩𝑈⟨𝑔, ℎ, 𝑖⟩ ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))
181	179, 180	bitrdi 287	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (𝑞𝑈𝑟 ↔ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))))
182	177, 181	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) ↔ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))))
183		an6 1447	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓))) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) ↔ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))))
184	182, 183	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) ↔ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖))))))
185		breq12 5148	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (𝑝𝑈𝑟 ↔ ⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑔, ℎ, 𝑖⟩))
186	185	3adant2 1132	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (𝑝𝑈𝑟 ↔ ⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑔, ℎ, 𝑖⟩))
187	11	xpord3lem 8174	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑎, 𝑏, 𝑐⟩𝑈⟨𝑔, ℎ, 𝑖⟩ ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑎𝑅𝑔 ∨ 𝑎 = 𝑔) ∧ (𝑏𝑆ℎ ∨ 𝑏 = ℎ) ∧ (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)) ∧ (𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖))))
188	186, 187	bitrdi 287	. . . . . . . . . . . . . . 15 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (𝑝𝑈𝑟 ↔ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑎𝑅𝑔 ∨ 𝑎 = 𝑔) ∧ (𝑏𝑆ℎ ∨ 𝑏 = ℎ) ∧ (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)) ∧ (𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖)))))
189	184, 188	imbi12d 344	. . . . . . . . . . . . . 14 ⊢ ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → (((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶)) ∧ ((𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶)) ∧ ((((𝑎𝑅𝑑 ∨ 𝑎 = 𝑑) ∧ (𝑏𝑆𝑒 ∨ 𝑏 = 𝑒) ∧ (𝑐𝑇𝑓 ∨ 𝑐 = 𝑓)) ∧ (𝑎 ≠ 𝑑 ∨ 𝑏 ≠ 𝑒 ∨ 𝑐 ≠ 𝑓)) ∧ (((𝑑𝑅𝑔 ∨ 𝑑 = 𝑔) ∧ (𝑒𝑆ℎ ∨ 𝑒 = ℎ) ∧ (𝑓𝑇𝑖 ∨ 𝑓 = 𝑖)) ∧ (𝑑 ≠ 𝑔 ∨ 𝑒 ≠ ℎ ∨ 𝑓 ≠ 𝑖)))) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶) ∧ (𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐵 ∧ 𝑖 ∈ 𝐶) ∧ (((𝑎𝑅𝑔 ∨ 𝑎 = 𝑔) ∧ (𝑏𝑆ℎ ∨ 𝑏 = ℎ) ∧ (𝑐𝑇𝑖 ∨ 𝑐 = 𝑖)) ∧ (𝑎 ≠ 𝑔 ∨ 𝑏 ≠ ℎ ∨ 𝑐 ≠ 𝑖))))))
190	173, 189	syl5ibrcom 247	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
191	190	rexlimdvw 3160	. . . . . . . . . . . 12 ⊢ (𝜑 → (∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
192	191	rexlimdvw 3160	. . . . . . . . . . 11 ⊢ (𝜑 → (∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
193	192	rexlimdvw 3160	. . . . . . . . . 10 ⊢ (𝜑 → (∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
194	193	rexlimdvw 3160	. . . . . . . . 9 ⊢ (𝜑 → (∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
195	194	rexlimdvw 3160	. . . . . . . 8 ⊢ (𝜑 → (∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
196	195	rexlimdvw 3160	. . . . . . 7 ⊢ (𝜑 → (∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
197	196	rexlimdvw 3160	. . . . . 6 ⊢ (𝜑 → (∃𝑔 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
198	197	rexlimdvw 3160	. . . . 5 ⊢ (𝜑 → (∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
199	198	rexlimdvw 3160	. . . 4 ⊢ (𝜑 → (∃𝑎 ∈ 𝐴 ∃𝑑 ∈ 𝐴 ∃𝑔 ∈ 𝐴 ∃𝑏 ∈ 𝐵 ∃𝑒 ∈ 𝐵 ∃ℎ ∈ 𝐵 ∃𝑐 ∈ 𝐶 ∃𝑓 ∈ 𝐶 ∃𝑖 ∈ 𝐶 (𝑝 = ⟨𝑎, 𝑏, 𝑐⟩ ∧ 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ ∧ 𝑟 = ⟨𝑔, ℎ, 𝑖⟩) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
200	31, 199	biimtrid 242	. . 3 ⊢ (𝜑 → ((𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑟 ∈ ((𝐴 × 𝐵) × 𝐶)) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟)))
201	200	imp 406	. 2 ⊢ ((𝜑 ∧ (𝑝 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑟 ∈ ((𝐴 × 𝐵) × 𝐶))) → ((𝑝𝑈𝑞 ∧ 𝑞𝑈𝑟) → 𝑝𝑈𝑟))
202	19, 201	ispod 5601	1 ⊢ (𝜑 → 𝑈 Po ((𝐴 × 𝐵) × 𝐶))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 ∨ w3o 1086 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∃wrex 3070 ⟨cotp 4634 class class class wbr 5143 {copab 5205 Po wpo 5590 × cxp 5683 ‘cfv 6561 1^st c1st 8012 2^nd c2nd 8013

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 ax-un 7755

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-ot 4635 df-uni 4908 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-po 5592 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-iota 6514 df-fun 6563 df-fv 6569 df-1st 8014 df-2nd 8015

This theorem is referenced by: xpord3inddlem 8179

W3C validator