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 8083

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 5642	. . . 4 ⊢ (𝑎 ∈ (𝐴 × 𝐵) ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩)
2		equid 2019	. . . . . . . . . . . 12 ⊢ 𝑝 = 𝑝
3		equid 2019	. . . . . . . . . . . 12 ⊢ 𝑞 = 𝑞
4	2, 3	pm3.2i 471	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑝 ∧ 𝑞 = 𝑞)
5		neorian 3029	. . . . . . . . . . . 12 ⊢ ((𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞) ↔ ¬ (𝑝 = 𝑝 ∧ 𝑞 = 𝑞))
6	5	con2bii 358	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑝 ∧ 𝑞 = 𝑞) ↔ ¬ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))
7	4, 6	mpbi 231	. . . . . . . . . 10 ⊢ ¬ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)
8		simp3 1144	. . . . . . . . . 10 ⊢ (((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)) → (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))
9	7, 8	mto 198	. . . . . . . . 9 ⊢ ¬ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))
10		simp3 1144	. . . . . . . . 9 ⊢ (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))) → ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)))
11	9, 10	mto 198	. . . . . . . 8 ⊢ ¬ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)))
12		xpord2.1	. . . . . . . . 9 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥)𝑆(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}
13	12	xpord2lem 8082	. . . . . . . 8 ⊢ (⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩ ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))))
14	11, 13	mtbir 324	. . . . . . 7 ⊢ ¬ ⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩
15		breq12 5077	. . . . . . . 8 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑎 = ⟨𝑝, 𝑞⟩) → (𝑎𝑇𝑎 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩))
16	15	anidms 571	. . . . . . 7 ⊢ (𝑎 = ⟨𝑝, 𝑞⟩ → (𝑎𝑇𝑎 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩))
17	14, 16	mtbiri 328	. . . . . 6 ⊢ (𝑎 = ⟨𝑝, 𝑞⟩ → ¬ 𝑎𝑇𝑎)
18	17	rexlimivw 3136	. . . . 5 ⊢ (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ → ¬ 𝑎𝑇𝑎)
19	18	rexlimivw 3136	. . . 4 ⊢ (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ → ¬ 𝑎𝑇𝑎)
20	1, 19	sylbi 218	. . 3 ⊢ (𝑎 ∈ (𝐴 × 𝐵) → ¬ 𝑎𝑇𝑎)
21	20	adantl 482	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐴 × 𝐵)) → ¬ 𝑎𝑇𝑎)
22		3reeanv 3212	. . . 4 ⊢ (∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩) ↔ (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑡 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
23		3reeanv 3212	. . . . . 6 ⊢ (∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) ↔ (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
24	23	rexbii 3086	. . . . 5 ⊢ (∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) ↔ ∃𝑡 ∈ 𝐴 (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
25	24	2rexbii 3115	. . . 4 ⊢ (∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) ↔ ∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
26		elxp2 5642	. . . . 5 ⊢ (𝑏 ∈ (𝐴 × 𝐵) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩)
27		elxp2 5642	. . . . 5 ⊢ (𝑐 ∈ (𝐴 × 𝐵) ↔ ∃𝑡 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩)
28	1, 26, 27	3anbi123i 1161	. . . 4 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑏 ∈ (𝐴 × 𝐵) ∧ 𝑐 ∈ (𝐴 × 𝐵)) ↔ (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑡 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
29	22, 25, 28	3bitr4ri 305	. . 3 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑏 ∈ (𝐴 × 𝐵) ∧ 𝑐 ∈ (𝐴 × 𝐵)) ↔ ∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩))
30		df-3an 1094	. . . . . . . . . 10 ⊢ (((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) ↔ (((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)))
31		simp3 1144	. . . . . . . . . . . 12 ⊢ (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)))
32		simp3 1144	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))) → ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))
33		simpr1l 1237	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑝 ∈ 𝐴)
34	33	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑝 ∈ 𝐴)
35		simpr2r 1240	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑞 ∈ 𝐵)
36	35	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑞 ∈ 𝐵)
37	34, 36	jca 516	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵))
38		simpr2l 1239	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑡 ∈ 𝐴)
39	38	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑡 ∈ 𝐴)
40		simpr3r 1242	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑢 ∈ 𝐵)
41	40	adantr 481	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑢 ∈ 𝐵)
42	39, 41	jca 516	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵))
43		poxp2.1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑅 Po 𝐴)
44	43	ad2antrr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑅 Po 𝐴)
45		simpr1r 1238	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑟 ∈ 𝐴)
46	45	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑟 ∈ 𝐴)
47		potr 5539	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Po 𝐴 ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴)) → ((𝑝𝑅𝑟 ∧ 𝑟𝑅𝑡) → 𝑝𝑅𝑡))
48	44, 34, 46, 39, 47	syl13anc 1380	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝𝑅𝑟 ∧ 𝑟𝑅𝑡) → 𝑝𝑅𝑡))
49		orc 873	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))
50	48, 49	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝𝑅𝑟 ∧ 𝑟𝑅𝑡) → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
51	50	expd 416	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝𝑅𝑟 → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))))
52		breq1 5075	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑟 → (𝑝𝑅𝑡 ↔ 𝑟𝑅𝑡))
53	52, 49	biimtrrdi 255	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑟 → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
54	53	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝 = 𝑟 → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))))
55		simprl1 1225	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝𝑅𝑟 ∨ 𝑝 = 𝑟))
56	51, 54, 55	mpjaod 866	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
57		breq2 5076	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑡 → (𝑝𝑅𝑟 ↔ 𝑝𝑅𝑡))
58		equequ2 2033	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑡 → (𝑝 = 𝑟 ↔ 𝑝 = 𝑡))
59	57, 58	orbi12d 924	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑡 → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ↔ (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
60	55, 59	syl5ibcom 246	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 = 𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
61		simprr1 1228	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡))
62	56, 60, 61	mpjaod 866	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))
63		poxp2.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑆 Po 𝐵)
64	63	ad2antrr 732	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑆 Po 𝐵)
65		simpr3l 1241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑠 ∈ 𝐵)
66	65	adantr 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑠 ∈ 𝐵)
67		potr 5539	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 Po 𝐵 ∧ (𝑞 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) → ((𝑞𝑆𝑠 ∧ 𝑠𝑆𝑢) → 𝑞𝑆𝑢))
68	64, 36, 66, 41, 67	syl13anc 1380	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑞𝑆𝑠 ∧ 𝑠𝑆𝑢) → 𝑞𝑆𝑢))
69		orc 873	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))
70	68, 69	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑞𝑆𝑠 ∧ 𝑠𝑆𝑢) → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
71	70	expd 416	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞𝑆𝑠 → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))))
72		breq1 5075	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = 𝑠 → (𝑞𝑆𝑢 ↔ 𝑠𝑆𝑢))
73	72, 69	biimtrrdi 255	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = 𝑠 → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
74	73	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞 = 𝑠 → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))))
75		simprl2 1226	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠))
76	71, 74, 75	mpjaod 866	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
77		breq2 5076	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑢 → (𝑞𝑆𝑠 ↔ 𝑞𝑆𝑢))
78		equequ2 2033	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑢 → (𝑞 = 𝑠 ↔ 𝑞 = 𝑢))
79	77, 78	orbi12d 924	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑢 → ((𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ↔ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
80	75, 79	syl5ibcom 246	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠 = 𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
81		simprr2 1229	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢))
82	76, 80, 81	mpjaod 866	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))
83		simprr3 1230	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))
84		neorian 3029	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢) ↔ ¬ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))
85	83, 84	sylib 219	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ¬ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))
86		neorian 3029	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢) ↔ ¬ (𝑝 = 𝑡 ∧ 𝑞 = 𝑢))
87	86	con2bii 358	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) ↔ ¬ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))
88		breq1 5075	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑡 → (𝑝𝑅𝑟 ↔ 𝑡𝑅𝑟))
89		equequ1 2032	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑡 → (𝑝 = 𝑟 ↔ 𝑡 = 𝑟))
90	88, 89	orbi12d 924	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = 𝑡 → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟)))
91	90	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟)))
92		breq1 5075	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑢 → (𝑞𝑆𝑠 ↔ 𝑢𝑆𝑠))
93		equequ1 2032	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑢 → (𝑞 = 𝑠 ↔ 𝑢 = 𝑠))
94	92, 93	orbi12d 924	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 = 𝑢 → ((𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠)))
95	94	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠)))
96		neeq1 2996	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑡 → (𝑝 ≠ 𝑟 ↔ 𝑡 ≠ 𝑟))
97	96	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (𝑝 ≠ 𝑟 ↔ 𝑡 ≠ 𝑟))
98		neeq1 2996	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑢 → (𝑞 ≠ 𝑠 ↔ 𝑢 ≠ 𝑠))
99	98	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (𝑞 ≠ 𝑠 ↔ 𝑢 ≠ 𝑠))
100	97, 99	orbi12d 924	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠) ↔ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)))
101	91, 95, 100	3anbi123d 1444	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ↔ ((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠))))
102	101	anbi1d 637	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))) ↔ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))))
103	102	anbi2d 636	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) ↔ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))))))
104		simprl1 1225	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟))
105		simprr1 1228	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡))
106		orcom 876	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡) ∨ 𝑟 = 𝑡) ↔ (𝑟 = 𝑡 ∨ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡)))
107		ordi 1013	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑟 = 𝑡 ∨ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡)) ↔ ((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ∧ (𝑟 = 𝑡 ∨ 𝑟𝑅𝑡)))
108		orcom 876	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑟 = 𝑡))
109		equcom 2025	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑟 = 𝑡 ↔ 𝑡 = 𝑟)
110	109	orbi2i 918	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡𝑅𝑟 ∨ 𝑟 = 𝑡) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟))
111	108, 110	bitri 276	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟))
112		orcom 876	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑟 = 𝑡 ∨ 𝑟𝑅𝑡) ↔ (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡))
113	111, 112	anbi12i 634	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ∧ (𝑟 = 𝑡 ∨ 𝑟𝑅𝑡)) ↔ ((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡)))
114	106, 107, 113	3bitri 298	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡) ∨ 𝑟 = 𝑡) ↔ ((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡)))
115	104, 105, 114	sylanbrc 589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡) ∨ 𝑟 = 𝑡))
116	43	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑅 Po 𝐴)
117	38	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑡 ∈ 𝐴)
118	45	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑟 ∈ 𝐴)
119		po2nr 5540	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po 𝐴 ∧ (𝑡 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) → ¬ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡))
120	116, 117, 118, 119	syl12anc 842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ¬ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡))
121	115, 120	orcnd 884	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑟 = 𝑡)
122		simprl2 1226	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠))
123		simprr2 1229	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢))
124		orcom 876	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢) ∨ 𝑠 = 𝑢) ↔ (𝑠 = 𝑢 ∨ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢)))
125		ordi 1013	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 = 𝑢 ∨ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢)) ↔ ((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ∧ (𝑠 = 𝑢 ∨ 𝑠𝑆𝑢)))
126		orcom 876	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑠 = 𝑢))
127		equcom 2025	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = 𝑢 ↔ 𝑢 = 𝑠)
128	127	orbi2i 918	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢𝑆𝑠 ∨ 𝑠 = 𝑢) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠))
129	126, 128	bitri 276	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠))
130		orcom 876	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 = 𝑢 ∨ 𝑠𝑆𝑢) ↔ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢))
131	129, 130	anbi12i 634	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ∧ (𝑠 = 𝑢 ∨ 𝑠𝑆𝑢)) ↔ ((𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢)))
132	124, 125, 131	3bitri 298	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢) ∨ 𝑠 = 𝑢) ↔ ((𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢)))
133	122, 123, 132	sylanbrc 589	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢) ∨ 𝑠 = 𝑢))
134	63	ad2antrr 732	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑆 Po 𝐵)
135	40	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑢 ∈ 𝐵)
136	65	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑠 ∈ 𝐵)
137		po2nr 5540	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 Po 𝐵 ∧ (𝑢 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵)) → ¬ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢))
138	134, 135, 136, 137	syl12anc 842	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ¬ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢))
139	133, 138	orcnd 884	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑠 = 𝑢)
140	121, 139	jca 516	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))
141	103, 140	biimtrdi 254	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
142	141	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
143	87, 142	biimtrrid 244	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (¬ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
144	85, 143	mt3d 148	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))
145	62, 82, 144	3jca 1134	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))
146	37, 42, 145	3jca 1134	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))))
147	146	ex 413	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))))
148	31, 32, 147	syl2ani 613	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))))
149		breq12 5077	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩) → (𝑎𝑇𝑏 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑟, 𝑠⟩))
150	149	3adant3 1138	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑏 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑟, 𝑠⟩))
151	12	xpord2lem 8082	. . . . . . . . . . . . . 14 ⊢ (⟨𝑝, 𝑞⟩𝑇⟨𝑟, 𝑠⟩ ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))))
152	150, 151	bitrdi 288	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑏 ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)))))
153		breq12 5077	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑏𝑇𝑐 ↔ ⟨𝑟, 𝑠⟩𝑇⟨𝑡, 𝑢⟩))
154	153	3adant1 1136	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑏𝑇𝑐 ↔ ⟨𝑟, 𝑠⟩𝑇⟨𝑡, 𝑢⟩))
155	12	xpord2lem 8082	. . . . . . . . . . . . . 14 ⊢ (⟨𝑟, 𝑠⟩𝑇⟨𝑡, 𝑢⟩ ↔ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))))
156	154, 155	bitrdi 288	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑏𝑇𝑐 ↔ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))))
157	152, 156	anbi12d 638	. . . . . . . . . . . 12 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) ↔ (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))))))
158		breq12 5077	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑐 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑡, 𝑢⟩))
159	158	3adant2 1137	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑐 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑡, 𝑢⟩))
160	12	xpord2lem 8082	. . . . . . . . . . . . 13 ⊢ (⟨𝑝, 𝑞⟩𝑇⟨𝑡, 𝑢⟩ ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))))
161	159, 160	bitrdi 288	. . . . . . . . . . . 12 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑐 ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))))
162	157, 161	imbi12d 345	. . . . . . . . . . 11 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐) ↔ ((((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))))))
163	148, 162	syl5ibrcom 248	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
164	30, 163	sylan2br 601	. . . . . . . . 9 ⊢ ((𝜑 ∧ (((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
165	164	anassrs 468	. . . . . . . 8 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵))) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) → ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
166	165	rexlimdvva 3196	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵))) → (∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
167	166	anassrs 468	. . . . . 6 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵)) → (∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
168	167	rexlimdvva 3196	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) → (∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
169	168	rexlimdvva 3196	. . . 4 ⊢ (𝜑 → (∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
170	169	imp 407	. . 3 ⊢ ((𝜑 ∧ ∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩)) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐))
171	29, 170	sylan2b 600	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑏 ∈ (𝐴 × 𝐵) ∧ 𝑐 ∈ (𝐴 × 𝐵))) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐))
172	21, 171	ispod 5535	1 ⊢ (𝜑 → 𝑇 Po (𝐴 × 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∨ wo 853 ∧ w3a 1092 = wceq 1547 ∈ wcel 2119 ≠ wne 2934 ∃wrex 3063 ⟨cop 4561 class class class wbr 5072 {copab 5134 Po wpo 5524 × cxp 5616 ‘cfv 6485 1^st c1st 7929 2^nd c2nd 7930

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-sep 5218 ax-nul 5228 ax-pr 5362 ax-un 7678

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-ral 3054 df-rex 3064 df-rab 3392 df-v 3433 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4262 df-if 4455 df-sn 4556 df-pr 4558 df-op 4562 df-uni 4839 df-br 5073 df-opab 5135 df-mpt 5154 df-id 5513 df-po 5526 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-iota 6441 df-fun 6487 df-fv 6493 df-1st 7931 df-2nd 7932

This theorem is referenced by: xpord2indlem 8087 on2recsfn 8593 on2recsov 8594 noxpordpo 27960

W3C validator