poxp - Metamath Proof Explorer

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

Theorem poxp 8101

Description: A lexicographical ordering of two posets. (Contributed by Scott Fenton, 16-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.)

**Hypothesis**
Ref	Expression
poxp.1	⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥)𝑆(2^nd ‘𝑦))))}

**Assertion**
Ref	Expression
poxp	⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))

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

Proof of Theorem poxp Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑡 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp 5695	. . . . . . . 8 ⊢ (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)))
2		elxp 5695	. . . . . . . 8 ⊢ (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)))
3		elxp 5695	. . . . . . . 8 ⊢ (𝑣 ∈ (𝐴 × 𝐵) ↔ ∃𝑒∃𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)))
4		3an6 1447	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) ↔ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))))
5		poirr 5596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑅 Po 𝐴 ∧ 𝑎 ∈ 𝐴) → ¬ 𝑎𝑅𝑎)
6	5	ex 414	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑅 Po 𝐴 → (𝑎 ∈ 𝐴 → ¬ 𝑎𝑅𝑎))
7		poirr 5596	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆 Po 𝐵 ∧ 𝑏 ∈ 𝐵) → ¬ 𝑏𝑆𝑏)
8	7	intnand 490	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆 Po 𝐵 ∧ 𝑏 ∈ 𝐵) → ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))
9	8	ex 414	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑆 Po 𝐵 → (𝑏 ∈ 𝐵 → ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))
10	6, 9	im2anan9 621	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
11		ioran 983	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)) ↔ (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))
12	10, 11	syl6ibr 252	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
13	12	imp 408	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))
14	13	intnand 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
15	14	3ad2antr1 1189	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
16		an4 655	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ ((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))))
17		3an6 1447	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
18		potr 5597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) → ((𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒) → 𝑎𝑅𝑒))
19	18	3impia 1118	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒)) → 𝑎𝑅𝑒)
20	19	orcd 872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))
21	20	3expia 1122	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) → ((𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
22	21	expdimp 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ 𝑎𝑅𝑐) → (𝑐𝑅𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
23		breq2 5148	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = 𝑒 → (𝑎𝑅𝑐 ↔ 𝑎𝑅𝑒))
24	23	biimpa 478	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑐 = 𝑒 ∧ 𝑎𝑅𝑐) → 𝑎𝑅𝑒)
25	24	orcd 872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑐 = 𝑒 ∧ 𝑎𝑅𝑐) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))
26	25	expcom 415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎𝑅𝑐 → (𝑐 = 𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
27	26	adantrd 493	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑎𝑅𝑐 → ((𝑐 = 𝑒 ∧ 𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
28	27	adantl 483	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐 = 𝑒 ∧ 𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
29	22, 28	jaod 858	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
30	29	ex 414	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) → (𝑎𝑅𝑐 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
31		potr 5597	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → ((𝑏𝑆𝑑 ∧ 𝑑𝑆𝑓) → 𝑏𝑆𝑓))
32	31	expdimp 454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → (𝑑𝑆𝑓 → 𝑏𝑆𝑓))
33	32	anim2d 613	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐 = 𝑒 ∧ 𝑑𝑆𝑓) → (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓)))
34	33	orim2d 966	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓))))
35		breq1 5147	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑐 → (𝑎𝑅𝑒 ↔ 𝑐𝑅𝑒))
36		equequ1 2029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑎 = 𝑐 → (𝑎 = 𝑒 ↔ 𝑐 = 𝑒))
37	36	anbi1d 631	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑐 → ((𝑎 = 𝑒 ∧ 𝑏𝑆𝑓) ↔ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓)))
38	35, 37	orbi12d 918	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑎 = 𝑐 → ((𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)) ↔ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓))))
39	38	imbi2d 341	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎 = 𝑐 → (((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))) ↔ ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓)))))
40	34, 39	imbitrrid 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑎 = 𝑐 → (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
41	40	expd 417	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = 𝑐 → ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))))
42	41	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑎 = 𝑐 → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))))
43	42	impd 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → ((𝑎 = 𝑐 ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
44	30, 43	jaao 954	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
45	44	impd 412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
46	45	an4s 659	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
47	17, 46	sylan2b 595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
48		an4 655	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
49	48	biimpi 215	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
50	49	3adant2 1132	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
51	50	adantl 483	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
52	47, 51	jctild 527	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
53	52	adantld 492	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ ((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
54	16, 53	biimtrid 241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
55	15, 54	jca 513	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))))
56		breq12 5149	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
57	56	anidms 568	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
58	57	notbid 318	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
59	58	3ad2ant1 1134	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
60		breq12 5149	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩))
61	60	3adant3 1133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩))
62		breq12 5149	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩))
63	62	3adant1 1131	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩))
64	61, 63	anbi12d 632	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) ↔ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩)))
65		breq12 5149	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩))
66	65	3adant2 1132	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩))
67	64, 66	imbi12d 345	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣) ↔ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩)))
68	59, 67	anbi12d 632	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩))))
69		poxp.1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥)𝑆(2^nd ‘𝑦))))}
70	69	xporderlem 8100	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
71	70	notbii 320	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ↔ ¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
72	69	xporderlem 8100	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))))
73	69	xporderlem 8100	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩ ↔ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))))
74	72, 73	anbi12i 628	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))))
75	69	xporderlem 8100	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
76	74, 75	imbi12i 351	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩) ↔ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
77	71, 76	anbi12i 628	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩)) ↔ (¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))))
78	68, 77	bitrdi 287	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))))
79	55, 78	imbitrrid 245	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
80	79	expcomd 418	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
81	80	imp 408	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
82	4, 81	sylbi 216	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
83	82	3exp 1120	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
84	83	com3l 89	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
85	84	exlimivv 1936	. . . . . . . . . . . . 13 ⊢ (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
86	85	com3l 89	. . . . . . . . . . . 12 ⊢ ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
87	86	exlimivv 1936	. . . . . . . . . . 11 ⊢ (∃𝑒∃𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
88	87	com3l 89	. . . . . . . . . 10 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (∃𝑒∃𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
89	88	exlimivv 1936	. . . . . . . . 9 ⊢ (∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (∃𝑒∃𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
90	89	3imp 1112	. . . . . . . 8 ⊢ ((∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) ∧ ∃𝑒∃𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
91	1, 2, 3, 90	syl3anb 1162	. . . . . . 7 ⊢ ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ (𝐴 × 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
92	91	3expia 1122	. . . . . 6 ⊢ ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
93	92	com3r 87	. . . . 5 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
94	93	imp 408	. . . 4 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
95	94	ralrimiv 3146	. . 3 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → ∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
96	95	ralrimivva 3201	. 2 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
97		df-po 5584	. 2 ⊢ (𝑇 Po (𝐴 × 𝐵) ↔ ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
98	96, 97	sylibr 233	1 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 397 ∨ wo 846 ∧ w3a 1088 = wceq 1542 ∃wex 1782 ∈ wcel 2107 ∀wral 3062 ⟨cop 4630 class class class wbr 5144 {copab 5206 Po wpo 5582 × cxp 5670 ‘cfv 6535 1^st c1st 7960 2^nd c2nd 7961

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5295 ax-nul 5302 ax-pr 5423 ax-un 7712

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4321 df-if 4525 df-sn 4625 df-pr 4627 df-op 4631 df-uni 4905 df-br 5145 df-opab 5207 df-mpt 5228 df-id 5570 df-po 5584 df-xp 5678 df-rel 5679 df-cnv 5680 df-co 5681 df-dm 5682 df-rn 5683 df-iota 6487 df-fun 6537 df-fv 6543 df-1st 7962 df-2nd 7963

This theorem is referenced by: soxp 8102

W3C validator