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 8168

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 5709	. . . 4 ⊢ (𝑎 ∈ (𝐴 × 𝐵) ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩)
2		equid 2011	. . . . . . . . . . . 12 ⊢ 𝑝 = 𝑝
3		equid 2011	. . . . . . . . . . . 12 ⊢ 𝑞 = 𝑞
4	2, 3	pm3.2i 470	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑝 ∧ 𝑞 = 𝑞)
5		neorian 3037	. . . . . . . . . . . 12 ⊢ ((𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞) ↔ ¬ (𝑝 = 𝑝 ∧ 𝑞 = 𝑞))
6	5	con2bii 357	. . . . . . . . . . 11 ⊢ ((𝑝 = 𝑝 ∧ 𝑞 = 𝑞) ↔ ¬ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))
7	4, 6	mpbi 230	. . . . . . . . . 10 ⊢ ¬ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)
8		simp3 1139	. . . . . . . . . 10 ⊢ (((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)) → (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))
9	7, 8	mto 197	. . . . . . . . 9 ⊢ ¬ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))
10		simp3 1139	. . . . . . . . 9 ⊢ (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))) → ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)))
11	9, 10	mto 197	. . . . . . . 8 ⊢ ¬ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞)))
12		xpord2.1	. . . . . . . . 9 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ (1^st ‘𝑥) = (1^st ‘𝑦)) ∧ ((2^nd ‘𝑥)𝑆(2^nd ‘𝑦) ∨ (2^nd ‘𝑥) = (2^nd ‘𝑦)) ∧ 𝑥 ≠ 𝑦))}
13	12	xpord2lem 8167	. . . . . . . 8 ⊢ (⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩ ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ ((𝑝𝑅𝑝 ∨ 𝑝 = 𝑝) ∧ (𝑞𝑆𝑞 ∨ 𝑞 = 𝑞) ∧ (𝑝 ≠ 𝑝 ∨ 𝑞 ≠ 𝑞))))
14	11, 13	mtbir 323	. . . . . . 7 ⊢ ¬ ⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩
15		breq12 5148	. . . . . . . 8 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑎 = ⟨𝑝, 𝑞⟩) → (𝑎𝑇𝑎 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩))
16	15	anidms 566	. . . . . . 7 ⊢ (𝑎 = ⟨𝑝, 𝑞⟩ → (𝑎𝑇𝑎 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑝, 𝑞⟩))
17	14, 16	mtbiri 327	. . . . . 6 ⊢ (𝑎 = ⟨𝑝, 𝑞⟩ → ¬ 𝑎𝑇𝑎)
18	17	rexlimivw 3151	. . . . 5 ⊢ (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ → ¬ 𝑎𝑇𝑎)
19	18	rexlimivw 3151	. . . 4 ⊢ (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ → ¬ 𝑎𝑇𝑎)
20	1, 19	sylbi 217	. . 3 ⊢ (𝑎 ∈ (𝐴 × 𝐵) → ¬ 𝑎𝑇𝑎)
21	20	adantl 481	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ (𝐴 × 𝐵)) → ¬ 𝑎𝑇𝑎)
22		3reeanv 3230	. . . 4 ⊢ (∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩) ↔ (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑡 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
23		3reeanv 3230	. . . . . 6 ⊢ (∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) ↔ (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
24	23	rexbii 3094	. . . . 5 ⊢ (∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) ↔ ∃𝑡 ∈ 𝐴 (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
25	24	2rexbii 3129	. . . 4 ⊢ (∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) ↔ ∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 (∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
26		elxp2 5709	. . . . 5 ⊢ (𝑏 ∈ (𝐴 × 𝐵) ↔ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩)
27		elxp2 5709	. . . . 5 ⊢ (𝑐 ∈ (𝐴 × 𝐵) ↔ ∃𝑡 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩)
28	1, 26, 27	3anbi123i 1156	. . . 4 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑏 ∈ (𝐴 × 𝐵) ∧ 𝑐 ∈ (𝐴 × 𝐵)) ↔ (∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐵 𝑎 = ⟨𝑝, 𝑞⟩ ∧ ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐵 𝑏 = ⟨𝑟, 𝑠⟩ ∧ ∃𝑡 ∈ 𝐴 ∃𝑢 ∈ 𝐵 𝑐 = ⟨𝑡, 𝑢⟩))
29	22, 25, 28	3bitr4ri 304	. . 3 ⊢ ((𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑏 ∈ (𝐴 × 𝐵) ∧ 𝑐 ∈ (𝐴 × 𝐵)) ↔ ∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩))
30		df-3an 1089	. . . . . . . . . 10 ⊢ (((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) ↔ (((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)))
31		simp3 1139	. . . . . . . . . . . 12 ⊢ (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)))
32		simp3 1139	. . . . . . . . . . . 12 ⊢ (((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))) → ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))
33		simpr1l 1231	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑝 ∈ 𝐴)
34	33	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑝 ∈ 𝐴)
35		simpr2r 1234	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑞 ∈ 𝐵)
36	35	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑞 ∈ 𝐵)
37	34, 36	jca 511	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵))
38		simpr2l 1233	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑡 ∈ 𝐴)
39	38	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑡 ∈ 𝐴)
40		simpr3r 1236	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑢 ∈ 𝐵)
41	40	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑢 ∈ 𝐵)
42	39, 41	jca 511	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵))
43		poxp2.1	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑅 Po 𝐴)
44	43	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑅 Po 𝐴)
45		simpr1r 1232	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑟 ∈ 𝐴)
46	45	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑟 ∈ 𝐴)
47		potr 5605	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑅 Po 𝐴 ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑡 ∈ 𝐴)) → ((𝑝𝑅𝑟 ∧ 𝑟𝑅𝑡) → 𝑝𝑅𝑡))
48	44, 34, 46, 39, 47	syl13anc 1374	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝𝑅𝑟 ∧ 𝑟𝑅𝑡) → 𝑝𝑅𝑡))
49		orc 868	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))
50	48, 49	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝𝑅𝑟 ∧ 𝑟𝑅𝑡) → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
51	50	expd 415	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝𝑅𝑟 → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))))
52		breq1 5146	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑟 → (𝑝𝑅𝑡 ↔ 𝑟𝑅𝑡))
53	52, 49	biimtrrdi 254	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑟 → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
54	53	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝 = 𝑟 → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))))
55		simprl1 1219	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝𝑅𝑟 ∨ 𝑝 = 𝑟))
56	51, 54, 55	mpjaod 861	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟𝑅𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
57		breq2 5147	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑡 → (𝑝𝑅𝑟 ↔ 𝑝𝑅𝑡))
58		equequ2 2025	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑡 → (𝑝 = 𝑟 ↔ 𝑝 = 𝑡))
59	57, 58	orbi12d 919	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑡 → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ↔ (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
60	55, 59	syl5ibcom 245	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 = 𝑡 → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡)))
61		simprr1 1222	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡))
62	56, 60, 61	mpjaod 861	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝𝑅𝑡 ∨ 𝑝 = 𝑡))
63		poxp2.2	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → 𝑆 Po 𝐵)
64	63	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑆 Po 𝐵)
65		simpr3l 1235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → 𝑠 ∈ 𝐵)
66	65	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑠 ∈ 𝐵)
67		potr 5605	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑆 Po 𝐵 ∧ (𝑞 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) → ((𝑞𝑆𝑠 ∧ 𝑠𝑆𝑢) → 𝑞𝑆𝑢))
68	64, 36, 66, 41, 67	syl13anc 1374	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑞𝑆𝑠 ∧ 𝑠𝑆𝑢) → 𝑞𝑆𝑢))
69		orc 868	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))
70	68, 69	syl6 35	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑞𝑆𝑠 ∧ 𝑠𝑆𝑢) → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
71	70	expd 415	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞𝑆𝑠 → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))))
72		breq1 5146	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑞 = 𝑠 → (𝑞𝑆𝑢 ↔ 𝑠𝑆𝑢))
73	72, 69	biimtrrdi 254	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 = 𝑠 → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
74	73	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞 = 𝑠 → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))))
75		simprl2 1220	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠))
76	71, 74, 75	mpjaod 861	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠𝑆𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
77		breq2 5147	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑢 → (𝑞𝑆𝑠 ↔ 𝑞𝑆𝑢))
78		equequ2 2025	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑠 = 𝑢 → (𝑞 = 𝑠 ↔ 𝑞 = 𝑢))
79	77, 78	orbi12d 919	. . . . . . . . . . . . . . . . 17 ⊢ (𝑠 = 𝑢 → ((𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ↔ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
80	75, 79	syl5ibcom 245	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠 = 𝑢 → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢)))
81		simprr2 1223	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢))
82	76, 80, 81	mpjaod 861	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢))
83		simprr3 1224	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))
84		neorian 3037	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢) ↔ ¬ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))
85	83, 84	sylib 218	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ¬ (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))
86		neorian 3037	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢) ↔ ¬ (𝑝 = 𝑡 ∧ 𝑞 = 𝑢))
87	86	con2bii 357	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) ↔ ¬ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))
88		breq1 5146	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑡 → (𝑝𝑅𝑟 ↔ 𝑡𝑅𝑟))
89		equequ1 2024	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑡 → (𝑝 = 𝑟 ↔ 𝑡 = 𝑟))
90	88, 89	orbi12d 919	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑝 = 𝑡 → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟)))
91	90	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟)))
92		breq1 5146	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑢 → (𝑞𝑆𝑠 ↔ 𝑢𝑆𝑠))
93		equequ1 2024	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑢 → (𝑞 = 𝑠 ↔ 𝑢 = 𝑠))
94	92, 93	orbi12d 919	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑞 = 𝑢 → ((𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠)))
95	94	adantl 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠)))
96		neeq1 3003	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑝 = 𝑡 → (𝑝 ≠ 𝑟 ↔ 𝑡 ≠ 𝑟))
97	96	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (𝑝 ≠ 𝑟 ↔ 𝑡 ≠ 𝑟))
98		neeq1 3003	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑞 = 𝑢 → (𝑞 ≠ 𝑠 ↔ 𝑢 ≠ 𝑠))
99	98	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (𝑞 ≠ 𝑠 ↔ 𝑢 ≠ 𝑠))
100	97, 99	orbi12d 919	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠) ↔ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)))
101	91, 95, 100	3anbi123d 1438	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ↔ ((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠))))
102	101	anbi1d 631	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → ((((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))) ↔ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))))
103	102	anbi2d 630	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) ↔ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))))))
104		simprl1 1219	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟))
105		simprr1 1222	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡))
106		orcom 871	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡) ∨ 𝑟 = 𝑡) ↔ (𝑟 = 𝑡 ∨ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡)))
107		ordi 1008	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑟 = 𝑡 ∨ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡)) ↔ ((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ∧ (𝑟 = 𝑡 ∨ 𝑟𝑅𝑡)))
108		orcom 871	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑟 = 𝑡))
109		equcom 2017	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑟 = 𝑡 ↔ 𝑡 = 𝑟)
110	109	orbi2i 913	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡𝑅𝑟 ∨ 𝑟 = 𝑡) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟))
111	108, 110	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ↔ (𝑡𝑅𝑟 ∨ 𝑡 = 𝑟))
112		orcom 871	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑟 = 𝑡 ∨ 𝑟𝑅𝑡) ↔ (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡))
113	111, 112	anbi12i 628	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑟 = 𝑡 ∨ 𝑡𝑅𝑟) ∧ (𝑟 = 𝑡 ∨ 𝑟𝑅𝑡)) ↔ ((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡)))
114	106, 107, 113	3bitri 297	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡) ∨ 𝑟 = 𝑡) ↔ ((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑟𝑅𝑡 ∨ 𝑟 = 𝑡)))
115	104, 105, 114	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡) ∨ 𝑟 = 𝑡))
116	43	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑅 Po 𝐴)
117	38	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑡 ∈ 𝐴)
118	45	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑟 ∈ 𝐴)
119		po2nr 5606	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑅 Po 𝐴 ∧ (𝑡 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) → ¬ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡))
120	116, 117, 118, 119	syl12anc 837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ¬ (𝑡𝑅𝑟 ∧ 𝑟𝑅𝑡))
121	115, 120	orcnd 879	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑟 = 𝑡)
122		simprl2 1220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠))
123		simprr2 1223	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢))
124		orcom 871	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢) ∨ 𝑠 = 𝑢) ↔ (𝑠 = 𝑢 ∨ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢)))
125		ordi 1008	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑠 = 𝑢 ∨ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢)) ↔ ((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ∧ (𝑠 = 𝑢 ∨ 𝑠𝑆𝑢)))
126		orcom 871	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑠 = 𝑢))
127		equcom 2017	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑠 = 𝑢 ↔ 𝑢 = 𝑠)
128	127	orbi2i 913	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢𝑆𝑠 ∨ 𝑠 = 𝑢) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠))
129	126, 128	bitri 275	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ↔ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠))
130		orcom 871	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑠 = 𝑢 ∨ 𝑠𝑆𝑢) ↔ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢))
131	129, 130	anbi12i 628	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑠 = 𝑢 ∨ 𝑢𝑆𝑠) ∧ (𝑠 = 𝑢 ∨ 𝑠𝑆𝑢)) ↔ ((𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢)))
132	124, 125, 131	3bitri 297	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢) ∨ 𝑠 = 𝑢) ↔ ((𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢)))
133	122, 123, 132	sylanbrc 583	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢) ∨ 𝑠 = 𝑢))
134	63	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑆 Po 𝐵)
135	40	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑢 ∈ 𝐵)
136	65	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑠 ∈ 𝐵)
137		po2nr 5606	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑆 Po 𝐵 ∧ (𝑢 ∈ 𝐵 ∧ 𝑠 ∈ 𝐵)) → ¬ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢))
138	134, 135, 136, 137	syl12anc 837	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ¬ (𝑢𝑆𝑠 ∧ 𝑠𝑆𝑢))
139	133, 138	orcnd 879	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → 𝑠 = 𝑢)
140	121, 139	jca 511	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑡𝑅𝑟 ∨ 𝑡 = 𝑟) ∧ (𝑢𝑆𝑠 ∨ 𝑢 = 𝑠) ∧ (𝑡 ≠ 𝑟 ∨ 𝑢 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢))
141	103, 140	biimtrdi 253	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
142	141	com12 32	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 = 𝑡 ∧ 𝑞 = 𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
143	87, 142	biimtrrid 243	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (¬ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢) → (𝑟 = 𝑡 ∧ 𝑠 = 𝑢)))
144	85, 143	mt3d 148	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))
145	62, 82, 144	3jca 1129	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))
146	37, 42, 145	3jca 1129	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) ∧ (((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))))
147	146	ex 412	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))))
148	31, 32, 147	syl2ani 607	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))))
149		breq12 5148	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩) → (𝑎𝑇𝑏 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑟, 𝑠⟩))
150	149	3adant3 1133	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑏 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑟, 𝑠⟩))
151	12	xpord2lem 8167	. . . . . . . . . . . . . 14 ⊢ (⟨𝑝, 𝑞⟩𝑇⟨𝑟, 𝑠⟩ ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))))
152	150, 151	bitrdi 287	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑏 ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠)))))
153		breq12 5148	. . . . . . . . . . . . . . 15 ⊢ ((𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑏𝑇𝑐 ↔ ⟨𝑟, 𝑠⟩𝑇⟨𝑡, 𝑢⟩))
154	153	3adant1 1131	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑏𝑇𝑐 ↔ ⟨𝑟, 𝑠⟩𝑇⟨𝑡, 𝑢⟩))
155	12	xpord2lem 8167	. . . . . . . . . . . . . 14 ⊢ (⟨𝑟, 𝑠⟩𝑇⟨𝑡, 𝑢⟩ ↔ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))))
156	154, 155	bitrdi 287	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑏𝑇𝑐 ↔ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))))
157	152, 156	anbi12d 632	. . . . . . . . . . . 12 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) ↔ (((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢))))))
158		breq12 5148	. . . . . . . . . . . . . 14 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑐 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑡, 𝑢⟩))
159	158	3adant2 1132	. . . . . . . . . . . . 13 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑐 ↔ ⟨𝑝, 𝑞⟩𝑇⟨𝑡, 𝑢⟩))
160	12	xpord2lem 8167	. . . . . . . . . . . . 13 ⊢ (⟨𝑝, 𝑞⟩𝑇⟨𝑡, 𝑢⟩ ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))))
161	159, 160	bitrdi 287	. . . . . . . . . . . 12 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (𝑎𝑇𝑐 ↔ ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢)))))
162	157, 161	imbi12d 344	. . . . . . . . . . 11 ⊢ ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → (((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐) ↔ ((((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ ((𝑝𝑅𝑟 ∨ 𝑝 = 𝑟) ∧ (𝑞𝑆𝑠 ∨ 𝑞 = 𝑠) ∧ (𝑝 ≠ 𝑟 ∨ 𝑞 ≠ 𝑠))) ∧ ((𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑟𝑅𝑡 ∨ 𝑟 = 𝑡) ∧ (𝑠𝑆𝑢 ∨ 𝑠 = 𝑢) ∧ (𝑟 ≠ 𝑡 ∨ 𝑠 ≠ 𝑢)))) → ((𝑝 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑡 ∈ 𝐴 ∧ 𝑢 ∈ 𝐵) ∧ ((𝑝𝑅𝑡 ∨ 𝑝 = 𝑡) ∧ (𝑞𝑆𝑢 ∨ 𝑞 = 𝑢) ∧ (𝑝 ≠ 𝑡 ∨ 𝑞 ≠ 𝑢))))))
163	148, 162	syl5ibrcom 247	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
164	30, 163	sylan2br 595	. . . . . . . . 9 ⊢ ((𝜑 ∧ (((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵)) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵))) → ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
165	164	anassrs 467	. . . . . . . 8 ⊢ (((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵))) ∧ (𝑠 ∈ 𝐵 ∧ 𝑢 ∈ 𝐵)) → ((𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
166	165	rexlimdvva 3213	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵))) → (∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
167	166	anassrs 467	. . . . . 6 ⊢ (((𝜑 ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ (𝑡 ∈ 𝐴 ∧ 𝑞 ∈ 𝐵)) → (∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
168	167	rexlimdvva 3213	. . . . 5 ⊢ ((𝜑 ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) → (∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
169	168	rexlimdvva 3213	. . . 4 ⊢ (𝜑 → (∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐)))
170	169	imp 406	. . 3 ⊢ ((𝜑 ∧ ∃𝑝 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑡 ∈ 𝐴 ∃𝑞 ∈ 𝐵 ∃𝑠 ∈ 𝐵 ∃𝑢 ∈ 𝐵 (𝑎 = ⟨𝑝, 𝑞⟩ ∧ 𝑏 = ⟨𝑟, 𝑠⟩ ∧ 𝑐 = ⟨𝑡, 𝑢⟩)) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐))
171	29, 170	sylan2b 594	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ (𝐴 × 𝐵) ∧ 𝑏 ∈ (𝐴 × 𝐵) ∧ 𝑐 ∈ (𝐴 × 𝐵))) → ((𝑎𝑇𝑏 ∧ 𝑏𝑇𝑐) → 𝑎𝑇𝑐))
172	21, 171	ispod 5601	1 ⊢ (𝜑 → 𝑇 Po (𝐴 × 𝐵))

Colors of variables: wff setvar class

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

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

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

This theorem is referenced by: xpord2indlem 8172 on2recsfn 8705 on2recsov 8706 noxpordpo 27983

W3C validator