poxp2 - Metamath Proof Explorer

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

Theorem poxp2 8138

Description: Another way of partially ordering a Cartesian product of two classes. (Contributed by Scott Fenton, 19-Aug-2024.)

**Hypotheses**
Ref	Expression
xpord2.1	⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥)𝑆(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}
poxp2.1	⊢ (𝜑 → 𝑅 Po 𝐴)
poxp2.2	⊢ (𝜑 → 𝑆 Po 𝐵)

**Assertion**
Ref	Expression
poxp2	⊢ (𝜑 → 𝑇 Po (𝐴 × 𝐵))

Distinct variable groups: 𝑥,𝐴,𝑦 𝑥,𝐵,𝑦 𝑥,𝑅,𝑦 𝑥,𝑆,𝑦 Allowed substitution hints: 𝜑(𝑥,𝑦) 𝑇(𝑥,𝑦)

Proof of Theorem poxp2 Dummy variables 𝑎 𝑏 𝑐 𝑝 𝑞 𝑟 𝑠 𝑡 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp2 5686	. . . 4 ⊢ (𝑎 ∈ (𝐴 × 𝐵) ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩)
2		equid 2039	. . . . . . . . . . . 12 ⊢ 𝑝 = 𝑝
3		equid 2039	. . . . . . . . . . . 12 ⊢ 𝑞 = 𝑞
4	2, 3	pm3.2i 475	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑝 ∧ 𝑞 = 𝑞)
5		neorian 3059	. . . . . . . . . . . 12 ⊢ ((𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞) ↔ ¬ (𝑝 = 𝑝 ∧ 𝑞 = 𝑞))
6	5	con2bii 360	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑝 ∧ 𝑞 = 𝑞) ↔ ¬ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))
7	4, 6	mpbi 233	. . . . . . . . . 10 ⊢ ¬ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)
8		simp3 1154	. . . . . . . . . 10 ⊢ (((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)) → (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))
9	7, 8	mto 200	. . . . . . . . 9 ⊢ ¬ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))
10		simp3 1154	. . . . . . . . 9 ⊢ (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))) → ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)))
11	9, 10	mto 200	. . . . . . . 8 ⊢ ¬ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)))
12		xpord2.1	. . . . . . . . 9 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥)𝑆(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}
13	12	xpord2lem 8137	. . . . . . . 8 ⊢ (⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩ ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))))
14	11, 13	mtbir 326	. . . . . . 7 ⊢ ¬ ⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩
15		breq12 5118	. . . . . . . 8 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑎 = ⟨𝑝, 𝑞⟩) → (𝑎𝑇𝑎 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩))
16	15	anidms 576	. . . . . . 7 ⊢ (𝑎 = ⟨𝑝, 𝑞⟩ → (𝑎𝑇𝑎 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩))
17	14, 16	mtbiri 330	. . . . . 6 ⊢ (𝑎 = ⟨𝑝, 𝑞⟩ → ¬ 𝑎𝑇𝑎)
18	17	rexlimivw 3168	. . . . 5 ⊢ (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ → ¬ 𝑎𝑇𝑎)
19	18	rexlimivw 3168	. . . 4 ⊢ (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ → ¬ 𝑎𝑇𝑎)
20	1, 19	sylbi 220	. . 3 ⊢ (𝑎 ∈ (𝐴 × 𝐵) → ¬ 𝑎𝑇𝑎)
21	20	adantl 486	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐴 × 𝐵)) → ¬ 𝑎𝑇𝑎)
22		3reeanv 3244	. . . 4 ⊢ (∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩) ↔ (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑡 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
23		3reeanv 3244	. . . . . 6 ⊢ (∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) ↔ (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
24	23	rexbii 3118	. . . . 5 ⊢ (∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) ↔ ∃𝑡 ∈ 𝐴 (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
25	24	2rexbii 3147	. . . 4 ⊢ (∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) ↔ ∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
26		elxp2 5686	. . . . 5 ⊢ (𝑏 ∈ (𝐴 × 𝐵) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩)
27		elxp2 5686	. . . . 5 ⊢ (𝑐 ∈ (𝐴 × 𝐵) ↔ ∃𝑡 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩)
28	1, 26, 27	3anbi123i 1171	. . . 4 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑏 ∈ (𝐴 × 𝐵) ∧ 𝑐 ∈ (𝐴 × 𝐵)) ↔ (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑡 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
29	22, 25, 28	3bitr4ri 307	. . 3 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑏 ∈ (𝐴 × 𝐵) ∧ 𝑐 ∈ (𝐴 × 𝐵)) ↔ ∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩))
30		df-3an 1103	. . . . . . . . . 10 ⊢ (((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) ↔ (((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)))
31		simp3 1154	. . . . . . . . . . . 12 ⊢ (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)))
32		simp3 1154	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))) → ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))
33		simpr1l 1247	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑝 ∈ 𝐴)
34	33	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑝 ∈ 𝐴)
35		simpr2r 1250	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑞 ∈ 𝐵)
36	35	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑞 ∈ 𝐵)
37	34, 36	jca 520	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵))
38		simpr2l 1249	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑡 ∈ 𝐴)
39	38	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑡 ∈ 𝐴)
40		simpr3r 1252	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑢 ∈ 𝐵)
41	40	adantr 485	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑢 ∈ 𝐵)
42	39, 41	jca 520	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵))
43		poxp2.1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑅 Po 𝐴)
44	43	ad2antrr 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑅 Po 𝐴)
45		simpr1r 1248	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑟 ∈ 𝐴)
46	45	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑟 ∈ 𝐴)
47		potr 5583	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Po 𝐴 ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴)) → ((𝑝𝑅𝑟 ∧ 𝑟𝑅𝑡) → 𝑝𝑅𝑡))
48	44, 34, 46, 39, 47	syl13anc 1397	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝𝑅𝑟 ∧ 𝑟𝑅𝑡) → 𝑝𝑅𝑡))
49		orc 880	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))
50	48, 49	syl6 36	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝𝑅𝑟 ∧ 𝑟𝑅𝑡) → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
51	50	expd 420	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝𝑅𝑟 → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))))
52		breq1 5116	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑟 → (𝑝𝑅𝑡 ↔ 𝑟𝑅𝑡))
53	52, 49	biimtrrdi 257	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑟 → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
54	53	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝 = 𝑟 → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))))
55		simprl1 1235	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝𝑅𝑟 ∨ 𝑝 = 𝑟))
56	51, 54, 55	mpjaod 873	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
57		breq2 5117	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑡 → (𝑝𝑅𝑟 ↔ 𝑝𝑅𝑡))
58		equequ2 2053	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑡 → (𝑝 = 𝑟 ↔ 𝑝 = 𝑡))
59	57, 58	orbi12d 931	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑡 → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ↔ (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
60	55, 59	syl5ibcom 248	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 = 𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
61		simprr1 1238	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡))
62	56, 60, 61	mpjaod 873	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))
63		poxp2.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑆 Po 𝐵)
64	63	ad2antrr 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑆 Po 𝐵)
65		simpr3l 1251	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑠 ∈ 𝐵)
66	65	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑠 ∈ 𝐵)
67		potr 5583	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 Po 𝐵 ∧ (𝑞 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) → ((𝑞𝑆𝑠 ∧ 𝑠𝑆𝑢) → 𝑞𝑆𝑢))
68	64, 36, 66, 41, 67	syl13anc 1397	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑞𝑆𝑠 ∧ 𝑠𝑆𝑢) → 𝑞𝑆𝑢))
69		orc 880	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))
70	68, 69	syl6 36	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑞𝑆𝑠 ∧ 𝑠𝑆𝑢) → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
71	70	expd 420	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞𝑆𝑠 → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))))
72		breq1 5116	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = 𝑠 → (𝑞𝑆𝑢 ↔ 𝑠𝑆𝑢))
73	72, 69	biimtrrdi 257	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = 𝑠 → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
74	73	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞 = 𝑠 → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))))
75		simprl2 1236	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠))
76	71, 74, 75	mpjaod 873	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
77		breq2 5117	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑢 → (𝑞𝑆𝑠 ↔ 𝑞𝑆𝑢))
78		equequ2 2053	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑢 → (𝑞 = 𝑠 ↔ 𝑞 = 𝑢))
79	77, 78	orbi12d 931	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑢 → ((𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ↔ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
80	75, 79	syl5ibcom 248	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠 = 𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
81		simprr2 1239	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢))
82	76, 80, 81	mpjaod 873	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))
83		simprr3 1240	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))
84		neorian 3059	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢) ↔ ¬ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))
85	83, 84	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ¬ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))
86		neorian 3059	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢) ↔ ¬ (𝑝 = 𝑡 ∧ 𝑞 = 𝑢))
87	86	con2bii 360	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) ↔ ¬ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))
88		breq1 5116	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑡 → (𝑝𝑅𝑟 ↔ 𝑡𝑅𝑟))
89		equequ1 2052	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑡 → (𝑝 = 𝑟 ↔ 𝑡 = 𝑟))
90	88, 89	orbi12d 931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = 𝑡 → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟)))
91	90	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟)))
92		breq1 5116	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑢 → (𝑞𝑆𝑠 ↔ 𝑢𝑆𝑠))
93		equequ1 2052	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑢 → (𝑞 = 𝑠 ↔ 𝑢 = 𝑠))
94	92, 93	orbi12d 931	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 = 𝑢 → ((𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠)))
95	94	adantl 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠)))
96		neeq1 3026	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑡 → (𝑝 ≠ 𝑟 ↔ 𝑡 ≠ 𝑟))
97	96	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (𝑝 ≠ 𝑟 ↔ 𝑡 ≠ 𝑟))
98		neeq1 3026	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑢 → (𝑞 ≠ 𝑠 ↔ 𝑢 ≠ 𝑠))
99	98	adantl 486	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (𝑞 ≠ 𝑠 ↔ 𝑢 ≠ 𝑠))
100	97, 99	orbi12d 931	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠) ↔ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)))
101	91, 95, 100	3anbi123d 1462	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ↔ ((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠))))
102	101	anbi1d 642	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))) ↔ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))))
103	102	anbi2d 641	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) ↔ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))))))
104		simprl1 1235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟))
105		simprr1 1238	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡))
106		orcom 883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡) ∨ 𝑟 = 𝑡) ↔ (𝑟 = 𝑡 ∨ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡)))
107		ordi 1021	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑟 = 𝑡 ∨ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡)) ↔ ((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ∧ (𝑟 = 𝑡 ∨ 𝑟𝑅𝑡)))
108		orcom 883	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑟 = 𝑡))
109		equcom 2045	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑟 = 𝑡 ↔ 𝑡 = 𝑟)
110	109	orbi2i 925	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡𝑅𝑟 ∨ 𝑟 = 𝑡) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟))
111	108, 110	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟))
112		orcom 883	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑟 = 𝑡 ∨ 𝑟𝑅𝑡) ↔ (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡))
113	111, 112	anbi12i 639	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ∧ (𝑟 = 𝑡 ∨ 𝑟𝑅𝑡)) ↔ ((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡)))
114	106, 107, 113	3bitri 300	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡) ∨ 𝑟 = 𝑡) ↔ ((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡)))
115	104, 105, 114	sylanbrc 594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡) ∨ 𝑟 = 𝑡))
116	43	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑅 Po 𝐴)
117	38	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑡 ∈ 𝐴)
118	45	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑟 ∈ 𝐴)
119		po2nr 5584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po 𝐴 ∧ (𝑡 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) → ¬ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡))
120	116, 117, 118, 119	syl12anc 849	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ¬ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡))
121	115, 120	orcnd 891	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑟 = 𝑡)
122		simprl2 1236	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠))
123		simprr2 1239	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢))
124		orcom 883	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢) ∨ 𝑠 = 𝑢) ↔ (𝑠 = 𝑢 ∨ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢)))
125		ordi 1021	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 = 𝑢 ∨ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢)) ↔ ((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ∧ (𝑠 = 𝑢 ∨ 𝑠𝑆𝑢)))
126		orcom 883	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑠 = 𝑢))
127		equcom 2045	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = 𝑢 ↔ 𝑢 = 𝑠)
128	127	orbi2i 925	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢𝑆𝑠 ∨ 𝑠 = 𝑢) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠))
129	126, 128	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠))
130		orcom 883	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 = 𝑢 ∨ 𝑠𝑆𝑢) ↔ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢))
131	129, 130	anbi12i 639	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ∧ (𝑠 = 𝑢 ∨ 𝑠𝑆𝑢)) ↔ ((𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢)))
132	124, 125, 131	3bitri 300	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢) ∨ 𝑠 = 𝑢) ↔ ((𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢)))
133	122, 123, 132	sylanbrc 594	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢) ∨ 𝑠 = 𝑢))
134	63	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑆 Po 𝐵)
135	40	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑢 ∈ 𝐵)
136	65	adantr 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑠 ∈ 𝐵)
137		po2nr 5584	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 Po 𝐵 ∧ (𝑢 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵)) → ¬ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢))
138	134, 135, 136, 137	syl12anc 849	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ¬ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢))
139	133, 138	orcnd 891	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑠 = 𝑢)
140	121, 139	jca 520	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))
141	103, 140	biimtrdi 256	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
142	141	com12 33	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
143	87, 142	biimtrrid 246	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (¬ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
144	85, 143	mt3d 149	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))
145	62, 82, 144	3jca 1144	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))
146	37, 42, 145	3jca 1144	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))))
147	146	ex 417	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))))
148	31, 32, 147	syl2ani 618	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))))
149		breq12 5118	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩) → (𝑎𝑇𝑏 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑟, 𝑠⟩))
150	149	3adant3 1148	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑏 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑟, 𝑠⟩))
151	12	xpord2lem 8137	. . . . . . . . . . . . . 14 ⊢ (⟨𝑝, 𝑞⟩𝑇⟨𝑟, 𝑠⟩ ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))))
152	150, 151	bitrdi 290	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑏 ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)))))
153		breq12 5118	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑏𝑇𝑐 ↔ ⟨𝑟, 𝑠⟩𝑇⟨𝑡, 𝑢⟩))
154	153	3adant1 1146	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑏𝑇𝑐 ↔ ⟨𝑟, 𝑠⟩𝑇⟨𝑡, 𝑢⟩))
155	12	xpord2lem 8137	. . . . . . . . . . . . . 14 ⊢ (⟨𝑟, 𝑠⟩𝑇⟨𝑡, 𝑢⟩ ↔ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))))
156	154, 155	bitrdi 290	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑏𝑇𝑐 ↔ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))))
157	152, 156	anbi12d 643	. . . . . . . . . . . 12 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) ↔ (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))))))
158		breq12 5118	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑐 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑡, 𝑢⟩))
159	158	3adant2 1147	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑐 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑡, 𝑢⟩))
160	12	xpord2lem 8137	. . . . . . . . . . . . 13 ⊢ (⟨𝑝, 𝑞⟩𝑇⟨𝑡, 𝑢⟩ ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))))
161	159, 160	bitrdi 290	. . . . . . . . . . . 12 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑐 ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))))
162	157, 161	imbi12d 347	. . . . . . . . . . 11 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐) ↔ ((((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))))))
163	148, 162	syl5ibrcom 250	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
164	30, 163	sylan2br 606	. . . . . . . . 9 ⊢ ((𝜑 ∧ (((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
165	164	anassrs 472	. . . . . . . 8 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵))) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) → ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
166	165	rexlimdvva 3228	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵))) → (∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
167	166	anassrs 472	. . . . . 6 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵)) → (∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
168	167	rexlimdvva 3228	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) → (∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
169	168	rexlimdvva 3228	. . . 4 ⊢ (𝜑 → (∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
170	169	imp 411	. . 3 ⊢ ((𝜑 ∧ ∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩)) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐))
171	29, 170	sylan2b 605	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑏 ∈ (𝐴 × 𝐵) ∧ 𝑐 ∈ (𝐴 × 𝐵))) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐))
172	21, 171	ispod 5579	1 ⊢ (𝜑 → 𝑇 Po (𝐴 × 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1101 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 ∃wrex 3095 ⟨cop 4600 class class class wbr 5113 {copab 5177 Po wpo 5568 × cxp 5660 ‘cfv 6537 1^st c1st 7983 2^nd c2nd 7984

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pr 5405 ax-un 7733

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-ral 3086 df-rex 3096 df-rab 3424 df-v 3465 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-nul 4295 df-if 4493 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-br 5114 df-opab 5178 df-mpt 5197 df-id 5557 df-po 5570 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-iota 6493 df-fun 6539 df-fv 6545 df-1st 7985 df-2nd 7986

This theorem is referenced by: xpord2indlem 8142 on2recsfn 8652 on2recsov 8653 noxpordpo 28108

W3C validator