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 33769

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 5612	. . . 4 ⊢ (𝑎 ∈ (𝐴 × 𝐵) ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩)
2		equid 2018	. . . . . . . . . . . 12 ⊢ 𝑝 = 𝑝
3		equid 2018	. . . . . . . . . . . 12 ⊢ 𝑞 = 𝑞
4	2, 3	pm3.2i 470	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑝 ∧ 𝑞 = 𝑞)
5		neorian 3040	. . . . . . . . . . . 12 ⊢ ((𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞) ↔ ¬ (𝑝 = 𝑝 ∧ 𝑞 = 𝑞))
6	5	con2bii 357	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑝 ∧ 𝑞 = 𝑞) ↔ ¬ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))
7	4, 6	mpbi 229	. . . . . . . . . 10 ⊢ ¬ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)
8		simp3 1136	. . . . . . . . . 10 ⊢ (((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)) → (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))
9	7, 8	mto 196	. . . . . . . . 9 ⊢ ¬ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))
10		simp3 1136	. . . . . . . . 9 ⊢ (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))) → ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)))
11	9, 10	mto 196	. . . . . . . 8 ⊢ ¬ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)))
12		xpord2.1	. . . . . . . . 9 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥)𝑆(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}
13	12	xpord2lem 33768	. . . . . . . 8 ⊢ (⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩ ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))))
14	11, 13	mtbir 322	. . . . . . 7 ⊢ ¬ ⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩
15		breq12 5083	. . . . . . . 8 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑎 = ⟨𝑝, 𝑞⟩) → (𝑎𝑇𝑎 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩))
16	15	anidms 566	. . . . . . 7 ⊢ (𝑎 = ⟨𝑝, 𝑞⟩ → (𝑎𝑇𝑎 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩))
17	14, 16	mtbiri 326	. . . . . 6 ⊢ (𝑎 = ⟨𝑝, 𝑞⟩ → ¬ 𝑎𝑇𝑎)
18	17	rexlimivw 3212	. . . . 5 ⊢ (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ → ¬ 𝑎𝑇𝑎)
19	18	rexlimivw 3212	. . . 4 ⊢ (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ → ¬ 𝑎𝑇𝑎)
20	1, 19	sylbi 216	. . 3 ⊢ (𝑎 ∈ (𝐴 × 𝐵) → ¬ 𝑎𝑇𝑎)
21	20	adantl 481	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐴 × 𝐵)) → ¬ 𝑎𝑇𝑎)
22		3reeanv 3295	. . . 4 ⊢ (∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩) ↔ (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑡 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
23		3reeanv 3295	. . . . . 6 ⊢ (∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) ↔ (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
24	23	rexbii 3179	. . . . 5 ⊢ (∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) ↔ ∃𝑡 ∈ 𝐴 (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
25	24	2rexbii 3180	. . . 4 ⊢ (∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) ↔ ∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
26		elxp2 5612	. . . . 5 ⊢ (𝑏 ∈ (𝐴 × 𝐵) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩)
27		elxp2 5612	. . . . 5 ⊢ (𝑐 ∈ (𝐴 × 𝐵) ↔ ∃𝑡 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩)
28	1, 26, 27	3anbi123i 1153	. . . 4 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑏 ∈ (𝐴 × 𝐵) ∧ 𝑐 ∈ (𝐴 × 𝐵)) ↔ (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑡 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
29	22, 25, 28	3bitr4ri 303	. . 3 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑏 ∈ (𝐴 × 𝐵) ∧ 𝑐 ∈ (𝐴 × 𝐵)) ↔ ∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩))
30		df-3an 1087	. . . . . . . . . 10 ⊢ (((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) ↔ (((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)))
31		simp3 1136	. . . . . . . . . . . 12 ⊢ (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)))
32		simp3 1136	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))) → ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))
33		simpr1l 1228	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑝 ∈ 𝐴)
34	33	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑝 ∈ 𝐴)
35		simpr2r 1231	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑞 ∈ 𝐵)
36	35	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑞 ∈ 𝐵)
37	34, 36	jca 511	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵))
38		simpr2l 1230	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑡 ∈ 𝐴)
39	38	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑡 ∈ 𝐴)
40		simpr3r 1233	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑢 ∈ 𝐵)
41	40	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑢 ∈ 𝐵)
42	39, 41	jca 511	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵))
43		poxp2.1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑅 Po 𝐴)
44	43	ad2antrr 722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑅 Po 𝐴)
45		simpr1r 1229	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑟 ∈ 𝐴)
46	45	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑟 ∈ 𝐴)
47		potr 5515	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Po 𝐴 ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴)) → ((𝑝𝑅𝑟 ∧ 𝑟𝑅𝑡) → 𝑝𝑅𝑡))
48	44, 34, 46, 39, 47	syl13anc 1370	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝𝑅𝑟 ∧ 𝑟𝑅𝑡) → 𝑝𝑅𝑡))
49		orc 863	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))
50	48, 49	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝𝑅𝑟 ∧ 𝑟𝑅𝑡) → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
51	50	expd 415	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝𝑅𝑟 → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))))
52		breq1 5081	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑟 → (𝑝𝑅𝑡 ↔ 𝑟𝑅𝑡))
53	52, 49	syl6bir 253	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑟 → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
54	53	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝 = 𝑟 → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))))
55		simprl1 1216	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝𝑅𝑟 ∨ 𝑝 = 𝑟))
56	51, 54, 55	mpjaod 856	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
57		breq2 5082	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑡 → (𝑝𝑅𝑟 ↔ 𝑝𝑅𝑡))
58		equequ2 2032	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑡 → (𝑝 = 𝑟 ↔ 𝑝 = 𝑡))
59	57, 58	orbi12d 915	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑡 → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ↔ (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
60	55, 59	syl5ibcom 244	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 = 𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
61		simprr1 1219	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡))
62	56, 60, 61	mpjaod 856	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))
63		poxp2.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑆 Po 𝐵)
64	63	ad2antrr 722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑆 Po 𝐵)
65		simpr3l 1232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑠 ∈ 𝐵)
66	65	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑠 ∈ 𝐵)
67		potr 5515	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 Po 𝐵 ∧ (𝑞 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) → ((𝑞𝑆𝑠 ∧ 𝑠𝑆𝑢) → 𝑞𝑆𝑢))
68	64, 36, 66, 41, 67	syl13anc 1370	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑞𝑆𝑠 ∧ 𝑠𝑆𝑢) → 𝑞𝑆𝑢))
69		orc 863	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))
70	68, 69	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑞𝑆𝑠 ∧ 𝑠𝑆𝑢) → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
71	70	expd 415	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞𝑆𝑠 → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))))
72		breq1 5081	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = 𝑠 → (𝑞𝑆𝑢 ↔ 𝑠𝑆𝑢))
73	72, 69	syl6bir 253	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = 𝑠 → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
74	73	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞 = 𝑠 → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))))
75		simprl2 1217	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠))
76	71, 74, 75	mpjaod 856	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
77		breq2 5082	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑢 → (𝑞𝑆𝑠 ↔ 𝑞𝑆𝑢))
78		equequ2 2032	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑢 → (𝑞 = 𝑠 ↔ 𝑞 = 𝑢))
79	77, 78	orbi12d 915	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑢 → ((𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ↔ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
80	75, 79	syl5ibcom 244	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠 = 𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
81		simprr2 1220	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢))
82	76, 80, 81	mpjaod 856	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))
83		simprr3 1221	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))
84		neorian 3040	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢) ↔ ¬ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))
85	83, 84	sylib 217	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ¬ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))
86		neorian 3040	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢) ↔ ¬ (𝑝 = 𝑡 ∧ 𝑞 = 𝑢))
87	86	con2bii 357	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) ↔ ¬ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))
88		breq1 5081	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑡 → (𝑝𝑅𝑟 ↔ 𝑡𝑅𝑟))
89		equequ1 2031	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑡 → (𝑝 = 𝑟 ↔ 𝑡 = 𝑟))
90	88, 89	orbi12d 915	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = 𝑡 → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟)))
91	90	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟)))
92		breq1 5081	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑢 → (𝑞𝑆𝑠 ↔ 𝑢𝑆𝑠))
93		equequ1 2031	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑢 → (𝑞 = 𝑠 ↔ 𝑢 = 𝑠))
94	92, 93	orbi12d 915	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 = 𝑢 → ((𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠)))
95	94	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠)))
96		neeq1 3007	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑡 → (𝑝 ≠ 𝑟 ↔ 𝑡 ≠ 𝑟))
97	96	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (𝑝 ≠ 𝑟 ↔ 𝑡 ≠ 𝑟))
98		neeq1 3007	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑢 → (𝑞 ≠ 𝑠 ↔ 𝑢 ≠ 𝑠))
99	98	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (𝑞 ≠ 𝑠 ↔ 𝑢 ≠ 𝑠))
100	97, 99	orbi12d 915	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠) ↔ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)))
101	91, 95, 100	3anbi123d 1434	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ↔ ((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠))))
102	101	anbi1d 629	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))) ↔ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))))
103	102	anbi2d 628	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) ↔ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))))))
104		simprl1 1216	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟))
105		simprr1 1219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡))
106		orcom 866	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡) ∨ 𝑟 = 𝑡) ↔ (𝑟 = 𝑡 ∨ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡)))
107		ordi 1002	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑟 = 𝑡 ∨ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡)) ↔ ((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ∧ (𝑟 = 𝑡 ∨ 𝑟𝑅𝑡)))
108		orcom 866	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑟 = 𝑡))
109		equcom 2024	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑟 = 𝑡 ↔ 𝑡 = 𝑟)
110	109	orbi2i 909	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡𝑅𝑟 ∨ 𝑟 = 𝑡) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟))
111	108, 110	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟))
112		orcom 866	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑟 = 𝑡 ∨ 𝑟𝑅𝑡) ↔ (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡))
113	111, 112	anbi12i 626	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ∧ (𝑟 = 𝑡 ∨ 𝑟𝑅𝑡)) ↔ ((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡)))
114	106, 107, 113	3bitri 296	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡) ∨ 𝑟 = 𝑡) ↔ ((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡)))
115	104, 105, 114	sylanbrc 582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡) ∨ 𝑟 = 𝑡))
116	43	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑅 Po 𝐴)
117	38	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑡 ∈ 𝐴)
118	45	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑟 ∈ 𝐴)
119		po2nr 5516	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po 𝐴 ∧ (𝑡 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) → ¬ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡))
120	116, 117, 118, 119	syl12anc 833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ¬ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡))
121	115, 120	orcnd 875	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑟 = 𝑡)
122		simprl2 1217	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠))
123		simprr2 1220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢))
124		orcom 866	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢) ∨ 𝑠 = 𝑢) ↔ (𝑠 = 𝑢 ∨ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢)))
125		ordi 1002	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 = 𝑢 ∨ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢)) ↔ ((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ∧ (𝑠 = 𝑢 ∨ 𝑠𝑆𝑢)))
126		orcom 866	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑠 = 𝑢))
127		equcom 2024	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = 𝑢 ↔ 𝑢 = 𝑠)
128	127	orbi2i 909	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢𝑆𝑠 ∨ 𝑠 = 𝑢) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠))
129	126, 128	bitri 274	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠))
130		orcom 866	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 = 𝑢 ∨ 𝑠𝑆𝑢) ↔ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢))
131	129, 130	anbi12i 626	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ∧ (𝑠 = 𝑢 ∨ 𝑠𝑆𝑢)) ↔ ((𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢)))
132	124, 125, 131	3bitri 296	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢) ∨ 𝑠 = 𝑢) ↔ ((𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢)))
133	122, 123, 132	sylanbrc 582	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢) ∨ 𝑠 = 𝑢))
134	63	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑆 Po 𝐵)
135	40	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑢 ∈ 𝐵)
136	65	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑠 ∈ 𝐵)
137		po2nr 5516	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 Po 𝐵 ∧ (𝑢 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵)) → ¬ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢))
138	134, 135, 136, 137	syl12anc 833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ¬ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢))
139	133, 138	orcnd 875	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑠 = 𝑢)
140	121, 139	jca 511	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))
141	103, 140	syl6bi 252	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
142	141	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
143	87, 142	syl5bir 242	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (¬ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
144	85, 143	mt3d 148	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))
145	62, 82, 144	3jca 1126	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))
146	37, 42, 145	3jca 1126	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))))
147	146	ex 412	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))))
148	31, 32, 147	syl2ani 606	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))))
149		breq12 5083	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩) → (𝑎𝑇𝑏 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑟, 𝑠⟩))
150	149	3adant3 1130	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑏 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑟, 𝑠⟩))
151	12	xpord2lem 33768	. . . . . . . . . . . . . 14 ⊢ (⟨𝑝, 𝑞⟩𝑇⟨𝑟, 𝑠⟩ ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))))
152	150, 151	bitrdi 286	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑏 ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)))))
153		breq12 5083	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑏𝑇𝑐 ↔ ⟨𝑟, 𝑠⟩𝑇⟨𝑡, 𝑢⟩))
154	153	3adant1 1128	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑏𝑇𝑐 ↔ ⟨𝑟, 𝑠⟩𝑇⟨𝑡, 𝑢⟩))
155	12	xpord2lem 33768	. . . . . . . . . . . . . 14 ⊢ (⟨𝑟, 𝑠⟩𝑇⟨𝑡, 𝑢⟩ ↔ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))))
156	154, 155	bitrdi 286	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑏𝑇𝑐 ↔ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))))
157	152, 156	anbi12d 630	. . . . . . . . . . . 12 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) ↔ (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))))))
158		breq12 5083	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑐 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑡, 𝑢⟩))
159	158	3adant2 1129	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑐 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑡, 𝑢⟩))
160	12	xpord2lem 33768	. . . . . . . . . . . . 13 ⊢ (⟨𝑝, 𝑞⟩𝑇⟨𝑡, 𝑢⟩ ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))))
161	159, 160	bitrdi 286	. . . . . . . . . . . 12 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑐 ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))))
162	157, 161	imbi12d 344	. . . . . . . . . . 11 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐) ↔ ((((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))))))
163	148, 162	syl5ibrcom 246	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
164	30, 163	sylan2br 594	. . . . . . . . 9 ⊢ ((𝜑 ∧ (((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
165	164	anassrs 467	. . . . . . . 8 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵))) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) → ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
166	165	rexlimdvva 3224	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵))) → (∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
167	166	anassrs 467	. . . . . 6 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵)) → (∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
168	167	rexlimdvva 3224	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) → (∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
169	168	rexlimdvva 3224	. . . 4 ⊢ (𝜑 → (∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
170	169	imp 406	. . 3 ⊢ ((𝜑 ∧ ∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩)) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐))
171	29, 170	sylan2b 593	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑏 ∈ (𝐴 × 𝐵) ∧ 𝑐 ∈ (𝐴 × 𝐵))) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐))
172	21, 171	ispod 5511	1 ⊢ (𝜑 → 𝑇 Po (𝐴 × 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 ∧ w3a 1085 = wceq 1541 ∈ wcel 2109 ≠ wne 2944 ∃wrex 3066 ⟨cop 4572 class class class wbr 5078 {copab 5140 Po wpo 5500 × cxp 5586 ‘cfv 6430 1^st c1st 7815 2^nd c2nd 7816

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1801 ax-4 1815 ax-5 1916 ax-6 1974 ax-7 2014 ax-8 2111 ax-9 2119 ax-10 2140 ax-11 2157 ax-12 2174 ax-ext 2710 ax-sep 5226 ax-nul 5233 ax-pr 5355 ax-un 7579

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1544 df-fal 1554 df-ex 1786 df-nf 1790 df-sb 2071 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2817 df-nfc 2890 df-ne 2945 df-ral 3070 df-rex 3071 df-rab 3074 df-v 3432 df-dif 3894 df-un 3896 df-in 3898 df-ss 3908 df-nul 4262 df-if 4465 df-sn 4567 df-pr 4569 df-op 4573 df-uni 4845 df-br 5079 df-opab 5141 df-mpt 5162 df-id 5488 df-po 5502 df-xp 5594 df-rel 5595 df-cnv 5596 df-co 5597 df-dm 5598 df-rn 5599 df-iota 6388 df-fun 6432 df-fv 6438 df-1st 7817 df-2nd 7818

This theorem is referenced by: xpord2ind 33773 on2recsfn 33805 on2recsov 33806 noxpordpo 34086

W3C validator