poxp

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

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

Proof

Step	Hyp	Ref	Expression
1		poxp.1	⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑦 ∈ ( 𝐴 × 𝐵 ) ) ∧ ( ( 1^st ‘ 𝑥 ) 𝑅 ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) 𝑆 ( 2^nd ‘ 𝑦 ) ) ) ) }
2		elxp	⊢ ( 𝑡 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) )
3		elxp	⊢ ( 𝑢 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑐 ∃ 𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) )
4		elxp	⊢ ( 𝑣 ∈ ( 𝐴 × 𝐵 ) ↔ ∃ 𝑒 ∃ 𝑓 ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) )
5		3an6	⊢ ( ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) ) ↔ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) ) )
6		poirr	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑎 ∈ 𝐴 ) → ¬ 𝑎 𝑅 𝑎 )
7	6	ex	⊢ ( 𝑅 Po 𝐴 → ( 𝑎 ∈ 𝐴 → ¬ 𝑎 𝑅 𝑎 ) )
8		poirr	⊢ ( ( 𝑆 Po 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ¬ 𝑏 𝑆 𝑏 )
9	8	intnand	⊢ ( ( 𝑆 Po 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ¬ ( 𝑎 = 𝑎 ∧ 𝑏 𝑆 𝑏 ) )
10	9	ex	⊢ ( 𝑆 Po 𝐵 → ( 𝑏 ∈ 𝐵 → ¬ ( 𝑎 = 𝑎 ∧ 𝑏 𝑆 𝑏 ) ) )
11	7 10	im2anan9	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ( ¬ 𝑎 𝑅 𝑎 ∧ ¬ ( 𝑎 = 𝑎 ∧ 𝑏 𝑆 𝑏 ) ) ) )
12		ioran	⊢ ( ¬ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎 ∧ 𝑏 𝑆 𝑏 ) ) ↔ ( ¬ 𝑎 𝑅 𝑎 ∧ ¬ ( 𝑎 = 𝑎 ∧ 𝑏 𝑆 𝑏 ) ) )
13	11 12	syl6ibr	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) → ¬ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎 ∧ 𝑏 𝑆 𝑏 ) ) ) )
14	13	imp	⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ¬ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎 ∧ 𝑏 𝑆 𝑏 ) ) )
15	14	intnand	⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ¬ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎 ∧ 𝑏 𝑆 𝑏 ) ) ) )
16	15	3ad2antr1	⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) ) → ¬ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎 ∧ 𝑏 𝑆 𝑏 ) ) ) )
17		an4	⊢ ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ∧ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) ) ) ↔ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( ( 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ) ∧ ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) ) ) )
18		3an6	⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) )
19		potr	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ) → ( ( 𝑎 𝑅 𝑐 ∧ 𝑐 𝑅 𝑒 ) → 𝑎 𝑅 𝑒 ) )
20	19	3impia	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑎 𝑅 𝑐 ∧ 𝑐 𝑅 𝑒 ) ) → 𝑎 𝑅 𝑒 )
21	20	orcd	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑎 𝑅 𝑐 ∧ 𝑐 𝑅 𝑒 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) )
22	21	3expia	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ) → ( ( 𝑎 𝑅 𝑐 ∧ 𝑐 𝑅 𝑒 ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) )
23	22	expdimp	⊢ ( ( ( 𝑅 Po 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ) ∧ 𝑎 𝑅 𝑐 ) → ( 𝑐 𝑅 𝑒 → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) )
24		breq2	⊢ ( 𝑐 = 𝑒 → ( 𝑎 𝑅 𝑐 ↔ 𝑎 𝑅 𝑒 ) )
25	24	biimpa	⊢ ( ( 𝑐 = 𝑒 ∧ 𝑎 𝑅 𝑐 ) → 𝑎 𝑅 𝑒 )
26	25	orcd	⊢ ( ( 𝑐 = 𝑒 ∧ 𝑎 𝑅 𝑐 ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) )
27	26	expcom	⊢ ( 𝑎 𝑅 𝑐 → ( 𝑐 = 𝑒 → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) )
28	27	adantrd	⊢ ( 𝑎 𝑅 𝑐 → ( ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) )
29	28	adantl	⊢ ( ( ( 𝑅 Po 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ) ∧ 𝑎 𝑅 𝑐 ) → ( ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) )
30	23 29	jaod	⊢ ( ( ( 𝑅 Po 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ) ∧ 𝑎 𝑅 𝑐 ) → ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) )
31	30	ex	⊢ ( ( 𝑅 Po 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ) → ( 𝑎 𝑅 𝑐 → ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) ) )
32		potr	⊢ ( ( 𝑆 Po 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) → ( ( 𝑏 𝑆 𝑑 ∧ 𝑑 𝑆 𝑓 ) → 𝑏 𝑆 𝑓 ) )
33	32	expdimp	⊢ ( ( ( 𝑆 Po 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ 𝑏 𝑆 𝑑 ) → ( 𝑑 𝑆 𝑓 → 𝑏 𝑆 𝑓 ) )
34	33	anim2d	⊢ ( ( ( 𝑆 Po 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ 𝑏 𝑆 𝑑 ) → ( ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) → ( 𝑐 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) )
35	34	orim2d	⊢ ( ( ( 𝑆 Po 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ 𝑏 𝑆 𝑑 ) → ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) → ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) )
36		breq1	⊢ ( 𝑎 = 𝑐 → ( 𝑎 𝑅 𝑒 ↔ 𝑐 𝑅 𝑒 ) )
37		equequ1	⊢ ( 𝑎 = 𝑐 → ( 𝑎 = 𝑒 ↔ 𝑐 = 𝑒 ) )
38	37	anbi1d	⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ↔ ( 𝑐 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) )
39	36 38	orbi12d	⊢ ( 𝑎 = 𝑐 → ( ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ↔ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) )
40	39	imbi2d	⊢ ( 𝑎 = 𝑐 → ( ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) ↔ ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) → ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) ) )
41	35 40	syl5ibr	⊢ ( 𝑎 = 𝑐 → ( ( ( 𝑆 Po 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ 𝑏 𝑆 𝑑 ) → ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) ) )
42	41	expd	⊢ ( 𝑎 = 𝑐 → ( ( 𝑆 Po 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) → ( 𝑏 𝑆 𝑑 → ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) ) ) )
43	42	com12	⊢ ( ( 𝑆 Po 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) → ( 𝑎 = 𝑐 → ( 𝑏 𝑆 𝑑 → ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) ) ) )
44	43	impd	⊢ ( ( 𝑆 Po 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) → ( ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) → ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) ) )
45	31 44	jaao	⊢ ( ( ( 𝑅 Po 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ) ∧ ( 𝑆 Po 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ) → ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) → ( ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) ) )
46	45	impd	⊢ ( ( ( 𝑅 Po 𝐴 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ) ∧ ( 𝑆 Po 𝐵 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ) → ( ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) )
47	46	an4s	⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ) → ( ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) )
48	18 47	sylan2b	⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) ) → ( ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) ) → ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) )
49		an4	⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) )
50	49	biimpi	⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) )
51	50	3adant2	⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) )
52	51	adantl	⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) ) → ( ( 𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) )
53	48 52	jctild	⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) ) → ( ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) ) )
54	53	adantld	⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) ) → ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( ( 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ) ∧ ( ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) ) ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) ) )
55	17 54	syl5bi	⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) ) → ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ∧ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) ) ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) ) )
56	16 55	jca	⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) ) → ( ¬ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎 ∧ 𝑏 𝑆 𝑏 ) ) ) ∧ ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ∧ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) ) ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) ) ) )
57		breq12	⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ) → ( 𝑡 𝑇 𝑡 ↔ ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) )
58	57	anidms	⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑡 𝑇 𝑡 ↔ ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) )
59	58	notbid	⊢ ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ → ( ¬ 𝑡 𝑇 𝑡 ↔ ¬ ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) )
60	59	3ad2ant1	⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( ¬ 𝑡 𝑇 𝑡 ↔ ¬ ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ) )
61		breq12	⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ) → ( 𝑡 𝑇 𝑢 ↔ ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ) )
62	61	3adant3	⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( 𝑡 𝑇 𝑢 ↔ ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ) )
63		breq12	⊢ ( ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( 𝑢 𝑇 𝑣 ↔ ⟨ 𝑐 , 𝑑 ⟩ 𝑇 ⟨ 𝑒 , 𝑓 ⟩ ) )
64	63	3adant1	⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( 𝑢 𝑇 𝑣 ↔ ⟨ 𝑐 , 𝑑 ⟩ 𝑇 ⟨ 𝑒 , 𝑓 ⟩ ) )
65	62 64	anbi12d	⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ 𝑇 ⟨ 𝑒 , 𝑓 ⟩ ) ) )
66		breq12	⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( 𝑡 𝑇 𝑣 ↔ ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑒 , 𝑓 ⟩ ) )
67	66	3adant2	⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( 𝑡 𝑇 𝑣 ↔ ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑒 , 𝑓 ⟩ ) )
68	65 67	imbi12d	⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ↔ ( ( ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ 𝑇 ⟨ 𝑒 , 𝑓 ⟩ ) → ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑒 , 𝑓 ⟩ ) ) )
69	60 68	anbi12d	⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ↔ ( ¬ ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ 𝑇 ⟨ 𝑒 , 𝑓 ⟩ ) → ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑒 , 𝑓 ⟩ ) ) ) )
70	1	xporderlem	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ↔ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎 ∧ 𝑏 𝑆 𝑏 ) ) ) )
71	70	notbii	⊢ ( ¬ ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ↔ ¬ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎 ∧ 𝑏 𝑆 𝑏 ) ) ) )
72	1	xporderlem	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ↔ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) )
73	1	xporderlem	⊢ ( ⟨ 𝑐 , 𝑑 ⟩ 𝑇 ⟨ 𝑒 , 𝑓 ⟩ ↔ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) ) )
74	72 73	anbi12i	⊢ ( ( ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ 𝑇 ⟨ 𝑒 , 𝑓 ⟩ ) ↔ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ∧ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) ) ) )
75	1	xporderlem	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑒 , 𝑓 ⟩ ↔ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) )
76	74 75	imbi12i	⊢ ( ( ( ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ 𝑇 ⟨ 𝑒 , 𝑓 ⟩ ) → ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑒 , 𝑓 ⟩ ) ↔ ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ∧ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) ) ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) ) )
77	71 76	anbi12i	⊢ ( ( ¬ ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑎 , 𝑏 ⟩ ∧ ( ( ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑐 , 𝑑 ⟩ ∧ ⟨ 𝑐 , 𝑑 ⟩ 𝑇 ⟨ 𝑒 , 𝑓 ⟩ ) → ⟨ 𝑎 , 𝑏 ⟩ 𝑇 ⟨ 𝑒 , 𝑓 ⟩ ) ) ↔ ( ¬ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎 ∧ 𝑏 𝑆 𝑏 ) ) ) ∧ ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ∧ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) ) ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) ) ) )
78	69 77	bitrdi	⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ↔ ( ¬ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑎 ∨ ( 𝑎 = 𝑎 ∧ 𝑏 𝑆 𝑏 ) ) ) ∧ ( ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑐 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑐 ∨ ( 𝑎 = 𝑐 ∧ 𝑏 𝑆 𝑑 ) ) ) ∧ ( ( ( 𝑐 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑑 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ ( 𝑐 𝑅 𝑒 ∨ ( 𝑐 = 𝑒 ∧ 𝑑 𝑆 𝑓 ) ) ) ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑒 ∈ 𝐴 ) ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑓 ∈ 𝐵 ) ) ∧ ( 𝑎 𝑅 𝑒 ∨ ( 𝑎 = 𝑒 ∧ 𝑏 𝑆 𝑓 ) ) ) ) ) ) )
79	56 78	syl5ibr	⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) )
80	79	expcomd	⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) → ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) → ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) )
81	80	imp	⊢ ( ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ) ∧ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) ) → ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) )
82	5 81	sylbi	⊢ ( ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) ) → ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) )
83	82	3exp	⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) → ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) ) )
84	83	com3l	⊢ ( ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) → ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) ) )
85	84	exlimivv	⊢ ( ∃ 𝑐 ∃ 𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) → ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) ) )
86	85	com3l	⊢ ( ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) → ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ∃ 𝑐 ∃ 𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) ) )
87	86	exlimivv	⊢ ( ∃ 𝑒 ∃ 𝑓 ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) → ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ∃ 𝑐 ∃ 𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) ) )
88	87	com3l	⊢ ( ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ∃ 𝑐 ∃ 𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ∃ 𝑒 ∃ 𝑓 ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) → ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) ) )
89	88	exlimivv	⊢ ( ∃ 𝑎 ∃ 𝑏 ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) → ( ∃ 𝑐 ∃ 𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) → ( ∃ 𝑒 ∃ 𝑓 ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) → ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) ) )
90	89	3imp	⊢ ( ( ∃ 𝑎 ∃ 𝑏 ( 𝑡 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ∧ ∃ 𝑐 ∃ 𝑑 ( 𝑢 = ⟨ 𝑐 , 𝑑 ⟩ ∧ ( 𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐵 ) ) ∧ ∃ 𝑒 ∃ 𝑓 ( 𝑣 = ⟨ 𝑒 , 𝑓 ⟩ ∧ ( 𝑒 ∈ 𝐴 ∧ 𝑓 ∈ 𝐵 ) ) ) → ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) )
91	2 3 4 90	syl3anb	⊢ ( ( 𝑡 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑢 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑣 ∈ ( 𝐴 × 𝐵 ) ) → ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) )
92	91	3expia	⊢ ( ( 𝑡 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑢 ∈ ( 𝐴 × 𝐵 ) ) → ( 𝑣 ∈ ( 𝐴 × 𝐵 ) → ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) )
93	92	com3r	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → ( ( 𝑡 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑢 ∈ ( 𝐴 × 𝐵 ) ) → ( 𝑣 ∈ ( 𝐴 × 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) ) )
94	93	imp	⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝑡 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑢 ∈ ( 𝐴 × 𝐵 ) ) ) → ( 𝑣 ∈ ( 𝐴 × 𝐵 ) → ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) ) )
95	94	ralrimiv	⊢ ( ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) ∧ ( 𝑡 ∈ ( 𝐴 × 𝐵 ) ∧ 𝑢 ∈ ( 𝐴 × 𝐵 ) ) ) → ∀ 𝑣 ∈ ( 𝐴 × 𝐵 ) ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) )
96	95	ralrimivva	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → ∀ 𝑡 ∈ ( 𝐴 × 𝐵 ) ∀ 𝑢 ∈ ( 𝐴 × 𝐵 ) ∀ 𝑣 ∈ ( 𝐴 × 𝐵 ) ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) )
97		df-po	⊢ ( 𝑇 Po ( 𝐴 × 𝐵 ) ↔ ∀ 𝑡 ∈ ( 𝐴 × 𝐵 ) ∀ 𝑢 ∈ ( 𝐴 × 𝐵 ) ∀ 𝑣 ∈ ( 𝐴 × 𝐵 ) ( ¬ 𝑡 𝑇 𝑡 ∧ ( ( 𝑡 𝑇 𝑢 ∧ 𝑢 𝑇 𝑣 ) → 𝑡 𝑇 𝑣 ) ) )
98	96 97	sylibr	⊢ ( ( 𝑅 Po 𝐴 ∧ 𝑆 Po 𝐵 ) → 𝑇 Po ( 𝐴 × 𝐵 ) )

Metamath Proof Explorer

Theorem poxp

Proof