poxp2 - Mathbox for Scott Fenton

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

Theorem poxp2 33357

Description: Another way of partially ordering a cross 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 5552	. . . 4 ⊢ (𝑎 ∈ (𝐴 × 𝐵) ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩)
2		equid 2019	. . . . . . . . . . . 12 ⊢ 𝑝 = 𝑝
3		equid 2019	. . . . . . . . . . . 12 ⊢ 𝑞 = 𝑞
4	2, 3	pm3.2i 474	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑝 ∧ 𝑞 = 𝑞)
5		neorian 3045	. . . . . . . . . . . 12 ⊢ ((𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞) ↔ ¬ (𝑝 = 𝑝 ∧ 𝑞 = 𝑞))
6	5	con2bii 361	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑝 ∧ 𝑞 = 𝑞) ↔ ¬ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))
7	4, 6	mpbi 233	. . . . . . . . . 10 ⊢ ¬ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)
8		simp3 1135	. . . . . . . . . 10 ⊢ (((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)) → (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))
9	7, 8	mto 200	. . . . . . . . 9 ⊢ ¬ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))
10		simp3 1135	. . . . . . . . 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 33356	. . . . . . . 8 ⊢ (⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩ ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))))
14	11, 13	mtbir 326	. . . . . . 7 ⊢ ¬ ⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩
15		breq12 5041	. . . . . . . 8 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑎 = ⟨𝑝, 𝑞⟩) → (𝑎𝑇𝑎 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩))
16	15	anidms 570	. . . . . . 7 ⊢ (𝑎 = ⟨𝑝, 𝑞⟩ → (𝑎𝑇𝑎 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩))
17	14, 16	mtbiri 330	. . . . . 6 ⊢ (𝑎 = ⟨𝑝, 𝑞⟩ → ¬ 𝑎𝑇𝑎)
18	17	rexlimivw 3206	. . . . 5 ⊢ (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ → ¬ 𝑎𝑇𝑎)
19	18	rexlimivw 3206	. . . 4 ⊢ (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ → ¬ 𝑎𝑇𝑎)
20	1, 19	sylbi 220	. . 3 ⊢ (𝑎 ∈ (𝐴 × 𝐵) → ¬ 𝑎𝑇𝑎)
21	20	adantl 485	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐴 × 𝐵)) → ¬ 𝑎𝑇𝑎)
22		3reeanv 3286	. . . 4 ⊢ (∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩) ↔ (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑡 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
23		3reeanv 3286	. . . . . 6 ⊢ (∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) ↔ (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
24	23	rexbii 3175	. . . . 5 ⊢ (∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) ↔ ∃𝑡 ∈ 𝐴 (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
25	24	2rexbii 3176	. . . 4 ⊢ (∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) ↔ ∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
26		elxp2 5552	. . . . 5 ⊢ (𝑏 ∈ (𝐴 × 𝐵) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩)
27		elxp2 5552	. . . . 5 ⊢ (𝑐 ∈ (𝐴 × 𝐵) ↔ ∃𝑡 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩)
28	1, 26, 27	3anbi123i 1152	. . . 4 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑏 ∈ (𝐴 × 𝐵) ∧ 𝑐 ∈ (𝐴 × 𝐵)) ↔ (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑡 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
29	22, 25, 28	3bitr4ri 307	. . 3 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑏 ∈ (𝐴 × 𝐵) ∧ 𝑐 ∈ (𝐴 × 𝐵)) ↔ ∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩))
30		df-3an 1086	. . . . . . . . . 10 ⊢ (((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) ↔ (((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)))
31		simp3 1135	. . . . . . . . . . . 12 ⊢ (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)))
32		simp3 1135	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))) → ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))
33		simpr1l 1227	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑝 ∈ 𝐴)
34	33	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑝 ∈ 𝐴)
35		simpr2r 1230	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑞 ∈ 𝐵)
36	35	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑞 ∈ 𝐵)
37	34, 36	jca 515	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵))
38		simpr2l 1229	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑡 ∈ 𝐴)
39	38	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑡 ∈ 𝐴)
40		simpr3r 1232	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑢 ∈ 𝐵)
41	40	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑢 ∈ 𝐵)
42	39, 41	jca 515	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵))
43		poxp2.1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑅 Po 𝐴)
44	43	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑅 Po 𝐴)
45		simpr1r 1228	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑟 ∈ 𝐴)
46	45	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑟 ∈ 𝐴)
47		potr 5459	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Po 𝐴 ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴)) → ((𝑝𝑅𝑟 ∧ 𝑟𝑅𝑡) → 𝑝𝑅𝑡))
48	44, 34, 46, 39, 47	syl13anc 1369	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝𝑅𝑟 ∧ 𝑟𝑅𝑡) → 𝑝𝑅𝑡))
49		orc 864	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))
50	48, 49	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝𝑅𝑟 ∧ 𝑟𝑅𝑡) → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
51	50	expd 419	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝𝑅𝑟 → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))))
52		breq1 5039	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑟 → (𝑝𝑅𝑡 ↔ 𝑟𝑅𝑡))
53	52, 49	syl6bir 257	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑟 → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
54	53	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝 = 𝑟 → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))))
55		simprl1 1215	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝𝑅𝑟 ∨ 𝑝 = 𝑟))
56	51, 54, 55	mpjaod 857	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
57		breq2 5040	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑡 → (𝑝𝑅𝑟 ↔ 𝑝𝑅𝑡))
58		equequ2 2033	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑡 → (𝑝 = 𝑟 ↔ 𝑝 = 𝑡))
59	57, 58	orbi12d 916	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑡 → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ↔ (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
60	55, 59	syl5ibcom 248	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 = 𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
61		simprr1 1218	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡))
62	56, 60, 61	mpjaod 857	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))
63		poxp2.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑆 Po 𝐵)
64	63	ad2antrr 725	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑆 Po 𝐵)
65		simpr3l 1231	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑠 ∈ 𝐵)
66	65	adantr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑠 ∈ 𝐵)
67		potr 5459	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 Po 𝐵 ∧ (𝑞 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) → ((𝑞𝑆𝑠 ∧ 𝑠𝑆𝑢) → 𝑞𝑆𝑢))
68	64, 36, 66, 41, 67	syl13anc 1369	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑞𝑆𝑠 ∧ 𝑠𝑆𝑢) → 𝑞𝑆𝑢))
69		orc 864	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))
70	68, 69	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑞𝑆𝑠 ∧ 𝑠𝑆𝑢) → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
71	70	expd 419	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞𝑆𝑠 → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))))
72		breq1 5039	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = 𝑠 → (𝑞𝑆𝑢 ↔ 𝑠𝑆𝑢))
73	72, 69	syl6bir 257	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = 𝑠 → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
74	73	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞 = 𝑠 → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))))
75		simprl2 1216	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠))
76	71, 74, 75	mpjaod 857	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
77		breq2 5040	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑢 → (𝑞𝑆𝑠 ↔ 𝑞𝑆𝑢))
78		equequ2 2033	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑢 → (𝑞 = 𝑠 ↔ 𝑞 = 𝑢))
79	77, 78	orbi12d 916	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑢 → ((𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ↔ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
80	75, 79	syl5ibcom 248	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠 = 𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
81		simprr2 1219	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢))
82	76, 80, 81	mpjaod 857	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))
83		simprr3 1220	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))
84		neorian 3045	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢) ↔ ¬ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))
85	83, 84	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ¬ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))
86		neorian 3045	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢) ↔ ¬ (𝑝 = 𝑡 ∧ 𝑞 = 𝑢))
87	86	con2bii 361	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) ↔ ¬ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))
88		breq1 5039	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑡 → (𝑝𝑅𝑟 ↔ 𝑡𝑅𝑟))
89		equequ1 2032	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑡 → (𝑝 = 𝑟 ↔ 𝑡 = 𝑟))
90	88, 89	orbi12d 916	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = 𝑡 → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟)))
91	90	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟)))
92		breq1 5039	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑢 → (𝑞𝑆𝑠 ↔ 𝑢𝑆𝑠))
93		equequ1 2032	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑢 → (𝑞 = 𝑠 ↔ 𝑢 = 𝑠))
94	92, 93	orbi12d 916	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 = 𝑢 → ((𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠)))
95	94	adantl 485	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠)))
96		neeq1 3013	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑡 → (𝑝 ≠ 𝑟 ↔ 𝑡 ≠ 𝑟))
97	96	adantr 484	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (𝑝 ≠ 𝑟 ↔ 𝑡 ≠ 𝑟))
98		neeq1 3013	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑢 → (𝑞 ≠ 𝑠 ↔ 𝑢 ≠ 𝑠))
99	98	adantl 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (𝑞 ≠ 𝑠 ↔ 𝑢 ≠ 𝑠))
100	97, 99	orbi12d 916	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠) ↔ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)))
101	91, 95, 100	3anbi123d 1433	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ↔ ((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠))))
102	101	anbi1d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))) ↔ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))))
103	102	anbi2d 631	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) ↔ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))))))
104		simprl1 1215	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟))
105		simprr1 1218	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡))
106		orcom 867	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡) ∨ 𝑟 = 𝑡) ↔ (𝑟 = 𝑡 ∨ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡)))
107		ordi 1003	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑟 = 𝑡 ∨ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡)) ↔ ((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ∧ (𝑟 = 𝑡 ∨ 𝑟𝑅𝑡)))
108		orcom 867	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑟 = 𝑡))
109		equcom 2025	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑟 = 𝑡 ↔ 𝑡 = 𝑟)
110	109	orbi2i 910	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡𝑅𝑟 ∨ 𝑟 = 𝑡) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟))
111	108, 110	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟))
112		orcom 867	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑟 = 𝑡 ∨ 𝑟𝑅𝑡) ↔ (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡))
113	111, 112	anbi12i 629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ∧ (𝑟 = 𝑡 ∨ 𝑟𝑅𝑡)) ↔ ((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡)))
114	106, 107, 113	3bitri 300	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡) ∨ 𝑟 = 𝑡) ↔ ((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡)))
115	104, 105, 114	sylanbrc 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡) ∨ 𝑟 = 𝑡))
116	43	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑅 Po 𝐴)
117	38	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑡 ∈ 𝐴)
118	45	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑟 ∈ 𝐴)
119		po2nr 5460	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po 𝐴 ∧ (𝑡 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) → ¬ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡))
120	116, 117, 118, 119	syl12anc 835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ¬ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡))
121	115, 120	orcnd 876	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑟 = 𝑡)
122		simprl2 1216	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠))
123		simprr2 1219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢))
124		orcom 867	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢) ∨ 𝑠 = 𝑢) ↔ (𝑠 = 𝑢 ∨ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢)))
125		ordi 1003	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 = 𝑢 ∨ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢)) ↔ ((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ∧ (𝑠 = 𝑢 ∨ 𝑠𝑆𝑢)))
126		orcom 867	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑠 = 𝑢))
127		equcom 2025	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = 𝑢 ↔ 𝑢 = 𝑠)
128	127	orbi2i 910	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢𝑆𝑠 ∨ 𝑠 = 𝑢) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠))
129	126, 128	bitri 278	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠))
130		orcom 867	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 = 𝑢 ∨ 𝑠𝑆𝑢) ↔ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢))
131	129, 130	anbi12i 629	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ∧ (𝑠 = 𝑢 ∨ 𝑠𝑆𝑢)) ↔ ((𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢)))
132	124, 125, 131	3bitri 300	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢) ∨ 𝑠 = 𝑢) ↔ ((𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢)))
133	122, 123, 132	sylanbrc 586	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢) ∨ 𝑠 = 𝑢))
134	63	ad2antrr 725	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑆 Po 𝐵)
135	40	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑢 ∈ 𝐵)
136	65	adantr 484	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑠 ∈ 𝐵)
137		po2nr 5460	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 Po 𝐵 ∧ (𝑢 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵)) → ¬ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢))
138	134, 135, 136, 137	syl12anc 835	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ¬ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢))
139	133, 138	orcnd 876	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑠 = 𝑢)
140	121, 139	jca 515	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))
141	103, 140	syl6bi 256	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
142	141	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
143	87, 142	syl5bir 246	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (¬ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
144	85, 143	mt3d 150	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))
145	62, 82, 144	3jca 1125	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))
146	37, 42, 145	3jca 1125	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))))
147	146	ex 416	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))))
148	31, 32, 147	syl2ani 609	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))))
149		breq12 5041	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩) → (𝑎𝑇𝑏 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑟, 𝑠⟩))
150	149	3adant3 1129	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑏 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑟, 𝑠⟩))
151	12	xpord2lem 33356	. . . . . . . . . . . . . 14 ⊢ (⟨𝑝, 𝑞⟩𝑇⟨𝑟, 𝑠⟩ ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))))
152	150, 151	bitrdi 290	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑏 ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)))))
153		breq12 5041	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑏𝑇𝑐 ↔ ⟨𝑟, 𝑠⟩𝑇⟨𝑡, 𝑢⟩))
154	153	3adant1 1127	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑏𝑇𝑐 ↔ ⟨𝑟, 𝑠⟩𝑇⟨𝑡, 𝑢⟩))
155	12	xpord2lem 33356	. . . . . . . . . . . . . 14 ⊢ (⟨𝑟, 𝑠⟩𝑇⟨𝑡, 𝑢⟩ ↔ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))))
156	154, 155	bitrdi 290	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑏𝑇𝑐 ↔ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))))
157	152, 156	anbi12d 633	. . . . . . . . . . . 12 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) ↔ (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))))))
158		breq12 5041	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑐 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑡, 𝑢⟩))
159	158	3adant2 1128	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑐 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑡, 𝑢⟩))
160	12	xpord2lem 33356	. . . . . . . . . . . . 13 ⊢ (⟨𝑝, 𝑞⟩𝑇⟨𝑡, 𝑢⟩ ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))))
161	159, 160	bitrdi 290	. . . . . . . . . . . 12 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑐 ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))))
162	157, 161	imbi12d 348	. . . . . . . . . . 11 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐) ↔ ((((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))))))
163	148, 162	syl5ibrcom 250	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
164	30, 163	sylan2br 597	. . . . . . . . 9 ⊢ ((𝜑 ∧ (((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
165	164	anassrs 471	. . . . . . . 8 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵))) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) → ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
166	165	rexlimdvva 3218	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵))) → (∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
167	166	anassrs 471	. . . . . 6 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵)) → (∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
168	167	rexlimdvva 3218	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) → (∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
169	168	rexlimdvva 3218	. . . 4 ⊢ (𝜑 → (∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
170	169	imp 410	. . 3 ⊢ ((𝜑 ∧ ∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩)) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐))
171	29, 170	sylan2b 596	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑏 ∈ (𝐴 × 𝐵) ∧ 𝑐 ∈ (𝐴 × 𝐵))) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐))
172	21, 171	ispod 5455	1 ⊢ (𝜑 → 𝑇 Po (𝐴 × 𝐵))

Colors of variables: wff setvar class

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

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

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

This theorem is referenced by: xpord2ind 33361 on2recsfn 33423 on2recsov 33424 noxpordpo 33689

W3C validator