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	$⊢ T = \{⟨x, y⟩ \| ((x \in (A \times B) \land y \in (A \times B)) \land (1^{st} (x) R 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) S 2^{nd} (y))))\}$
	Assertion	poxp	$⊢ (R Po A \land S Po B) \to T Po (A \times B)$

Proof

Step	Hyp	Ref	Expression
1		poxp.1	$⊢ T = \{⟨x, y⟩ \| ((x \in (A \times B) \land y \in (A \times B)) \land (1^{st} (x) R 1^{st} (y) \lor (1^{st} (x) = 1^{st} (y) \land 2^{nd} (x) S 2^{nd} (y))))\}$
2		elxp	$⊢ t \in (A \times B) \leftrightarrow \exists a \exists b (t = ⟨a, b⟩ \land (a \in A \land b \in B))$
3		elxp	$⊢ u \in (A \times B) \leftrightarrow \exists c \exists d (u = ⟨c, d⟩ \land (c \in A \land d \in B))$
4		elxp	$⊢ v \in (A \times B) \leftrightarrow \exists e \exists f (v = ⟨e, f⟩ \land (e \in A \land f \in B))$
5		3an6	$⊢ ((t = ⟨a, b⟩ \land (a \in A \land b \in B)) \land (u = ⟨c, d⟩ \land (c \in A \land d \in B)) \land (v = ⟨e, f⟩ \land (e \in A \land f \in B))) \leftrightarrow ((t = ⟨a, b⟩ \land u = ⟨c, d⟩ \land v = ⟨e, f⟩) \land ((a \in A \land b \in B) \land (c \in A \land d \in B) \land (e \in A \land f \in B)))$
6		poirr	$⊢ (R Po A \land a \in A) \to \neg a R a$
7	6	ex	$⊢ R Po A \to (a \in A \to \neg a R a)$
8		poirr	$⊢ (S Po B \land b \in B) \to \neg b S b$
9	8	intnand	$⊢ (S Po B \land b \in B) \to \neg (a = a \land b S b)$
10	9	ex	$⊢ S Po B \to (b \in B \to \neg (a = a \land b S b))$
11	7 10	im2anan9	$⊢ (R Po A \land S Po B) \to ((a \in A \land b \in B) \to (\neg a R a \land \neg (a = a \land b S b)))$
12		ioran	$⊢ \neg (a R a \lor (a = a \land b S b)) \leftrightarrow (\neg a R a \land \neg (a = a \land b S b))$
13	11 12	syl6ibr	$⊢ (R Po A \land S Po B) \to ((a \in A \land b \in B) \to \neg (a R a \lor (a = a \land b S b)))$
14	13	imp	$⊢ ((R Po A \land S Po B) \land (a \in A \land b \in B)) \to \neg (a R a \lor (a = a \land b S b))$
15	14	intnand	$⊢ ((R Po A \land S Po B) \land (a \in A \land b \in B)) \to \neg (((a \in A \land a \in A) \land (b \in B \land b \in B)) \land (a R a \lor (a = a \land b S b)))$
16	15	3ad2antr1	$⊢ ((R Po A \land S Po B) \land ((a \in A \land b \in B) \land (c \in A \land d \in B) \land (e \in A \land f \in B))) \to \neg (((a \in A \land a \in A) \land (b \in B \land b \in B)) \land (a R a \lor (a = a \land b S b)))$
17		an4	$⊢ ((((a \in A \land c \in A) \land (b \in B \land d \in B)) \land (a R c \lor (a = c \land b S d))) \land (((c \in A \land e \in A) \land (d \in B \land f \in B)) \land (c R e \lor (c = e \land d S f)))) \leftrightarrow ((((a \in A \land c \in A) \land (b \in B \land d \in B)) \land ((c \in A \land e \in A) \land (d \in B \land f \in B))) \land ((a R c \lor (a = c \land b S d)) \land (c R e \lor (c = e \land d S f))))$
18		3an6	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B) \land (e \in A \land f \in B)) \leftrightarrow ((a \in A \land c \in A \land e \in A) \land (b \in B \land d \in B \land f \in B))$
19		potr	$⊢ (R Po A \land (a \in A \land c \in A \land e \in A)) \to ((a R c \land c R e) \to a R e)$
20	19	3impia	$⊢ (R Po A \land (a \in A \land c \in A \land e \in A) \land (a R c \land c R e)) \to a R e$
21	20	orcd	$⊢ (R Po A \land (a \in A \land c \in A \land e \in A) \land (a R c \land c R e)) \to (a R e \lor (a = e \land b S f))$
22	21	3expia	$⊢ (R Po A \land (a \in A \land c \in A \land e \in A)) \to ((a R c \land c R e) \to (a R e \lor (a = e \land b S f)))$
23	22	expdimp	$⊢ ((R Po A \land (a \in A \land c \in A \land e \in A)) \land a R c) \to (c R e \to (a R e \lor (a = e \land b S f)))$
24		breq2	$⊢ c = e \to (a R c \leftrightarrow a R e)$
25	24	biimpa	$⊢ (c = e \land a R c) \to a R e$
26	25	orcd	$⊢ (c = e \land a R c) \to (a R e \lor (a = e \land b S f))$
27	26	expcom	$⊢ a R c \to (c = e \to (a R e \lor (a = e \land b S f)))$
28	27	adantrd	$⊢ a R c \to ((c = e \land d S f) \to (a R e \lor (a = e \land b S f)))$
29	28	adantl	$⊢ ((R Po A \land (a \in A \land c \in A \land e \in A)) \land a R c) \to ((c = e \land d S f) \to (a R e \lor (a = e \land b S f)))$
30	23 29	jaod	$⊢ ((R Po A \land (a \in A \land c \in A \land e \in A)) \land a R c) \to ((c R e \lor (c = e \land d S f)) \to (a R e \lor (a = e \land b S f)))$
31	30	ex	$⊢ (R Po A \land (a \in A \land c \in A \land e \in A)) \to (a R c \to ((c R e \lor (c = e \land d S f)) \to (a R e \lor (a = e \land b S f))))$
32		potr	$⊢ (S Po B \land (b \in B \land d \in B \land f \in B)) \to ((b S d \land d S f) \to b S f)$
33	32	expdimp	$⊢ ((S Po B \land (b \in B \land d \in B \land f \in B)) \land b S d) \to (d S f \to b S f)$
34	33	anim2d	$⊢ ((S Po B \land (b \in B \land d \in B \land f \in B)) \land b S d) \to ((c = e \land d S f) \to (c = e \land b S f))$
35	34	orim2d	$⊢ ((S Po B \land (b \in B \land d \in B \land f \in B)) \land b S d) \to ((c R e \lor (c = e \land d S f)) \to (c R e \lor (c = e \land b S f)))$
36		breq1	$⊢ a = c \to (a R e \leftrightarrow c R e)$
37		equequ1	$⊢ a = c \to (a = e \leftrightarrow c = e)$
38	37	anbi1d	$⊢ a = c \to ((a = e \land b S f) \leftrightarrow (c = e \land b S f))$
39	36 38	orbi12d	$⊢ a = c \to ((a R e \lor (a = e \land b S f)) \leftrightarrow (c R e \lor (c = e \land b S f)))$
40	39	imbi2d	$⊢ a = c \to (((c R e \lor (c = e \land d S f)) \to (a R e \lor (a = e \land b S f))) \leftrightarrow ((c R e \lor (c = e \land d S f)) \to (c R e \lor (c = e \land b S f))))$
41	35 40	syl5ibr	$⊢ a = c \to (((S Po B \land (b \in B \land d \in B \land f \in B)) \land b S d) \to ((c R e \lor (c = e \land d S f)) \to (a R e \lor (a = e \land b S f))))$
42	41	expd	$⊢ a = c \to ((S Po B \land (b \in B \land d \in B \land f \in B)) \to (b S d \to ((c R e \lor (c = e \land d S f)) \to (a R e \lor (a = e \land b S f)))))$
43	42	com12	$⊢ (S Po B \land (b \in B \land d \in B \land f \in B)) \to (a = c \to (b S d \to ((c R e \lor (c = e \land d S f)) \to (a R e \lor (a = e \land b S f)))))$
44	43	impd	$⊢ (S Po B \land (b \in B \land d \in B \land f \in B)) \to ((a = c \land b S d) \to ((c R e \lor (c = e \land d S f)) \to (a R e \lor (a = e \land b S f))))$
45	31 44	jaao	$⊢ ((R Po A \land (a \in A \land c \in A \land e \in A)) \land (S Po B \land (b \in B \land d \in B \land f \in B))) \to ((a R c \lor (a = c \land b S d)) \to ((c R e \lor (c = e \land d S f)) \to (a R e \lor (a = e \land b S f))))$
46	45	impd	$⊢ ((R Po A \land (a \in A \land c \in A \land e \in A)) \land (S Po B \land (b \in B \land d \in B \land f \in B))) \to (((a R c \lor (a = c \land b S d)) \land (c R e \lor (c = e \land d S f))) \to (a R e \lor (a = e \land b S f)))$
47	46	an4s	$⊢ ((R Po A \land S Po B) \land ((a \in A \land c \in A \land e \in A) \land (b \in B \land d \in B \land f \in B))) \to (((a R c \lor (a = c \land b S d)) \land (c R e \lor (c = e \land d S f))) \to (a R e \lor (a = e \land b S f)))$
48	18 47	sylan2b	$⊢ ((R Po A \land S Po B) \land ((a \in A \land b \in B) \land (c \in A \land d \in B) \land (e \in A \land f \in B))) \to (((a R c \lor (a = c \land b S d)) \land (c R e \lor (c = e \land d S f))) \to (a R e \lor (a = e \land b S f)))$
49		an4	$⊢ ((a \in A \land b \in B) \land (e \in A \land f \in B)) \leftrightarrow ((a \in A \land e \in A) \land (b \in B \land f \in B))$
50	49	biimpi	$⊢ ((a \in A \land b \in B) \land (e \in A \land f \in B)) \to ((a \in A \land e \in A) \land (b \in B \land f \in B))$
51	50	3adant2	$⊢ ((a \in A \land b \in B) \land (c \in A \land d \in B) \land (e \in A \land f \in B)) \to ((a \in A \land e \in A) \land (b \in B \land f \in B))$
52	51	adantl	$⊢ ((R Po A \land S Po B) \land ((a \in A \land b \in B) \land (c \in A \land d \in B) \land (e \in A \land f \in B))) \to ((a \in A \land e \in A) \land (b \in B \land f \in B))$
53	48 52	jctild	$⊢ ((R Po A \land S Po B) \land ((a \in A \land b \in B) \land (c \in A \land d \in B) \land (e \in A \land f \in B))) \to (((a R c \lor (a = c \land b S d)) \land (c R e \lor (c = e \land d S f))) \to (((a \in A \land e \in A) \land (b \in B \land f \in B)) \land (a R e \lor (a = e \land b S f))))$
54	53	adantld	$⊢ ((R Po A \land S Po B) \land ((a \in A \land b \in B) \land (c \in A \land d \in B) \land (e \in A \land f \in B))) \to (((((a \in A \land c \in A) \land (b \in B \land d \in B)) \land ((c \in A \land e \in A) \land (d \in B \land f \in B))) \land ((a R c \lor (a = c \land b S d)) \land (c R e \lor (c = e \land d S f)))) \to (((a \in A \land e \in A) \land (b \in B \land f \in B)) \land (a R e \lor (a = e \land b S f))))$
55	17 54	syl5bi	$⊢ ((R Po A \land S Po B) \land ((a \in A \land b \in B) \land (c \in A \land d \in B) \land (e \in A \land f \in B))) \to (((((a \in A \land c \in A) \land (b \in B \land d \in B)) \land (a R c \lor (a = c \land b S d))) \land (((c \in A \land e \in A) \land (d \in B \land f \in B)) \land (c R e \lor (c = e \land d S f)))) \to (((a \in A \land e \in A) \land (b \in B \land f \in B)) \land (a R e \lor (a = e \land b S f))))$
56	16 55	jca	$⊢ ((R Po A \land S Po B) \land ((a \in A \land b \in B) \land (c \in A \land d \in B) \land (e \in A \land f \in B))) \to (\neg (((a \in A \land a \in A) \land (b \in B \land b \in B)) \land (a R a \lor (a = a \land b S b))) \land (((((a \in A \land c \in A) \land (b \in B \land d \in B)) \land (a R c \lor (a = c \land b S d))) \land (((c \in A \land e \in A) \land (d \in B \land f \in B)) \land (c R e \lor (c = e \land d S f)))) \to (((a \in A \land e \in A) \land (b \in B \land f \in B)) \land (a R e \lor (a = e \land b S f)))))$
57		breq12	$⊢ (t = ⟨a, b⟩ \land t = ⟨a, b⟩) \to (t T t \leftrightarrow ⟨a, b⟩ T ⟨a, b⟩)$
58	57	anidms	$⊢ t = ⟨a, b⟩ \to (t T t \leftrightarrow ⟨a, b⟩ T ⟨a, b⟩)$
59	58	notbid	$⊢ t = ⟨a, b⟩ \to (\neg t T t \leftrightarrow \neg ⟨a, b⟩ T ⟨a, b⟩)$
60	59	3ad2ant1	$⊢ (t = ⟨a, b⟩ \land u = ⟨c, d⟩ \land v = ⟨e, f⟩) \to (\neg t T t \leftrightarrow \neg ⟨a, b⟩ T ⟨a, b⟩)$
61		breq12	$⊢ (t = ⟨a, b⟩ \land u = ⟨c, d⟩) \to (t T u \leftrightarrow ⟨a, b⟩ T ⟨c, d⟩)$
62	61	3adant3	$⊢ (t = ⟨a, b⟩ \land u = ⟨c, d⟩ \land v = ⟨e, f⟩) \to (t T u \leftrightarrow ⟨a, b⟩ T ⟨c, d⟩)$
63		breq12	$⊢ (u = ⟨c, d⟩ \land v = ⟨e, f⟩) \to (u T v \leftrightarrow ⟨c, d⟩ T ⟨e, f⟩)$
64	63	3adant1	$⊢ (t = ⟨a, b⟩ \land u = ⟨c, d⟩ \land v = ⟨e, f⟩) \to (u T v \leftrightarrow ⟨c, d⟩ T ⟨e, f⟩)$
65	62 64	anbi12d	$⊢ (t = ⟨a, b⟩ \land u = ⟨c, d⟩ \land v = ⟨e, f⟩) \to ((t T u \land u T v) \leftrightarrow (⟨a, b⟩ T ⟨c, d⟩ \land ⟨c, d⟩ T ⟨e, f⟩))$
66		breq12	$⊢ (t = ⟨a, b⟩ \land v = ⟨e, f⟩) \to (t T v \leftrightarrow ⟨a, b⟩ T ⟨e, f⟩)$
67	66	3adant2	$⊢ (t = ⟨a, b⟩ \land u = ⟨c, d⟩ \land v = ⟨e, f⟩) \to (t T v \leftrightarrow ⟨a, b⟩ T ⟨e, f⟩)$
68	65 67	imbi12d	$⊢ (t = ⟨a, b⟩ \land u = ⟨c, d⟩ \land v = ⟨e, f⟩) \to (((t T u \land u T v) \to t T v) \leftrightarrow ((⟨a, b⟩ T ⟨c, d⟩ \land ⟨c, d⟩ T ⟨e, f⟩) \to ⟨a, b⟩ T ⟨e, f⟩))$
69	60 68	anbi12d	$⊢ (t = ⟨a, b⟩ \land u = ⟨c, d⟩ \land v = ⟨e, f⟩) \to ((\neg t T t \land ((t T u \land u T v) \to t T v)) \leftrightarrow (\neg ⟨a, b⟩ T ⟨a, b⟩ \land ((⟨a, b⟩ T ⟨c, d⟩ \land ⟨c, d⟩ T ⟨e, f⟩) \to ⟨a, b⟩ T ⟨e, f⟩)))$
70	1	xporderlem	$⊢ ⟨a, b⟩ T ⟨a, b⟩ \leftrightarrow (((a \in A \land a \in A) \land (b \in B \land b \in B)) \land (a R a \lor (a = a \land b S b)))$
71	70	notbii	$⊢ \neg ⟨a, b⟩ T ⟨a, b⟩ \leftrightarrow \neg (((a \in A \land a \in A) \land (b \in B \land b \in B)) \land (a R a \lor (a = a \land b S b)))$
72	1	xporderlem	$⊢ ⟨a, b⟩ T ⟨c, d⟩ \leftrightarrow (((a \in A \land c \in A) \land (b \in B \land d \in B)) \land (a R c \lor (a = c \land b S d)))$
73	1	xporderlem	$⊢ ⟨c, d⟩ T ⟨e, f⟩ \leftrightarrow (((c \in A \land e \in A) \land (d \in B \land f \in B)) \land (c R e \lor (c = e \land d S f)))$
74	72 73	anbi12i	$⊢ (⟨a, b⟩ T ⟨c, d⟩ \land ⟨c, d⟩ T ⟨e, f⟩) \leftrightarrow ((((a \in A \land c \in A) \land (b \in B \land d \in B)) \land (a R c \lor (a = c \land b S d))) \land (((c \in A \land e \in A) \land (d \in B \land f \in B)) \land (c R e \lor (c = e \land d S f))))$
75	1	xporderlem	$⊢ ⟨a, b⟩ T ⟨e, f⟩ \leftrightarrow (((a \in A \land e \in A) \land (b \in B \land f \in B)) \land (a R e \lor (a = e \land b S f)))$
76	74 75	imbi12i	$⊢ ((⟨a, b⟩ T ⟨c, d⟩ \land ⟨c, d⟩ T ⟨e, f⟩) \to ⟨a, b⟩ T ⟨e, f⟩) \leftrightarrow (((((a \in A \land c \in A) \land (b \in B \land d \in B)) \land (a R c \lor (a = c \land b S d))) \land (((c \in A \land e \in A) \land (d \in B \land f \in B)) \land (c R e \lor (c = e \land d S f)))) \to (((a \in A \land e \in A) \land (b \in B \land f \in B)) \land (a R e \lor (a = e \land b S f))))$
77	71 76	anbi12i	$⊢ (\neg ⟨a, b⟩ T ⟨a, b⟩ \land ((⟨a, b⟩ T ⟨c, d⟩ \land ⟨c, d⟩ T ⟨e, f⟩) \to ⟨a, b⟩ T ⟨e, f⟩)) \leftrightarrow (\neg (((a \in A \land a \in A) \land (b \in B \land b \in B)) \land (a R a \lor (a = a \land b S b))) \land (((((a \in A \land c \in A) \land (b \in B \land d \in B)) \land (a R c \lor (a = c \land b S d))) \land (((c \in A \land e \in A) \land (d \in B \land f \in B)) \land (c R e \lor (c = e \land d S f)))) \to (((a \in A \land e \in A) \land (b \in B \land f \in B)) \land (a R e \lor (a = e \land b S f)))))$
78	69 77	syl6bb	$⊢ (t = ⟨a, b⟩ \land u = ⟨c, d⟩ \land v = ⟨e, f⟩) \to ((\neg t T t \land ((t T u \land u T v) \to t T v)) \leftrightarrow (\neg (((a \in A \land a \in A) \land (b \in B \land b \in B)) \land (a R a \lor (a = a \land b S b))) \land (((((a \in A \land c \in A) \land (b \in B \land d \in B)) \land (a R c \lor (a = c \land b S d))) \land (((c \in A \land e \in A) \land (d \in B \land f \in B)) \land (c R e \lor (c = e \land d S f)))) \to (((a \in A \land e \in A) \land (b \in B \land f \in B)) \land (a R e \lor (a = e \land b S f))))))$
79	56 78	syl5ibr	$⊢ (t = ⟨a, b⟩ \land u = ⟨c, d⟩ \land v = ⟨e, f⟩) \to (((R Po A \land S Po B) \land ((a \in A \land b \in B) \land (c \in A \land d \in B) \land (e \in A \land f \in B))) \to (\neg t T t \land ((t T u \land u T v) \to t T v)))$
80	79	expcomd	$⊢ (t = ⟨a, b⟩ \land u = ⟨c, d⟩ \land v = ⟨e, f⟩) \to (((a \in A \land b \in B) \land (c \in A \land d \in B) \land (e \in A \land f \in B)) \to ((R Po A \land S Po B) \to (\neg t T t \land ((t T u \land u T v) \to t T v))))$
81	80	imp	$⊢ ((t = ⟨a, b⟩ \land u = ⟨c, d⟩ \land v = ⟨e, f⟩) \land ((a \in A \land b \in B) \land (c \in A \land d \in B) \land (e \in A \land f \in B))) \to ((R Po A \land S Po B) \to (\neg t T t \land ((t T u \land u T v) \to t T v)))$
82	5 81	sylbi	$⊢ ((t = ⟨a, b⟩ \land (a \in A \land b \in B)) \land (u = ⟨c, d⟩ \land (c \in A \land d \in B)) \land (v = ⟨e, f⟩ \land (e \in A \land f \in B))) \to ((R Po A \land S Po B) \to (\neg t T t \land ((t T u \land u T v) \to t T v)))$
83	82	3exp	$⊢ (t = ⟨a, b⟩ \land (a \in A \land b \in B)) \to ((u = ⟨c, d⟩ \land (c \in A \land d \in B)) \to ((v = ⟨e, f⟩ \land (e \in A \land f \in B)) \to ((R Po A \land S Po B) \to (\neg t T t \land ((t T u \land u T v) \to t T v)))))$
84	83	com3l	$⊢ (u = ⟨c, d⟩ \land (c \in A \land d \in B)) \to ((v = ⟨e, f⟩ \land (e \in A \land f \in B)) \to ((t = ⟨a, b⟩ \land (a \in A \land b \in B)) \to ((R Po A \land S Po B) \to (\neg t T t \land ((t T u \land u T v) \to t T v)))))$
85	84	exlimivv	$⊢ \exists c \exists d (u = ⟨c, d⟩ \land (c \in A \land d \in B)) \to ((v = ⟨e, f⟩ \land (e \in A \land f \in B)) \to ((t = ⟨a, b⟩ \land (a \in A \land b \in B)) \to ((R Po A \land S Po B) \to (\neg t T t \land ((t T u \land u T v) \to t T v)))))$
86	85	com3l	$⊢ (v = ⟨e, f⟩ \land (e \in A \land f \in B)) \to ((t = ⟨a, b⟩ \land (a \in A \land b \in B)) \to (\exists c \exists d (u = ⟨c, d⟩ \land (c \in A \land d \in B)) \to ((R Po A \land S Po B) \to (\neg t T t \land ((t T u \land u T v) \to t T v)))))$
87	86	exlimivv	$⊢ \exists e \exists f (v = ⟨e, f⟩ \land (e \in A \land f \in B)) \to ((t = ⟨a, b⟩ \land (a \in A \land b \in B)) \to (\exists c \exists d (u = ⟨c, d⟩ \land (c \in A \land d \in B)) \to ((R Po A \land S Po B) \to (\neg t T t \land ((t T u \land u T v) \to t T v)))))$
88	87	com3l	$⊢ (t = ⟨a, b⟩ \land (a \in A \land b \in B)) \to (\exists c \exists d (u = ⟨c, d⟩ \land (c \in A \land d \in B)) \to (\exists e \exists f (v = ⟨e, f⟩ \land (e \in A \land f \in B)) \to ((R Po A \land S Po B) \to (\neg t T t \land ((t T u \land u T v) \to t T v)))))$
89	88	exlimivv	$⊢ \exists a \exists b (t = ⟨a, b⟩ \land (a \in A \land b \in B)) \to (\exists c \exists d (u = ⟨c, d⟩ \land (c \in A \land d \in B)) \to (\exists e \exists f (v = ⟨e, f⟩ \land (e \in A \land f \in B)) \to ((R Po A \land S Po B) \to (\neg t T t \land ((t T u \land u T v) \to t T v)))))$
90	89	3imp	$⊢ (\exists a \exists b (t = ⟨a, b⟩ \land (a \in A \land b \in B)) \land \exists c \exists d (u = ⟨c, d⟩ \land (c \in A \land d \in B)) \land \exists e \exists f (v = ⟨e, f⟩ \land (e \in A \land f \in B))) \to ((R Po A \land S Po B) \to (\neg t T t \land ((t T u \land u T v) \to t T v)))$
91	2 3 4 90	syl3anb	$⊢ (t \in (A \times B) \land u \in (A \times B) \land v \in (A \times B)) \to ((R Po A \land S Po B) \to (\neg t T t \land ((t T u \land u T v) \to t T v)))$
92	91	3expia	$⊢ (t \in (A \times B) \land u \in (A \times B)) \to (v \in (A \times B) \to ((R Po A \land S Po B) \to (\neg t T t \land ((t T u \land u T v) \to t T v))))$
93	92	com3r	$⊢ (R Po A \land S Po B) \to ((t \in (A \times B) \land u \in (A \times B)) \to (v \in (A \times B) \to (\neg t T t \land ((t T u \land u T v) \to t T v))))$
94	93	imp	$⊢ ((R Po A \land S Po B) \land (t \in (A \times B) \land u \in (A \times B))) \to (v \in (A \times B) \to (\neg t T t \land ((t T u \land u T v) \to t T v)))$
95	94	ralrimiv	$⊢ ((R Po A \land S Po B) \land (t \in (A \times B) \land u \in (A \times B))) \to \forall v \in (A \times B) (\neg t T t \land ((t T u \land u T v) \to t T v))$
96	95	ralrimivva	$⊢ (R Po A \land S Po B) \to \forall t \in (A \times B) \forall u \in (A \times B) \forall v \in (A \times B) (\neg t T t \land ((t T u \land u T v) \to t T v))$
97		df-po	$⊢ T Po (A \times B) \leftrightarrow \forall t \in (A \times B) \forall u \in (A \times B) \forall v \in (A \times B) (\neg t T t \land ((t T u \land u T v) \to t T v))$
98	96 97	sylibr	$⊢ (R Po A \land S Po B) \to T Po (A \times B)$

Metamath Proof Explorer

Theorem poxp

Proof