poxp - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > poxp		GIF version

Theorem poxp 6059

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 4494	. . . . . . . 8 ⊢ (𝑡 ∈ (𝐴 × 𝐵) ↔ ∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)))
2		elxp 4494	. . . . . . . 8 ⊢ (𝑢 ∈ (𝐴 × 𝐵) ↔ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)))
3		elxp 4494	. . . . . . . 8 ⊢ (𝑣 ∈ (𝐴 × 𝐵) ↔ ∃𝑒∃𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)))
4		3an6 1268	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) ↔ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))))
5		poirr 4167	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑅 Po 𝐴 ∧ 𝑎 ∈ 𝐴) → ¬ 𝑎𝑅𝑎)
6	5	ex 114	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑅 Po 𝐴 → (𝑎 ∈ 𝐴 → ¬ 𝑎𝑅𝑎))
7		poirr 4167	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆 Po 𝐵 ∧ 𝑏 ∈ 𝐵) → ¬ 𝑏𝑆𝑏)
8	7	intnand 884	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆 Po 𝐵 ∧ 𝑏 ∈ 𝐵) → ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))
9	8	ex 114	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑆 Po 𝐵 → (𝑏 ∈ 𝐵 → ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))
10	6, 9	im2anan9 568	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
11		ioran 710	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)) ↔ (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))
12	10, 11	syl6ibr 161	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
13	12	imp 123	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))
14	13	intnand 884	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
15	14	3ad2antr1 1114	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
16		an4 556	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ ((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))))
17		3an6 1268	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
18		potr 4168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) → ((𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒) → 𝑎𝑅𝑒))
19	18	3impia 1146	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒)) → 𝑎𝑅𝑒)
20	19	orcd 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))
21	20	3expia 1151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) → ((𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
22	21	expdimp 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ 𝑎𝑅𝑐) → (𝑐𝑅𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
23		breq2 3879	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = 𝑒 → (𝑎𝑅𝑐 ↔ 𝑎𝑅𝑒))
24	23	biimpa 292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑐 = 𝑒 ∧ 𝑎𝑅𝑐) → 𝑎𝑅𝑒)
25	24	orcd 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑐 = 𝑒 ∧ 𝑎𝑅𝑐) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))
26	25	expcom 115	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎𝑅𝑐 → (𝑐 = 𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
27	26	adantrd 275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑎𝑅𝑐 → ((𝑐 = 𝑒 ∧ 𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
28	27	adantl 273	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐 = 𝑒 ∧ 𝑑𝑆𝑓) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
29	22, 28	jaod 678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ 𝑎𝑅𝑐) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
30	29	ex 114	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) → (𝑎𝑅𝑐 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
31		potr 4168	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → ((𝑏𝑆𝑑 ∧ 𝑑𝑆𝑓) → 𝑏𝑆𝑓))
32	31	expdimp 257	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → (𝑑𝑆𝑓 → 𝑏𝑆𝑓))
33	32	anim2d 333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐 = 𝑒 ∧ 𝑑𝑆𝑓) → (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓)))
34	33	orim2d 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓))))
35		breq1 3878	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑐 → (𝑎𝑅𝑒 ↔ 𝑐𝑅𝑒))
36		equequ1 1656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑎 = 𝑐 → (𝑎 = 𝑒 ↔ 𝑐 = 𝑒))
37	36	anbi1d 456	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑐 → ((𝑎 = 𝑒 ∧ 𝑏𝑆𝑓) ↔ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓)))
38	35, 37	orbi12d 748	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑎 = 𝑐 → ((𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)) ↔ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓))))
39	38	imbi2d 229	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎 = 𝑐 → (((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))) ↔ ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆𝑓)))))
40	34, 39	syl5ibr 155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑎 = 𝑐 → (((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
41	40	expd 256	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = 𝑐 → ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))))
42	41	com12 30	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → (𝑎 = 𝑐 → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))))
43	42	impd 252	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) → ((𝑎 = 𝑐 ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
44	30, 43	jaao 680	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
45	44	impd 252	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 Po 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴)) ∧ (𝑆 Po 𝐵 ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
46	45	an4s 558	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
47	17, 46	sylan2b 283	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
48		an4 556	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) ↔ ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
49	48	biimpi 119	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
50	49	3adant2 968	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
51	50	adantl 273	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)))
52	47, 51	jctild 312	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
53	52	adantld 274	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ ((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
54	16, 53	syl5bi 151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
55	15, 54	jca 302	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))))
56		breq12 3880	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
57	56	anidms 392	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
58	57	notbid 633	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
59	58	3ad2ant1 970	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
60		breq12 3880	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩))
61	60	3adant3 969	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑢 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩))
62		breq12 3880	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩))
63	62	3adant1 967	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑢𝑇𝑣 ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩))
64	61, 63	anbi12d 460	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) ↔ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩)))
65		breq12 3880	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩))
66	65	3adant2 968	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (𝑡𝑇𝑣 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩))
67	64, 66	imbi12d 233	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣) ↔ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩)))
68	59, 67	anbi12d 460	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩))))
69		poxp.1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑇 = {⟨𝑥, 𝑦⟩ ∣ ((𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵)) ∧ ((1^st ‘𝑥)𝑅(1^st ‘𝑦) ∨ ((1^st ‘𝑥) = (1^st ‘𝑦) ∧ (2^nd ‘𝑥)𝑆(2^nd ‘𝑦))))}
70	69	xporderlem 6058	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
71	70	notbii 635	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ↔ ¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
72	69	xporderlem 6058	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))))
73	69	xporderlem 6058	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩ ↔ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓))))
74	72, 73	anbi12i 451	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) ↔ ((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))))
75	69	xporderlem 6058	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩ ↔ (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))
76	74, 75	imbi12i 238	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩) ↔ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))
77	71, 76	anbi12i 451	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, 𝑓⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, 𝑓⟩)) ↔ (¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓))))))
78	68, 77	syl6bb 195	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)) ↔ (¬ (((𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆𝑓)))) → (((𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴) ∧ (𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆𝑓)))))))
79	55, 78	syl5ibr 155	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
80	79	expcomd 1385	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) → (((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
81	80	imp 123	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑢 = ⟨𝑐, 𝑑⟩ ∧ 𝑣 = ⟨𝑒, 𝑓⟩) ∧ ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵) ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
82	4, 81	sylbi 120	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) ∧ (𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
83	82	3exp 1148	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
84	83	com3l 81	. . . . . . . . . . . . . 14 ⊢ ((𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
85	84	exlimivv 1835	. . . . . . . . . . . . 13 ⊢ (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
86	85	com3l 81	. . . . . . . . . . . 12 ⊢ ((𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
87	86	exlimivv 1835	. . . . . . . . . . 11 ⊢ (∃𝑒∃𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
88	87	com3l 81	. . . . . . . . . 10 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (∃𝑒∃𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
89	88	exlimivv 1835	. . . . . . . . 9 ⊢ (∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) → (∃𝑒∃𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))))
90	89	3imp 1143	. . . . . . . 8 ⊢ ((∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) ∧ ∃𝑐∃𝑑(𝑢 = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵)) ∧ ∃𝑒∃𝑓(𝑣 = ⟨𝑒, 𝑓⟩ ∧ (𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵))) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
91	1, 2, 3, 90	syl3anb 1227	. . . . . . 7 ⊢ ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵) ∧ 𝑣 ∈ (𝐴 × 𝐵)) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
92	91	3expia 1151	. . . . . 6 ⊢ ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
93	92	com3r 79	. . . . 5 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ((𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵)) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))))
94	93	imp 123	. . . 4 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → (𝑣 ∈ (𝐴 × 𝐵) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣))))
95	94	ralrimiv 2463	. . 3 ⊢ (((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) ∧ (𝑡 ∈ (𝐴 × 𝐵) ∧ 𝑢 ∈ (𝐴 × 𝐵))) → ∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
96	95	ralrimivva 2473	. 2 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
97		df-po 4156	. 2 ⊢ (𝑇 Po (𝐴 × 𝐵) ↔ ∀𝑡 ∈ (𝐴 × 𝐵)∀𝑢 ∈ (𝐴 × 𝐵)∀𝑣 ∈ (𝐴 × 𝐵)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇𝑢 ∧ 𝑢𝑇𝑣) → 𝑡𝑇𝑣)))
98	96, 97	sylibr 133	1 ⊢ ((𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵) → 𝑇 Po (𝐴 × 𝐵))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 670 ∧ w3a 930 = wceq 1299 ∃wex 1436 ∈ wcel 1448 ∀wral 2375 ⟨cop 3477 class class class wbr 3875 {copab 3928 Po wpo 4154 × cxp 4475 ‘cfv 5059 1^st c1st 5967 2^nd c2nd 5968

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 584 ax-in2 585 ax-io 671 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-10 1451 ax-11 1452 ax-i12 1453 ax-bndl 1454 ax-4 1455 ax-13 1459 ax-14 1460 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 ax-sep 3986 ax-pow 4038 ax-pr 4069 ax-un 4293

This theorem depends on definitions: df-bi 116 df-3an 932 df-tru 1302 df-nf 1405 df-sb 1704 df-eu 1963 df-mo 1964 df-clab 2087 df-cleq 2093 df-clel 2096 df-nfc 2229 df-ral 2380 df-rex 2381 df-v 2643 df-sbc 2863 df-un 3025 df-in 3027 df-ss 3034 df-pw 3459 df-sn 3480 df-pr 3481 df-op 3483 df-uni 3684 df-br 3876 df-opab 3930 df-mpt 3931 df-id 4153 df-po 4156 df-xp 4483 df-rel 4484 df-cnv 4485 df-co 4486 df-dm 4487 df-rn 4488 df-iota 5024 df-fun 5061 df-fv 5067 df-1st 5969 df-2nd 5970

This theorem is referenced by: (None)

W3C validator