poxp2

Description: Another way of partially ordering a Cartesian product of two classes. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Hypotheses	xpord2.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) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}$
	poxp2.1	$⊢ φ \to R Po A$
	poxp2.2	$⊢ φ \to S Po B$
Assertion	poxp2	$⊢ φ \to T Po (A \times B)$

Proof

Step	Hyp	Ref	Expression
1		xpord2.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) \lor 2^{nd} (x) = 2^{nd} (y)) \land x \neq y))\}$
2		poxp2.1	$⊢ φ \to R Po A$
3		poxp2.2	$⊢ φ \to S Po B$
4		elxp2	$⊢ a \in (A \times B) \leftrightarrow \exists p \in A \exists q \in B a = ⟨p, q⟩$
5		equid	$⊢ p = p$
6		equid	$⊢ q = q$
7	5 6	pm3.2i	$⊢ (p = p \land q = q)$
8		neorian	$⊢ (p \neq p \lor q \neq q) \leftrightarrow \neg (p = p \land q = q)$
9	8	con2bii	$⊢ (p = p \land q = q) \leftrightarrow \neg (p \neq p \lor q \neq q)$
10	7 9	mpbi	$⊢ \neg (p \neq p \lor q \neq q)$
11		simp3	$⊢ ((p R p \lor p = p) \land (q S q \lor q = q) \land (p \neq p \lor q \neq q)) \to (p \neq p \lor q \neq q)$
12	10 11	mto	$⊢ \neg ((p R p \lor p = p) \land (q S q \lor q = q) \land (p \neq p \lor q \neq q))$
13		simp3	$⊢ ((p \in A \land q \in B) \land (p \in A \land q \in B) \land ((p R p \lor p = p) \land (q S q \lor q = q) \land (p \neq p \lor q \neq q))) \to ((p R p \lor p = p) \land (q S q \lor q = q) \land (p \neq p \lor q \neq q))$
14	12 13	mto	$⊢ \neg ((p \in A \land q \in B) \land (p \in A \land q \in B) \land ((p R p \lor p = p) \land (q S q \lor q = q) \land (p \neq p \lor q \neq q)))$
15	1	xpord2lem	$⊢ ⟨p, q⟩ T ⟨p, q⟩ \leftrightarrow ((p \in A \land q \in B) \land (p \in A \land q \in B) \land ((p R p \lor p = p) \land (q S q \lor q = q) \land (p \neq p \lor q \neq q)))$
16	14 15	mtbir	$⊢ \neg ⟨p, q⟩ T ⟨p, q⟩$
17		breq12	$⊢ (a = ⟨p, q⟩ \land a = ⟨p, q⟩) \to (a T a \leftrightarrow ⟨p, q⟩ T ⟨p, q⟩)$
18	17	anidms	$⊢ a = ⟨p, q⟩ \to (a T a \leftrightarrow ⟨p, q⟩ T ⟨p, q⟩)$
19	16 18	mtbiri	$⊢ a = ⟨p, q⟩ \to \neg a T a$
20	19	rexlimivw	$⊢ \exists q \in B a = ⟨p, q⟩ \to \neg a T a$
21	20	rexlimivw	$⊢ \exists p \in A \exists q \in B a = ⟨p, q⟩ \to \neg a T a$
22	4 21	sylbi	$⊢ a \in (A \times B) \to \neg a T a$
23	22	adantl	$⊢ (φ \land a \in (A \times B)) \to \neg a T a$
24		3reeanv	$⊢ \exists p \in A \exists r \in A \exists t \in A (\exists q \in B a = ⟨p, q⟩ \land \exists s \in B b = ⟨r, s⟩ \land \exists u \in B c = ⟨t, u⟩) \leftrightarrow (\exists p \in A \exists q \in B a = ⟨p, q⟩ \land \exists r \in A \exists s \in B b = ⟨r, s⟩ \land \exists t \in A \exists u \in B c = ⟨t, u⟩)$
25		3reeanv	$⊢ \exists q \in B \exists s \in B \exists u \in B (a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \leftrightarrow (\exists q \in B a = ⟨p, q⟩ \land \exists s \in B b = ⟨r, s⟩ \land \exists u \in B c = ⟨t, u⟩)$
26	25	rexbii	$⊢ \exists t \in A \exists q \in B \exists s \in B \exists u \in B (a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \leftrightarrow \exists t \in A (\exists q \in B a = ⟨p, q⟩ \land \exists s \in B b = ⟨r, s⟩ \land \exists u \in B c = ⟨t, u⟩)$
27	26	2rexbii	$⊢ \exists p \in A \exists r \in A \exists t \in A \exists q \in B \exists s \in B \exists u \in B (a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \leftrightarrow \exists p \in A \exists r \in A \exists t \in A (\exists q \in B a = ⟨p, q⟩ \land \exists s \in B b = ⟨r, s⟩ \land \exists u \in B c = ⟨t, u⟩)$
28		elxp2	$⊢ b \in (A \times B) \leftrightarrow \exists r \in A \exists s \in B b = ⟨r, s⟩$
29		elxp2	$⊢ c \in (A \times B) \leftrightarrow \exists t \in A \exists u \in B c = ⟨t, u⟩$
30	4 28 29	3anbi123i	$⊢ (a \in (A \times B) \land b \in (A \times B) \land c \in (A \times B)) \leftrightarrow (\exists p \in A \exists q \in B a = ⟨p, q⟩ \land \exists r \in A \exists s \in B b = ⟨r, s⟩ \land \exists t \in A \exists u \in B c = ⟨t, u⟩)$
31	24 27 30	3bitr4ri	$⊢ (a \in (A \times B) \land b \in (A \times B) \land c \in (A \times B)) \leftrightarrow \exists p \in A \exists r \in A \exists t \in A \exists q \in B \exists s \in B \exists u \in B (a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩)$
32		df-3an	$⊢ ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B)) \leftrightarrow (((p \in A \land r \in A) \land (t \in A \land q \in B)) \land (s \in B \land u \in B))$
33		simp3	$⊢ ((p \in A \land q \in B) \land (r \in A \land s \in B) \land ((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s))) \to ((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s))$
34		simp3	$⊢ ((r \in A \land s \in B) \land (t \in A \land u \in B) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u))) \to ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u))$
35		simpr1l	$⊢ (φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \to p \in A$
36	35	adantr	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to p \in A$
37		simpr2r	$⊢ (φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \to q \in B$
38	37	adantr	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to q \in B$
39	36 38	jca	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (p \in A \land q \in B)$
40		simpr2l	$⊢ (φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \to t \in A$
41	40	adantr	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to t \in A$
42		simpr3r	$⊢ (φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \to u \in B$
43	42	adantr	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to u \in B$
44	41 43	jca	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (t \in A \land u \in B)$
45	2	ad2antrr	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to R Po A$
46		simpr1r	$⊢ (φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \to r \in A$
47	46	adantr	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to r \in A$
48		potr	$⊢ (R Po A \land (p \in A \land r \in A \land t \in A)) \to ((p R r \land r R t) \to p R t)$
49	45 36 47 41 48	syl13anc	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to ((p R r \land r R t) \to p R t)$
50		orc	$⊢ p R t \to (p R t \lor p = t)$
51	49 50	syl6	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to ((p R r \land r R t) \to (p R t \lor p = t))$
52	51	expd	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (p R r \to (r R t \to (p R t \lor p = t)))$
53		breq1	$⊢ p = r \to (p R t \leftrightarrow r R t)$
54	53 50	syl6bir	$⊢ p = r \to (r R t \to (p R t \lor p = t))$
55	54	a1i	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (p = r \to (r R t \to (p R t \lor p = t)))$
56		simprl1	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (p R r \lor p = r)$
57	52 55 56	mpjaod	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (r R t \to (p R t \lor p = t))$
58		breq2	$⊢ r = t \to (p R r \leftrightarrow p R t)$
59		equequ2	$⊢ r = t \to (p = r \leftrightarrow p = t)$
60	58 59	orbi12d	$⊢ r = t \to ((p R r \lor p = r) \leftrightarrow (p R t \lor p = t))$
61	56 60	syl5ibcom	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (r = t \to (p R t \lor p = t))$
62		simprr1	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (r R t \lor r = t)$
63	57 61 62	mpjaod	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (p R t \lor p = t)$
64	3	ad2antrr	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to S Po B$
65		simpr3l	$⊢ (φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \to s \in B$
66	65	adantr	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to s \in B$
67		potr	$⊢ (S Po B \land (q \in B \land s \in B \land u \in B)) \to ((q S s \land s S u) \to q S u)$
68	64 38 66 43 67	syl13anc	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to ((q S s \land s S u) \to q S u)$
69		orc	$⊢ q S u \to (q S u \lor q = u)$
70	68 69	syl6	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to ((q S s \land s S u) \to (q S u \lor q = u))$
71	70	expd	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (q S s \to (s S u \to (q S u \lor q = u)))$
72		breq1	$⊢ q = s \to (q S u \leftrightarrow s S u)$
73	72 69	syl6bir	$⊢ q = s \to (s S u \to (q S u \lor q = u))$
74	73	a1i	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (q = s \to (s S u \to (q S u \lor q = u)))$
75		simprl2	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (q S s \lor q = s)$
76	71 74 75	mpjaod	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (s S u \to (q S u \lor q = u))$
77		breq2	$⊢ s = u \to (q S s \leftrightarrow q S u)$
78		equequ2	$⊢ s = u \to (q = s \leftrightarrow q = u)$
79	77 78	orbi12d	$⊢ s = u \to ((q S s \lor q = s) \leftrightarrow (q S u \lor q = u))$
80	75 79	syl5ibcom	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (s = u \to (q S u \lor q = u))$
81		simprr2	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (s S u \lor s = u)$
82	76 80 81	mpjaod	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (q S u \lor q = u)$
83		simprr3	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (r \neq t \lor s \neq u)$
84		neorian	$⊢ (r \neq t \lor s \neq u) \leftrightarrow \neg (r = t \land s = u)$
85	83 84	sylib	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to \neg (r = t \land s = u)$
86		neorian	$⊢ (p \neq t \lor q \neq u) \leftrightarrow \neg (p = t \land q = u)$
87	86	con2bii	$⊢ (p = t \land q = u) \leftrightarrow \neg (p \neq t \lor q \neq u)$
88		breq1	$⊢ p = t \to (p R r \leftrightarrow t R r)$
89		equequ1	$⊢ p = t \to (p = r \leftrightarrow t = r)$
90	88 89	orbi12d	$⊢ p = t \to ((p R r \lor p = r) \leftrightarrow (t R r \lor t = r))$
91	90	adantr	$⊢ (p = t \land q = u) \to ((p R r \lor p = r) \leftrightarrow (t R r \lor t = r))$
92		breq1	$⊢ q = u \to (q S s \leftrightarrow u S s)$
93		equequ1	$⊢ q = u \to (q = s \leftrightarrow u = s)$
94	92 93	orbi12d	$⊢ q = u \to ((q S s \lor q = s) \leftrightarrow (u S s \lor u = s))$
95	94	adantl	$⊢ (p = t \land q = u) \to ((q S s \lor q = s) \leftrightarrow (u S s \lor u = s))$
96		neeq1	$⊢ p = t \to (p \neq r \leftrightarrow t \neq r)$
97	96	adantr	$⊢ (p = t \land q = u) \to (p \neq r \leftrightarrow t \neq r)$
98		neeq1	$⊢ q = u \to (q \neq s \leftrightarrow u \neq s)$
99	98	adantl	$⊢ (p = t \land q = u) \to (q \neq s \leftrightarrow u \neq s)$
100	97 99	orbi12d	$⊢ (p = t \land q = u) \to ((p \neq r \lor q \neq s) \leftrightarrow (t \neq r \lor u \neq s))$
101	91 95 100	3anbi123d	$⊢ (p = t \land q = u) \to (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \leftrightarrow ((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)))$
102	101	anbi1d	$⊢ (p = t \land q = u) \to ((((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u))) \leftrightarrow (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u))))$
103	102	anbi2d	$⊢ (p = t \land q = u) \to (((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \leftrightarrow ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))))$
104		simprl1	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (t R r \lor t = r)$
105		simprr1	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (r R t \lor r = t)$
106		orcom	$⊢ ((t R r \land r R t) \lor r = t) \leftrightarrow (r = t \lor (t R r \land r R t))$
107		ordi	$⊢ (r = t \lor (t R r \land r R t)) \leftrightarrow ((r = t \lor t R r) \land (r = t \lor r R t))$
108		orcom	$⊢ (r = t \lor t R r) \leftrightarrow (t R r \lor r = t)$
109		equcom	$⊢ r = t \leftrightarrow t = r$
110	109	orbi2i	$⊢ (t R r \lor r = t) \leftrightarrow (t R r \lor t = r)$
111	108 110	bitri	$⊢ (r = t \lor t R r) \leftrightarrow (t R r \lor t = r)$
112		orcom	$⊢ (r = t \lor r R t) \leftrightarrow (r R t \lor r = t)$
113	111 112	anbi12i	$⊢ ((r = t \lor t R r) \land (r = t \lor r R t)) \leftrightarrow ((t R r \lor t = r) \land (r R t \lor r = t))$
114	106 107 113	3bitri	$⊢ ((t R r \land r R t) \lor r = t) \leftrightarrow ((t R r \lor t = r) \land (r R t \lor r = t))$
115	104 105 114	sylanbrc	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to ((t R r \land r R t) \lor r = t)$
116	2	ad2antrr	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to R Po A$
117	40	adantr	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to t \in A$
118	46	adantr	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to r \in A$
119		po2nr	$⊢ (R Po A \land (t \in A \land r \in A)) \to \neg (t R r \land r R t)$
120	116 117 118 119	syl12anc	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to \neg (t R r \land r R t)$
121	115 120	orcnd	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to r = t$
122		simprl2	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (u S s \lor u = s)$
123		simprr2	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (s S u \lor s = u)$
124		orcom	$⊢ ((u S s \land s S u) \lor s = u) \leftrightarrow (s = u \lor (u S s \land s S u))$
125		ordi	$⊢ (s = u \lor (u S s \land s S u)) \leftrightarrow ((s = u \lor u S s) \land (s = u \lor s S u))$
126		orcom	$⊢ (s = u \lor u S s) \leftrightarrow (u S s \lor s = u)$
127		equcom	$⊢ s = u \leftrightarrow u = s$
128	127	orbi2i	$⊢ (u S s \lor s = u) \leftrightarrow (u S s \lor u = s)$
129	126 128	bitri	$⊢ (s = u \lor u S s) \leftrightarrow (u S s \lor u = s)$
130		orcom	$⊢ (s = u \lor s S u) \leftrightarrow (s S u \lor s = u)$
131	129 130	anbi12i	$⊢ ((s = u \lor u S s) \land (s = u \lor s S u)) \leftrightarrow ((u S s \lor u = s) \land (s S u \lor s = u))$
132	124 125 131	3bitri	$⊢ ((u S s \land s S u) \lor s = u) \leftrightarrow ((u S s \lor u = s) \land (s S u \lor s = u))$
133	122 123 132	sylanbrc	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to ((u S s \land s S u) \lor s = u)$
134	3	ad2antrr	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to S Po B$
135	42	adantr	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to u \in B$
136	65	adantr	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to s \in B$
137		po2nr	$⊢ (S Po B \land (u \in B \land s \in B)) \to \neg (u S s \land s S u)$
138	134 135 136 137	syl12anc	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to \neg (u S s \land s S u)$
139	133 138	orcnd	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to s = u$
140	121 139	jca	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((t R r \lor t = r) \land (u S s \lor u = s) \land (t \neq r \lor u \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (r = t \land s = u)$
141	103 140	biimtrdi	$⊢ (p = t \land q = u) \to (((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (r = t \land s = u))$
142	141	com12	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to ((p = t \land q = u) \to (r = t \land s = u))$
143	87 142	biimtrrid	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (\neg (p \neq t \lor q \neq u) \to (r = t \land s = u))$
144	85 143	mt3d	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to (p \neq t \lor q \neq u)$
145	63 82 144	3jca	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to ((p R t \lor p = t) \land (q S u \lor q = u) \land (p \neq t \lor q \neq u))$
146	39 44 145	3jca	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \land (((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to ((p \in A \land q \in B) \land (t \in A \land u \in B) \land ((p R t \lor p = t) \land (q S u \lor q = u) \land (p \neq t \lor q \neq u)))$
147	146	ex	$⊢ (φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \to ((((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u))) \to ((p \in A \land q \in B) \land (t \in A \land u \in B) \land ((p R t \lor p = t) \land (q S u \lor q = u) \land (p \neq t \lor q \neq u))))$
148	33 34 147	syl2ani	$⊢ (φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \to ((((p \in A \land q \in B) \land (r \in A \land s \in B) \land ((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s))) \land ((r \in A \land s \in B) \land (t \in A \land u \in B) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to ((p \in A \land q \in B) \land (t \in A \land u \in B) \land ((p R t \lor p = t) \land (q S u \lor q = u) \land (p \neq t \lor q \neq u))))$
149		breq12	$⊢ (a = ⟨p, q⟩ \land b = ⟨r, s⟩) \to (a T b \leftrightarrow ⟨p, q⟩ T ⟨r, s⟩)$
150	149	3adant3	$⊢ (a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \to (a T b \leftrightarrow ⟨p, q⟩ T ⟨r, s⟩)$
151	1	xpord2lem	$⊢ ⟨p, q⟩ T ⟨r, s⟩ \leftrightarrow ((p \in A \land q \in B) \land (r \in A \land s \in B) \land ((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s)))$
152	150 151	bitrdi	$⊢ (a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \to (a T b \leftrightarrow ((p \in A \land q \in B) \land (r \in A \land s \in B) \land ((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s))))$
153		breq12	$⊢ (b = ⟨r, s⟩ \land c = ⟨t, u⟩) \to (b T c \leftrightarrow ⟨r, s⟩ T ⟨t, u⟩)$
154	153	3adant1	$⊢ (a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \to (b T c \leftrightarrow ⟨r, s⟩ T ⟨t, u⟩)$
155	1	xpord2lem	$⊢ ⟨r, s⟩ T ⟨t, u⟩ \leftrightarrow ((r \in A \land s \in B) \land (t \in A \land u \in B) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))$
156	154 155	bitrdi	$⊢ (a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \to (b T c \leftrightarrow ((r \in A \land s \in B) \land (t \in A \land u \in B) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u))))$
157	152 156	anbi12d	$⊢ (a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \to ((a T b \land b T c) \leftrightarrow (((p \in A \land q \in B) \land (r \in A \land s \in B) \land ((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s))) \land ((r \in A \land s \in B) \land (t \in A \land u \in B) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))))$
158		breq12	$⊢ (a = ⟨p, q⟩ \land c = ⟨t, u⟩) \to (a T c \leftrightarrow ⟨p, q⟩ T ⟨t, u⟩)$
159	158	3adant2	$⊢ (a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \to (a T c \leftrightarrow ⟨p, q⟩ T ⟨t, u⟩)$
160	1	xpord2lem	$⊢ ⟨p, q⟩ T ⟨t, u⟩ \leftrightarrow ((p \in A \land q \in B) \land (t \in A \land u \in B) \land ((p R t \lor p = t) \land (q S u \lor q = u) \land (p \neq t \lor q \neq u)))$
161	159 160	bitrdi	$⊢ (a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \to (a T c \leftrightarrow ((p \in A \land q \in B) \land (t \in A \land u \in B) \land ((p R t \lor p = t) \land (q S u \lor q = u) \land (p \neq t \lor q \neq u))))$
162	157 161	imbi12d	$⊢ (a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \to (((a T b \land b T c) \to a T c) \leftrightarrow ((((p \in A \land q \in B) \land (r \in A \land s \in B) \land ((p R r \lor p = r) \land (q S s \lor q = s) \land (p \neq r \lor q \neq s))) \land ((r \in A \land s \in B) \land (t \in A \land u \in B) \land ((r R t \lor r = t) \land (s S u \lor s = u) \land (r \neq t \lor s \neq u)))) \to ((p \in A \land q \in B) \land (t \in A \land u \in B) \land ((p R t \lor p = t) \land (q S u \lor q = u) \land (p \neq t \lor q \neq u)))))$
163	148 162	syl5ibrcom	$⊢ (φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B) \land (s \in B \land u \in B))) \to ((a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \to ((a T b \land b T c) \to a T c))$
164	32 163	sylan2br	$⊢ (φ \land (((p \in A \land r \in A) \land (t \in A \land q \in B)) \land (s \in B \land u \in B))) \to ((a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \to ((a T b \land b T c) \to a T c))$
165	164	anassrs	$⊢ ((φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B))) \land (s \in B \land u \in B)) \to ((a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \to ((a T b \land b T c) \to a T c))$
166	165	rexlimdvva	$⊢ (φ \land ((p \in A \land r \in A) \land (t \in A \land q \in B))) \to (\exists s \in B \exists u \in B (a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \to ((a T b \land b T c) \to a T c))$
167	166	anassrs	$⊢ ((φ \land (p \in A \land r \in A)) \land (t \in A \land q \in B)) \to (\exists s \in B \exists u \in B (a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \to ((a T b \land b T c) \to a T c))$
168	167	rexlimdvva	$⊢ (φ \land (p \in A \land r \in A)) \to (\exists t \in A \exists q \in B \exists s \in B \exists u \in B (a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \to ((a T b \land b T c) \to a T c))$
169	168	rexlimdvva	$⊢ φ \to (\exists p \in A \exists r \in A \exists t \in A \exists q \in B \exists s \in B \exists u \in B (a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩) \to ((a T b \land b T c) \to a T c))$
170	169	imp	$⊢ (φ \land \exists p \in A \exists r \in A \exists t \in A \exists q \in B \exists s \in B \exists u \in B (a = ⟨p, q⟩ \land b = ⟨r, s⟩ \land c = ⟨t, u⟩)) \to ((a T b \land b T c) \to a T c)$
171	31 170	sylan2b	$⊢ (φ \land (a \in (A \times B) \land b \in (A \times B) \land c \in (A \times B))) \to ((a T b \land b T c) \to a T c)$
172	23 171	ispod	$⊢ φ \to T Po (A \times B)$

Metamath Proof Explorer

Theorem poxp2

Proof