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 8129

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 5674	. . . . . . . 8 ⊢ (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)))
2		elxp 5674	. . . . . . . 8 ⊢ (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)))
3		elxp 5674	. . . . . . . 8 ⊢ (𝑣 ∈ (𝐴 × 𝐵) ↔ ∃𝑒∃𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)))
4		3an6 1475	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) ↔ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))))
5		poirr 5571	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑅 Po 𝐴 ∧ 𝑎 ∈ 𝐴) → ¬ 𝑎𝑅𝑎)
6	5	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑅 Po 𝐴 → (𝑎 ∈ 𝐴 → ¬ 𝑎𝑅𝑎))
7		poirr 5571	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆 Po 𝐵 ∧ 𝑏 ∈ 𝐵) → ¬ 𝑏𝑆𝑏)
8	7	intnand 494	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆 Po 𝐵 ∧ 𝑏 ∈ 𝐵) → ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))
9	8	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑆 Po 𝐵 → (𝑏 ∈ 𝐵 → ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))
10	6, 9	im2anan9 632	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
11		ioran 999	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)) ↔ (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))
12	10, 11	imbitrrdi 255	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
13	12	imp 412	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))
14	13	intnand 494	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
15	14	3ad2antr1 1207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
16		an4 669	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ ((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))))
17		3an6 1475	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
18		potr 5572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) → ((𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒) → 𝑎𝑅𝑒))
19	18	3impia 1135	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒)) → 𝑎𝑅𝑒)
20	19	orcd 887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))
21	20	3expia 1139	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) → ((𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
22	21	expdimp 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ 𝑎𝑅𝑐) → (𝑐𝑅𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
23		breq2 5107	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = 𝑒 → (𝑎𝑅𝑐 ↔ 𝑎𝑅𝑒))
24	23	biimpa 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑐 = 𝑒 ∧ 𝑎𝑅𝑐) → 𝑎𝑅𝑒)
25	24	orcd 887	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑐 = 𝑒 ∧ 𝑎𝑅𝑐) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))
26	25	expcom 419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎𝑅𝑐 → (𝑐 = 𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
27	26	adantrd 497	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑎𝑅𝑐 → ((𝑐 = 𝑒 ∧ 𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
28	27	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐 = 𝑒 ∧ 𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
29	22, 28	jaod 873	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
30	29	ex 418	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) → (𝑎𝑅𝑐 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
31		potr 5572	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → ((𝑏𝑆𝑑 ∧ 𝑑𝑆𝑓) → 𝑏𝑆𝑓))
32	31	expdimp 458	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → (𝑑𝑆𝑓 → 𝑏𝑆𝑓))
33	32	anim2d 624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐 = 𝑒 ∧ 𝑑𝑆𝑓) → (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓)))
34	33	orim2d 982	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓))))
35		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑐 → (𝑎𝑅𝑒 ↔ 𝑐𝑅𝑒))
36		equequ1 2058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑎 = 𝑐 → (𝑎 = 𝑒 ↔ 𝑐 = 𝑒))
37	36	anbi1d 643	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑐 → ((𝑎 = 𝑒 ∧ 𝑏𝑆𝑓) ↔ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓)))
38	35, 37	orbi12d 932	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑎 = 𝑐 → ((𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)) ↔ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓))))
39	38	imbi2d 343	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎 = 𝑐 → (((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))) ↔ ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓)))))
40	34, 39	imbitrrid 249	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑎 = 𝑐 → (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
41	40	expd 421	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = 𝑐 → ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))))
42	41	com12 33	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑎 = 𝑐 → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))))
43	42	impd 416	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → ((𝑎 = 𝑐 ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
44	30, 43	jaao 969	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
45	44	impd 416	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
46	45	an4s 673	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
47	17, 46	sylan2b 606	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
48		an4 669	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
49	48	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
50	49	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
51	50	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
52	47, 51	jctild 535	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
53	52	adantld 496	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ ((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
54	16, 53	biimtrid 245	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
55	15, 54	jca 521	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))))
56		breq12 5108	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
57	56	anidms 577	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
58	57	notbid 321	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
59	58	3ad2ant1 1151	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
60		breq12 5108	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩))
61	60	3adant3 1150	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩))
62		breq12 5108	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩))
63	62	3adant1 1148	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩))
64	61, 63	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) ↔ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩)))
65		breq12 5108	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩))
66	65	3adant2 1149	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩))
67	64, 66	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣) ↔ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩)))
68	59, 67	anbi12d 644	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩))))
69		poxp.1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥)𝑆(2^nd ‘𝑦))))}
70	69	xporderlem 8128	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
71	70	notbii 323	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ↔ ¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
72	69	xporderlem 8128	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))))
73	69	xporderlem 8128	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩ ↔ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))))
74	72, 73	anbi12i 640	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))))
75	69	xporderlem 8128	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
76	74, 75	imbi12i 353	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩) ↔ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
77	71, 76	anbi12i 640	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩)) ↔ (¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))))
78	68, 77	bitrdi 290	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))))
79	55, 78	imbitrrid 249	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
80	79	expcomd 422	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
81	80	imp 412	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
82	4, 81	sylbi 220	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
83	82	3exp 1137	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
84	83	com3l 90	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
85	84	exlimivv 1965	. . . . . . . . . . . . 13 ⊢ (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
86	85	com3l 90	. . . . . . . . . . . 12 ⊢ ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
87	86	exlimivv 1965	. . . . . . . . . . 11 ⊢ (∃𝑒∃𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
88	87	com3l 90	. . . . . . . . . 10 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (∃𝑒∃𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
89	88	exlimivv 1965	. . . . . . . . 9 ⊢ (∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (∃𝑒∃𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
90	89	3imp 1128	. . . . . . . 8 ⊢ ((∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) ∧ ∃𝑒∃𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
91	1, 2, 3, 90	syl3anb 1179	. . . . . . 7 ⊢ ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ (𝐴 × 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
92	91	3expia 1139	. . . . . 6 ⊢ ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
93	92	com3r 88	. . . . 5 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
94	93	imp 412	. . . 4 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
95	94	ralrimiv 3154	. . 3 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → ∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
96	95	ralrimivva 3206	. 2 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
97		df-po 5559	. 2 ⊢ (𝑇 Po (𝐴 × 𝐵) ↔ ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
98	96, 97	sylibr 237	1 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 ∧ w3a 1103 = wceq 1570 ∃wex 1812 ∈ wcel 2145 ∀wral 3077 ⟨cop 4590 class class class wbr 5103 {copab 5167 Po wpo 5557 × cxp 5649 ‘cfv 6531 1^st c1st 7988 2^nd c2nd 7989

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2733 ax-sep 5249 ax-nul 5260 ax-pr 5391 ax-un 7740

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-ral 3078 df-rex 3088 df-rab 3414 df-v 3453 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-sn 4585 df-pr 4587 df-op 4591 df-uni 4868 df-br 5104 df-opab 5168 df-mpt 5187 df-id 5546 df-po 5559 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-iota 6487 df-fun 6533 df-fv 6539 df-1st 7990 df-2nd 7991

This theorem is used by: soxp 8130

W3C validator