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 7940

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 5603	. . . . . . . 8 ⊢ (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)))
2		elxp 5603	. . . . . . . 8 ⊢ (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)))
3		elxp 5603	. . . . . . . 8 ⊢ (𝑣 ∈ (𝐴 × 𝐵) ↔ ∃𝑒∃𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)))
4		3an6 1444	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) ↔ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))))
5		poirr 5506	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑅 Po 𝐴 ∧ 𝑎 ∈ 𝐴) → ¬ 𝑎𝑅𝑎)
6	5	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑅 Po 𝐴 → (𝑎 ∈ 𝐴 → ¬ 𝑎𝑅𝑎))
7		poirr 5506	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆 Po 𝐵 ∧ 𝑏 ∈ 𝐵) → ¬ 𝑏𝑆𝑏)
8	7	intnand 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆 Po 𝐵 ∧ 𝑏 ∈ 𝐵) → ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))
9	8	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑆 Po 𝐵 → (𝑏 ∈ 𝐵 → ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))
10	6, 9	im2anan9 619	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
11		ioran 980	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)) ↔ (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))
12	10, 11	syl6ibr 251	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
13	12	imp 406	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))
14	13	intnand 488	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
15	14	3ad2antr1 1186	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
16		an4 652	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ ((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))))
17		3an6 1444	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
18		potr 5507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) → ((𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒) → 𝑎𝑅𝑒))
19	18	3impia 1115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒)) → 𝑎𝑅𝑒)
20	19	orcd 869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))
21	20	3expia 1119	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) → ((𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
22	21	expdimp 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ 𝑎𝑅𝑐) → (𝑐𝑅𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
23		breq2 5074	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = 𝑒 → (𝑎𝑅𝑐 ↔ 𝑎𝑅𝑒))
24	23	biimpa 476	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑐 = 𝑒 ∧ 𝑎𝑅𝑐) → 𝑎𝑅𝑒)
25	24	orcd 869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑐 = 𝑒 ∧ 𝑎𝑅𝑐) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))
26	25	expcom 413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎𝑅𝑐 → (𝑐 = 𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
27	26	adantrd 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑎𝑅𝑐 → ((𝑐 = 𝑒 ∧ 𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
28	27	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐 = 𝑒 ∧ 𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
29	22, 28	jaod 855	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
30	29	ex 412	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) → (𝑎𝑅𝑐 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
31		potr 5507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → ((𝑏𝑆𝑑 ∧ 𝑑𝑆𝑓) → 𝑏𝑆𝑓))
32	31	expdimp 452	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → (𝑑𝑆𝑓 → 𝑏𝑆𝑓))
33	32	anim2d 611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐 = 𝑒 ∧ 𝑑𝑆𝑓) → (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓)))
34	33	orim2d 963	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓))))
35		breq1 5073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑐 → (𝑎𝑅𝑒 ↔ 𝑐𝑅𝑒))
36		equequ1 2029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑎 = 𝑐 → (𝑎 = 𝑒 ↔ 𝑐 = 𝑒))
37	36	anbi1d 629	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑐 → ((𝑎 = 𝑒 ∧ 𝑏𝑆𝑓) ↔ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓)))
38	35, 37	orbi12d 915	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑎 = 𝑐 → ((𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)) ↔ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓))))
39	38	imbi2d 340	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎 = 𝑐 → (((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))) ↔ ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓)))))
40	34, 39	syl5ibr 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑎 = 𝑐 → (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
41	40	expd 415	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = 𝑐 → ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))))
42	41	com12 32	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑎 = 𝑐 → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))))
43	42	impd 410	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → ((𝑎 = 𝑐 ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
44	30, 43	jaao 951	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
45	44	impd 410	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
46	45	an4s 656	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
47	17, 46	sylan2b 593	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
48		an4 652	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
49	48	biimpi 215	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
50	49	3adant2 1129	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
51	50	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
52	47, 51	jctild 525	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
53	52	adantld 490	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ ((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
54	16, 53	syl5bi 241	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
55	15, 54	jca 511	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))))
56		breq12 5075	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
57	56	anidms 566	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
58	57	notbid 317	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
59	58	3ad2ant1 1131	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
60		breq12 5075	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩))
61	60	3adant3 1130	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩))
62		breq12 5075	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩))
63	62	3adant1 1128	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩))
64	61, 63	anbi12d 630	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) ↔ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩)))
65		breq12 5075	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩))
66	65	3adant2 1129	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩))
67	64, 66	imbi12d 344	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣) ↔ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩)))
68	59, 67	anbi12d 630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩))))
69		poxp.1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥)𝑆(2^nd ‘𝑦))))}
70	69	xporderlem 7939	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
71	70	notbii 319	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ↔ ¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
72	69	xporderlem 7939	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))))
73	69	xporderlem 7939	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩ ↔ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))))
74	72, 73	anbi12i 626	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))))
75	69	xporderlem 7939	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
76	74, 75	imbi12i 350	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩) ↔ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
77	71, 76	anbi12i 626	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩)) ↔ (¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))))
78	68, 77	bitrdi 286	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))))
79	55, 78	syl5ibr 245	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
80	79	expcomd 416	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
81	80	imp 406	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
82	4, 81	sylbi 216	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
83	82	3exp 1117	. . . . . . . . . . . . . . 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 1109	. . . . . . . 8 ⊢ ((∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) ∧ ∃𝑒∃𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
91	1, 2, 3, 90	syl3anb 1159	. . . . . . 7 ⊢ ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ (𝐴 × 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
92	91	3expia 1119	. . . . . 6 ⊢ ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
93	92	com3r 87	. . . . 5 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
94	93	imp 406	. . . 4 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
95	94	ralrimiv 3106	. . 3 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → ∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
96	95	ralrimivva 3114	. 2 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
97		df-po 5494	. 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 395 ∨ wo 843 ∧ w3a 1085 = wceq 1539 ∃wex 1783 ∈ wcel 2108 ∀wral 3063 ⟨cop 4564 class class class wbr 5070 {copab 5132 Po wpo 5492 × cxp 5578 ‘cfv 6418 1^st c1st 7802 2^nd c2nd 7803

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-sep 5218 ax-nul 5225 ax-pr 5347 ax-un 7566

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-ral 3068 df-rex 3069 df-rab 3072 df-v 3424 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-nul 4254 df-if 4457 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4837 df-br 5071 df-opab 5133 df-mpt 5154 df-id 5480 df-po 5494 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-iota 6376 df-fun 6420 df-fv 6426 df-1st 7804 df-2nd 7805

This theorem is referenced by: soxp 7941

W3C validator