poxp - Intuitionistic Logic Explorer

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

Theorem poxp 5794

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	⊢ 𝑇 = {⟨x, y⟩ ∣ ((x ∈ (A × B) ∧ y ∈ (A × B)) ∧ ((1^st ‘x)𝑅(1^st ‘y) ∨ ((1^st ‘x) = (1^st ‘y) ∧ (2^nd ‘x)𝑆(2^nd ‘y))))}

**Assertion**
Ref	Expression
poxp	⊢ ((𝑅 Po A ∧ 𝑆 Po B) → 𝑇 Po (A × B))

Distinct variable groups: x,A,y x,B,y x,𝑅,y x,𝑆,y Allowed substitution hints: 𝑇(x,y)

Proof of Theorem poxp Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 f 𝑡 u v are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		elxp 4305	. . . . . . . 8 ⊢ (𝑡 ∈ (A × B) ↔ ∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ A ∧ 𝑏 ∈ B)))
2		elxp 4305	. . . . . . . 8 ⊢ (u ∈ (A × B) ↔ ∃𝑐∃𝑑(u = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B)))
3		elxp 4305	. . . . . . . 8 ⊢ (v ∈ (A × B) ↔ ∃𝑒∃f(v = ⟨𝑒, f⟩ ∧ (𝑒 ∈ A ∧ f ∈ B)))
4		3an6 1216	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ A ∧ 𝑏 ∈ B)) ∧ (u = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B)) ∧ (v = ⟨𝑒, f⟩ ∧ (𝑒 ∈ A ∧ f ∈ B))) ↔ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ u = ⟨𝑐, 𝑑⟩ ∧ v = ⟨𝑒, f⟩) ∧ ((𝑎 ∈ A ∧ 𝑏 ∈ B) ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))))
5		poirr 4035	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑅 Po A ∧ 𝑎 ∈ A) → ¬ 𝑎𝑅𝑎)
6	5	ex 108	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑅 Po A → (𝑎 ∈ A → ¬ 𝑎𝑅𝑎))
7		poirr 4035	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆 Po B ∧ 𝑏 ∈ B) → ¬ 𝑏𝑆𝑏)
8	7	intnand 839	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝑆 Po B ∧ 𝑏 ∈ B) → ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))
9	8	ex 108	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑆 Po B → (𝑏 ∈ B → ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))
10	6, 9	im2anan9 530	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑅 Po A ∧ 𝑆 Po B) → ((𝑎 ∈ A ∧ 𝑏 ∈ B) → (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
11		ioran 668	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)) ↔ (¬ 𝑎𝑅𝑎 ∧ ¬ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))
12	10, 11	syl6ibr 151	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑅 Po A ∧ 𝑆 Po B) → ((𝑎 ∈ A ∧ 𝑏 ∈ B) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
13	12	imp 115	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ (𝑎 ∈ A ∧ 𝑏 ∈ B)) → ¬ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏)))
14	13	intnand 839	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ (𝑎 ∈ A ∧ 𝑏 ∈ B)) → ¬ (((𝑎 ∈ A ∧ 𝑎 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑏 ∈ B)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
15	14	3ad2antr1 1068	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ ((𝑎 ∈ A ∧ 𝑏 ∈ B) ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))) → ¬ (((𝑎 ∈ A ∧ 𝑎 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑏 ∈ B)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
16		an4 520	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑎 ∈ A ∧ 𝑐 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑑 ∈ B ∧ f ∈ B)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)))) ↔ ((((𝑎 ∈ A ∧ 𝑐 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B)) ∧ ((𝑐 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑑 ∈ B ∧ f ∈ B))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)))))
17		3an6 1216	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 ∈ A ∧ 𝑏 ∈ B) ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B)) ↔ ((𝑎 ∈ A ∧ 𝑐 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B)))
18		potr 4036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐 ∈ A ∧ 𝑒 ∈ A)) → ((𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒) → 𝑎𝑅𝑒))
19	18	3impia 1100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒)) → 𝑎𝑅𝑒)
20	19	orcd 651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))
21	20	3expia 1105	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐 ∈ A ∧ 𝑒 ∈ A)) → ((𝑎𝑅𝑐 ∧ 𝑐𝑅𝑒) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))
22	21	expdimp 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐 ∈ A ∧ 𝑒 ∈ A)) ∧ 𝑎𝑅𝑐) → (𝑐𝑅𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))
23		breq2 3759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑐 = 𝑒 → (𝑎𝑅𝑐 ↔ 𝑎𝑅𝑒))
24	23	biimpa 280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑐 = 𝑒 ∧ 𝑎𝑅𝑐) → 𝑎𝑅𝑒)
25	24	orcd 651	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑐 = 𝑒 ∧ 𝑎𝑅𝑐) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))
26	25	expcom 109	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎𝑅𝑐 → (𝑐 = 𝑒 → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))
27	26	adantrd 264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑎𝑅𝑐 → ((𝑐 = 𝑒 ∧ 𝑑𝑆f) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))
28	27	adantl 262	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐 ∈ A ∧ 𝑒 ∈ A)) ∧ 𝑎𝑅𝑐) → ((𝑐 = 𝑒 ∧ 𝑑𝑆f) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))
29	22, 28	jaod 636	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐 ∈ A ∧ 𝑒 ∈ A)) ∧ 𝑎𝑅𝑐) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))
30	29	ex 108	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐 ∈ A ∧ 𝑒 ∈ A)) → (𝑎𝑅𝑐 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))))
31		potr 4036	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ((𝑆 Po B ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B)) → ((𝑏𝑆𝑑 ∧ 𝑑𝑆f) → 𝑏𝑆f))
32	31	expdimp 246	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (((𝑆 Po B ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B)) ∧ 𝑏𝑆𝑑) → (𝑑𝑆f → 𝑏𝑆f))
33	32	anim2d 320	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((𝑆 Po B ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B)) ∧ 𝑏𝑆𝑑) → ((𝑐 = 𝑒 ∧ 𝑑𝑆f) → (𝑐 = 𝑒 ∧ 𝑏𝑆f)))
34	33	orim2d 701	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((𝑆 Po B ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆f))))
35		breq1 3758	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑐 → (𝑎𝑅𝑒 ↔ 𝑐𝑅𝑒))
36		equequ1 1595	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑎 = 𝑐 → (𝑎 = 𝑒 ↔ 𝑐 = 𝑒))
37	36	anbi1d 438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑎 = 𝑐 → ((𝑎 = 𝑒 ∧ 𝑏𝑆f) ↔ (𝑐 = 𝑒 ∧ 𝑏𝑆f)))
38	35, 37	orbi12d 706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑎 = 𝑐 → ((𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)) ↔ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆f))))
39	38	imbi2d 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑎 = 𝑐 → (((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))) ↔ ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)) → (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑏𝑆f)))))
40	34, 39	syl5ibr 145	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑎 = 𝑐 → (((𝑆 Po B ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B)) ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))))
41	40	expd 245	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑎 = 𝑐 → ((𝑆 Po B ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B)) → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))))
42	41	com12 27	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑆 Po B ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B)) → (𝑎 = 𝑐 → (𝑏𝑆𝑑 → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))))
43	42	impd 242	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑆 Po B ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B)) → ((𝑎 = 𝑐 ∧ 𝑏𝑆𝑑) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))))
44	30, 43	jaao 638	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐 ∈ A ∧ 𝑒 ∈ A)) ∧ (𝑆 Po B ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B))) → ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) → ((𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))))
45	44	impd 242	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑅 Po A ∧ (𝑎 ∈ A ∧ 𝑐 ∈ A ∧ 𝑒 ∈ A)) ∧ (𝑆 Po B ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))
46	45	an4s 522	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ ((𝑎 ∈ A ∧ 𝑐 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B ∧ f ∈ B))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))
47	17, 46	sylan2b 271	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ ((𝑎 ∈ A ∧ 𝑏 ∈ B) ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))) → (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))
48		an4 520	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑎 ∈ A ∧ 𝑏 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B)) ↔ ((𝑎 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑏 ∈ B ∧ f ∈ B)))
49	48	biimpi 113	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑎 ∈ A ∧ 𝑏 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B)) → ((𝑎 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑏 ∈ B ∧ f ∈ B)))
50	49	3adant2 922	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑎 ∈ A ∧ 𝑏 ∈ B) ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B)) → ((𝑎 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑏 ∈ B ∧ f ∈ B)))
51	50	adantl 262	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ ((𝑎 ∈ A ∧ 𝑏 ∈ B) ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))) → ((𝑎 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑏 ∈ B ∧ f ∈ B)))
52	47, 51	jctild 299	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ ((𝑎 ∈ A ∧ 𝑏 ∈ B) ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))) → (((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))) → (((𝑎 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑏 ∈ B ∧ f ∈ B)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))))
53	52	adantld 263	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ ((𝑎 ∈ A ∧ 𝑏 ∈ B) ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))) → (((((𝑎 ∈ A ∧ 𝑐 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B)) ∧ ((𝑐 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑑 ∈ B ∧ f ∈ B))) ∧ ((𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)))) → (((𝑎 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑏 ∈ B ∧ f ∈ B)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))))
54	16, 53	syl5bi 141	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ ((𝑎 ∈ A ∧ 𝑏 ∈ B) ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))) → (((((𝑎 ∈ A ∧ 𝑐 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑑 ∈ B ∧ f ∈ B)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)))) → (((𝑎 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑏 ∈ B ∧ f ∈ B)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))))
55	15, 54	jca 290	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ ((𝑎 ∈ A ∧ 𝑏 ∈ B) ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))) → (¬ (((𝑎 ∈ A ∧ 𝑎 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑏 ∈ B)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ A ∧ 𝑐 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑑 ∈ B ∧ f ∈ B)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)))) → (((𝑎 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑏 ∈ B ∧ f ∈ B)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))))
56		breq12 3760	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ 𝑡 = ⟨𝑎, 𝑏⟩) → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
57	56	anidms 377	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (𝑡𝑇𝑡 ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
58	57	notbid 591	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑡 = ⟨𝑎, 𝑏⟩ → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
59	58	3ad2ant1 924	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ u = ⟨𝑐, 𝑑⟩ ∧ v = ⟨𝑒, f⟩) → (¬ 𝑡𝑇𝑡 ↔ ¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩))
60		breq12 3760	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ u = ⟨𝑐, 𝑑⟩) → (𝑡𝑇u ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩))
61	60	3adant3 923	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ u = ⟨𝑐, 𝑑⟩ ∧ v = ⟨𝑒, f⟩) → (𝑡𝑇u ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩))
62		breq12 3760	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((u = ⟨𝑐, 𝑑⟩ ∧ v = ⟨𝑒, f⟩) → (u𝑇v ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, f⟩))
63	62	3adant1 921	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ u = ⟨𝑐, 𝑑⟩ ∧ v = ⟨𝑒, f⟩) → (u𝑇v ↔ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, f⟩))
64	61, 63	anbi12d 442	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ u = ⟨𝑐, 𝑑⟩ ∧ v = ⟨𝑒, f⟩) → ((𝑡𝑇u ∧ u𝑇v) ↔ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, f⟩)))
65		breq12 3760	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ v = ⟨𝑒, f⟩) → (𝑡𝑇v ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑒, f⟩))
66	65	3adant2 922	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ u = ⟨𝑐, 𝑑⟩ ∧ v = ⟨𝑒, f⟩) → (𝑡𝑇v ↔ ⟨𝑎, 𝑏⟩𝑇⟨𝑒, f⟩))
67	64, 66	imbi12d 223	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ u = ⟨𝑐, 𝑑⟩ ∧ v = ⟨𝑒, f⟩) → (((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v) ↔ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, f⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, f⟩)))
68	59, 67	anbi12d 442	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ u = ⟨𝑐, 𝑑⟩ ∧ v = ⟨𝑒, f⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)) ↔ (¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, f⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, f⟩))))
69		poxp.1	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑇 = {⟨x, y⟩ ∣ ((x ∈ (A × B) ∧ y ∈ (A × B)) ∧ ((1^st ‘x)𝑅(1^st ‘y) ∨ ((1^st ‘x) = (1^st ‘y) ∧ (2^nd ‘x)𝑆(2^nd ‘y))))}
70	69	xporderlem 5793	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ↔ (((𝑎 ∈ A ∧ 𝑎 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑏 ∈ B)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
71	70	notbii 593	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ↔ ¬ (((𝑎 ∈ A ∧ 𝑎 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑏 ∈ B)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))))
72	69	xporderlem 5793	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ↔ (((𝑎 ∈ A ∧ 𝑐 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))))
73	69	xporderlem 5793	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑐, 𝑑⟩𝑇⟨𝑒, f⟩ ↔ (((𝑐 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑑 ∈ B ∧ f ∈ B)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f))))
74	72, 73	anbi12i 433	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, f⟩) ↔ ((((𝑎 ∈ A ∧ 𝑐 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑑 ∈ B ∧ f ∈ B)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)))))
75	69	xporderlem 5793	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨𝑎, 𝑏⟩𝑇⟨𝑒, f⟩ ↔ (((𝑎 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑏 ∈ B ∧ f ∈ B)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))
76	74, 75	imbi12i 228	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, f⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, f⟩) ↔ (((((𝑎 ∈ A ∧ 𝑐 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑑 ∈ B ∧ f ∈ B)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)))) → (((𝑎 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑏 ∈ B ∧ f ∈ B)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))))
77	71, 76	anbi12i 433	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((¬ ⟨𝑎, 𝑏⟩𝑇⟨𝑎, 𝑏⟩ ∧ ((⟨𝑎, 𝑏⟩𝑇⟨𝑐, 𝑑⟩ ∧ ⟨𝑐, 𝑑⟩𝑇⟨𝑒, f⟩) → ⟨𝑎, 𝑏⟩𝑇⟨𝑒, f⟩)) ↔ (¬ (((𝑎 ∈ A ∧ 𝑎 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑏 ∈ B)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ A ∧ 𝑐 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑑 ∈ B ∧ f ∈ B)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)))) → (((𝑎 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑏 ∈ B ∧ f ∈ B)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f))))))
78	68, 77	syl6bb 185	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ u = ⟨𝑐, 𝑑⟩ ∧ v = ⟨𝑒, f⟩) → ((¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)) ↔ (¬ (((𝑎 ∈ A ∧ 𝑎 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑏 ∈ B)) ∧ (𝑎𝑅𝑎 ∨ (𝑎 = 𝑎 ∧ 𝑏𝑆𝑏))) ∧ (((((𝑎 ∈ A ∧ 𝑐 ∈ A) ∧ (𝑏 ∈ B ∧ 𝑑 ∈ B)) ∧ (𝑎𝑅𝑐 ∨ (𝑎 = 𝑐 ∧ 𝑏𝑆𝑑))) ∧ (((𝑐 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑑 ∈ B ∧ f ∈ B)) ∧ (𝑐𝑅𝑒 ∨ (𝑐 = 𝑒 ∧ 𝑑𝑆f)))) → (((𝑎 ∈ A ∧ 𝑒 ∈ A) ∧ (𝑏 ∈ B ∧ f ∈ B)) ∧ (𝑎𝑅𝑒 ∨ (𝑎 = 𝑒 ∧ 𝑏𝑆f)))))))
79	55, 78	syl5ibr 145	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ u = ⟨𝑐, 𝑑⟩ ∧ v = ⟨𝑒, f⟩) → (((𝑅 Po A ∧ 𝑆 Po B) ∧ ((𝑎 ∈ A ∧ 𝑏 ∈ B) ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))))
80	79	expcomd 1327	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ u = ⟨𝑐, 𝑑⟩ ∧ v = ⟨𝑒, f⟩) → (((𝑎 ∈ A ∧ 𝑏 ∈ B) ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B)) → ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))))
81	80	imp 115	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ u = ⟨𝑐, 𝑑⟩ ∧ v = ⟨𝑒, f⟩) ∧ ((𝑎 ∈ A ∧ 𝑏 ∈ B) ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B) ∧ (𝑒 ∈ A ∧ f ∈ B))) → ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))))
82	4, 81	sylbi 114	. . . . . . . . . . . . . . . 16 ⊢ (((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ A ∧ 𝑏 ∈ B)) ∧ (u = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B)) ∧ (v = ⟨𝑒, f⟩ ∧ (𝑒 ∈ A ∧ f ∈ B))) → ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))))
83	82	3exp 1102	. . . . . . . . . . . . . . 15 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ A ∧ 𝑏 ∈ B)) → ((u = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B)) → ((v = ⟨𝑒, f⟩ ∧ (𝑒 ∈ A ∧ f ∈ B)) → ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))))))
84	83	com3l 75	. . . . . . . . . . . . . 14 ⊢ ((u = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B)) → ((v = ⟨𝑒, f⟩ ∧ (𝑒 ∈ A ∧ f ∈ B)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ A ∧ 𝑏 ∈ B)) → ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))))))
85	84	exlimivv 1773	. . . . . . . . . . . . 13 ⊢ (∃𝑐∃𝑑(u = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B)) → ((v = ⟨𝑒, f⟩ ∧ (𝑒 ∈ A ∧ f ∈ B)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ A ∧ 𝑏 ∈ B)) → ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))))))
86	85	com3l 75	. . . . . . . . . . . 12 ⊢ ((v = ⟨𝑒, f⟩ ∧ (𝑒 ∈ A ∧ f ∈ B)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ A ∧ 𝑏 ∈ B)) → (∃𝑐∃𝑑(u = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B)) → ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))))))
87	86	exlimivv 1773	. . . . . . . . . . 11 ⊢ (∃𝑒∃f(v = ⟨𝑒, f⟩ ∧ (𝑒 ∈ A ∧ f ∈ B)) → ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ A ∧ 𝑏 ∈ B)) → (∃𝑐∃𝑑(u = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B)) → ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))))))
88	87	com3l 75	. . . . . . . . . 10 ⊢ ((𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ A ∧ 𝑏 ∈ B)) → (∃𝑐∃𝑑(u = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B)) → (∃𝑒∃f(v = ⟨𝑒, f⟩ ∧ (𝑒 ∈ A ∧ f ∈ B)) → ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))))))
89	88	exlimivv 1773	. . . . . . . . 9 ⊢ (∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ A ∧ 𝑏 ∈ B)) → (∃𝑐∃𝑑(u = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B)) → (∃𝑒∃f(v = ⟨𝑒, f⟩ ∧ (𝑒 ∈ A ∧ f ∈ B)) → ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))))))
90	89	3imp 1097	. . . . . . . 8 ⊢ ((∃𝑎∃𝑏(𝑡 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 ∈ A ∧ 𝑏 ∈ B)) ∧ ∃𝑐∃𝑑(u = ⟨𝑐, 𝑑⟩ ∧ (𝑐 ∈ A ∧ 𝑑 ∈ B)) ∧ ∃𝑒∃f(v = ⟨𝑒, f⟩ ∧ (𝑒 ∈ A ∧ f ∈ B))) → ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))))
91	1, 2, 3, 90	syl3anb 1177	. . . . . . 7 ⊢ ((𝑡 ∈ (A × B) ∧ u ∈ (A × B) ∧ v ∈ (A × B)) → ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))))
92	91	3expia 1105	. . . . . 6 ⊢ ((𝑡 ∈ (A × B) ∧ u ∈ (A × B)) → (v ∈ (A × B) → ((𝑅 Po A ∧ 𝑆 Po B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))))
93	92	com3r 73	. . . . 5 ⊢ ((𝑅 Po A ∧ 𝑆 Po B) → ((𝑡 ∈ (A × B) ∧ u ∈ (A × B)) → (v ∈ (A × B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))))
94	93	imp 115	. . . 4 ⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ (𝑡 ∈ (A × B) ∧ u ∈ (A × B))) → (v ∈ (A × B) → (¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v))))
95	94	ralrimiv 2385	. . 3 ⊢ (((𝑅 Po A ∧ 𝑆 Po B) ∧ (𝑡 ∈ (A × B) ∧ u ∈ (A × B))) → ∀v ∈ (A × B)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))
96	95	ralrimivva 2395	. 2 ⊢ ((𝑅 Po A ∧ 𝑆 Po B) → ∀𝑡 ∈ (A × B)∀u ∈ (A × B)∀v ∈ (A × B)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))
97		df-po 4024	. 2 ⊢ (𝑇 Po (A × B) ↔ ∀𝑡 ∈ (A × B)∀u ∈ (A × B)∀v ∈ (A × B)(¬ 𝑡𝑇𝑡 ∧ ((𝑡𝑇u ∧ u𝑇v) → 𝑡𝑇v)))
98	96, 97	sylibr 137	1 ⊢ ((𝑅 Po A ∧ 𝑆 Po B) → 𝑇 Po (A × B))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 97 ↔ wb 98 ∨ wo 628 ∧ w3a 884 = wceq 1242 ∃wex 1378 ∈ wcel 1390 ∀wral 2300 ⟨cop 3370 class class class wbr 3755 {copab 3808 Po wpo 4022 × cxp 4286 ‘cfv 4845 1^st c1st 5707 2^nd c2nd 5708

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-in1 544 ax-in2 545 ax-io 629 ax-5 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-10 1393 ax-11 1394 ax-i12 1395 ax-bnd 1396 ax-4 1397 ax-13 1401 ax-14 1402 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 ax-sep 3866 ax-pow 3918 ax-pr 3935 ax-un 4136

This theorem depends on definitions: df-bi 110 df-3an 886 df-tru 1245 df-nf 1347 df-sb 1643 df-eu 1900 df-mo 1901 df-clab 2024 df-cleq 2030 df-clel 2033 df-nfc 2164 df-ral 2305 df-rex 2306 df-v 2553 df-sbc 2759 df-un 2916 df-in 2918 df-ss 2925 df-pw 3353 df-sn 3373 df-pr 3374 df-op 3376 df-uni 3572 df-br 3756 df-opab 3810 df-mpt 3811 df-id 4021 df-po 4024 df-xp 4294 df-rel 4295 df-cnv 4296 df-co 4297 df-dm 4298 df-rn 4299 df-iota 4810 df-fun 4847 df-fv 4853 df-1st 5709 df-2nd 5710

This theorem is referenced by: (None)

W3C validator