ltsosr

Description: Signed real 'less than' is a strict ordering. (Contributed by NM, 19-Feb-1996) (New usage is discouraged.)

		Ref	Expression
	Assertion	ltsosr	$⊢ <_{𝑹} Or 𝑹$

Proof

Step	Hyp	Ref	Expression
1		df-nr	$⊢ 𝑹 = (𝑷 \times 𝑷) / ~_{𝑹}$
2		breq1	$⊢ [⟨x, y⟩] ~_{𝑹} = f \to ([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow f <_{𝑹} [⟨z, w⟩] ~_{𝑹})$
3		eqeq1	$⊢ [⟨x, y⟩] ~_{𝑹} = f \to ([⟨x, y⟩] ~_{𝑹} = [⟨z, w⟩] ~_{𝑹} \leftrightarrow f = [⟨z, w⟩] ~_{𝑹})$
4		breq2	$⊢ [⟨x, y⟩] ~_{𝑹} = f \to ([⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨x, y⟩] ~_{𝑹} \leftrightarrow [⟨z, w⟩] ~_{𝑹} <_{𝑹} f)$
5	3 4	orbi12d	$⊢ [⟨x, y⟩] ~_{𝑹} = f \to (([⟨x, y⟩] ~_{𝑹} = [⟨z, w⟩] ~_{𝑹} \lor [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨x, y⟩] ~_{𝑹}) \leftrightarrow (f = [⟨z, w⟩] ~_{𝑹} \lor [⟨z, w⟩] ~_{𝑹} <_{𝑹} f))$
6	5	notbid	$⊢ [⟨x, y⟩] ~_{𝑹} = f \to (\neg ([⟨x, y⟩] ~_{𝑹} = [⟨z, w⟩] ~_{𝑹} \lor [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨x, y⟩] ~_{𝑹}) \leftrightarrow \neg (f = [⟨z, w⟩] ~_{𝑹} \lor [⟨z, w⟩] ~_{𝑹} <_{𝑹} f))$
7	2 6	bibi12d	$⊢ [⟨x, y⟩] ~_{𝑹} = f \to (([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow \neg ([⟨x, y⟩] ~_{𝑹} = [⟨z, w⟩] ~_{𝑹} \lor [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨x, y⟩] ~_{𝑹})) \leftrightarrow (f <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow \neg (f = [⟨z, w⟩] ~_{𝑹} \lor [⟨z, w⟩] ~_{𝑹} <_{𝑹} f)))$
8		breq2	$⊢ [⟨z, w⟩] ~_{𝑹} = g \to (f <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow f <_{𝑹} g)$
9		eqeq2	$⊢ [⟨z, w⟩] ~_{𝑹} = g \to (f = [⟨z, w⟩] ~_{𝑹} \leftrightarrow f = g)$
10		breq1	$⊢ [⟨z, w⟩] ~_{𝑹} = g \to ([⟨z, w⟩] ~_{𝑹} <_{𝑹} f \leftrightarrow g <_{𝑹} f)$
11	9 10	orbi12d	$⊢ [⟨z, w⟩] ~_{𝑹} = g \to ((f = [⟨z, w⟩] ~_{𝑹} \lor [⟨z, w⟩] ~_{𝑹} <_{𝑹} f) \leftrightarrow (f = g \lor g <_{𝑹} f))$
12	11	notbid	$⊢ [⟨z, w⟩] ~_{𝑹} = g \to (\neg (f = [⟨z, w⟩] ~_{𝑹} \lor [⟨z, w⟩] ~_{𝑹} <_{𝑹} f) \leftrightarrow \neg (f = g \lor g <_{𝑹} f))$
13	8 12	bibi12d	$⊢ [⟨z, w⟩] ~_{𝑹} = g \to ((f <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow \neg (f = [⟨z, w⟩] ~_{𝑹} \lor [⟨z, w⟩] ~_{𝑹} <_{𝑹} f)) \leftrightarrow (f <_{𝑹} g \leftrightarrow \neg (f = g \lor g <_{𝑹} f)))$
14		ltsrpr	$⊢ [⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow (x +_{𝑷} w) <_{𝑷} (y +_{𝑷} z)$
15		addclpr	$⊢ (x \in 𝑷 \land w \in 𝑷) \to x +_{𝑷} w \in 𝑷$
16		addclpr	$⊢ (y \in 𝑷 \land z \in 𝑷) \to y +_{𝑷} z \in 𝑷$
17		ltsopr	$⊢ <_{𝑷} Or 𝑷$
18		sotric	$⊢ (<_{𝑷} Or 𝑷 \land (x +_{𝑷} w \in 𝑷 \land y +_{𝑷} z \in 𝑷)) \to ((x +_{𝑷} w) <_{𝑷} (y +_{𝑷} z) \leftrightarrow \neg (x +_{𝑷} w = y +_{𝑷} z \lor (y +_{𝑷} z) <_{𝑷} (x +_{𝑷} w)))$
19	17 18	mpan	$⊢ (x +_{𝑷} w \in 𝑷 \land y +_{𝑷} z \in 𝑷) \to ((x +_{𝑷} w) <_{𝑷} (y +_{𝑷} z) \leftrightarrow \neg (x +_{𝑷} w = y +_{𝑷} z \lor (y +_{𝑷} z) <_{𝑷} (x +_{𝑷} w)))$
20	15 16 19	syl2an	$⊢ ((x \in 𝑷 \land w \in 𝑷) \land (y \in 𝑷 \land z \in 𝑷)) \to ((x +_{𝑷} w) <_{𝑷} (y +_{𝑷} z) \leftrightarrow \neg (x +_{𝑷} w = y +_{𝑷} z \lor (y +_{𝑷} z) <_{𝑷} (x +_{𝑷} w)))$
21	20	an42s	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to ((x +_{𝑷} w) <_{𝑷} (y +_{𝑷} z) \leftrightarrow \neg (x +_{𝑷} w = y +_{𝑷} z \lor (y +_{𝑷} z) <_{𝑷} (x +_{𝑷} w)))$
22		enreceq	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to ([⟨x, y⟩] ~_{𝑹} = [⟨z, w⟩] ~_{𝑹} \leftrightarrow x +_{𝑷} w = y +_{𝑷} z)$
23		ltsrpr	$⊢ [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨x, y⟩] ~_{𝑹} \leftrightarrow (z +_{𝑷} y) <_{𝑷} (w +_{𝑷} x)$
24		addcompr	$⊢ z +_{𝑷} y = y +_{𝑷} z$
25		addcompr	$⊢ w +_{𝑷} x = x +_{𝑷} w$
26	24 25	breq12i	$⊢ (z +_{𝑷} y) <_{𝑷} (w +_{𝑷} x) \leftrightarrow (y +_{𝑷} z) <_{𝑷} (x +_{𝑷} w)$
27	23 26	bitri	$⊢ [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨x, y⟩] ~_{𝑹} \leftrightarrow (y +_{𝑷} z) <_{𝑷} (x +_{𝑷} w)$
28	27	a1i	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to ([⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨x, y⟩] ~_{𝑹} \leftrightarrow (y +_{𝑷} z) <_{𝑷} (x +_{𝑷} w))$
29	22 28	orbi12d	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to (([⟨x, y⟩] ~_{𝑹} = [⟨z, w⟩] ~_{𝑹} \lor [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨x, y⟩] ~_{𝑹}) \leftrightarrow (x +_{𝑷} w = y +_{𝑷} z \lor (y +_{𝑷} z) <_{𝑷} (x +_{𝑷} w)))$
30	29	notbid	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to (\neg ([⟨x, y⟩] ~_{𝑹} = [⟨z, w⟩] ~_{𝑹} \lor [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨x, y⟩] ~_{𝑹}) \leftrightarrow \neg (x +_{𝑷} w = y +_{𝑷} z \lor (y +_{𝑷} z) <_{𝑷} (x +_{𝑷} w)))$
31	21 30	bitr4d	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to ((x +_{𝑷} w) <_{𝑷} (y +_{𝑷} z) \leftrightarrow \neg ([⟨x, y⟩] ~_{𝑹} = [⟨z, w⟩] ~_{𝑹} \lor [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨x, y⟩] ~_{𝑹}))$
32	14 31	syl5bb	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷)) \to ([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow \neg ([⟨x, y⟩] ~_{𝑹} = [⟨z, w⟩] ~_{𝑹} \lor [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨x, y⟩] ~_{𝑹}))$
33	1 7 13 32	2ecoptocl	$⊢ (f \in 𝑹 \land g \in 𝑹) \to (f <_{𝑹} g \leftrightarrow \neg (f = g \lor g <_{𝑹} f))$
34	2	anbi1d	$⊢ [⟨x, y⟩] ~_{𝑹} = f \to (([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \land [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹}) \leftrightarrow (f <_{𝑹} [⟨z, w⟩] ~_{𝑹} \land [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹}))$
35		breq1	$⊢ [⟨x, y⟩] ~_{𝑹} = f \to ([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹} \leftrightarrow f <_{𝑹} [⟨v, u⟩] ~_{𝑹})$
36	34 35	imbi12d	$⊢ [⟨x, y⟩] ~_{𝑹} = f \to ((([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \land [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹}) \to [⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹}) \leftrightarrow ((f <_{𝑹} [⟨z, w⟩] ~_{𝑹} \land [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹}) \to f <_{𝑹} [⟨v, u⟩] ~_{𝑹}))$
37		breq1	$⊢ [⟨z, w⟩] ~_{𝑹} = g \to ([⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹} \leftrightarrow g <_{𝑹} [⟨v, u⟩] ~_{𝑹})$
38	8 37	anbi12d	$⊢ [⟨z, w⟩] ~_{𝑹} = g \to ((f <_{𝑹} [⟨z, w⟩] ~_{𝑹} \land [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹}) \leftrightarrow (f <_{𝑹} g \land g <_{𝑹} [⟨v, u⟩] ~_{𝑹}))$
39	38	imbi1d	$⊢ [⟨z, w⟩] ~_{𝑹} = g \to (((f <_{𝑹} [⟨z, w⟩] ~_{𝑹} \land [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹}) \to f <_{𝑹} [⟨v, u⟩] ~_{𝑹}) \leftrightarrow ((f <_{𝑹} g \land g <_{𝑹} [⟨v, u⟩] ~_{𝑹}) \to f <_{𝑹} [⟨v, u⟩] ~_{𝑹}))$
40		breq2	$⊢ [⟨v, u⟩] ~_{𝑹} = h \to (g <_{𝑹} [⟨v, u⟩] ~_{𝑹} \leftrightarrow g <_{𝑹} h)$
41	40	anbi2d	$⊢ [⟨v, u⟩] ~_{𝑹} = h \to ((f <_{𝑹} g \land g <_{𝑹} [⟨v, u⟩] ~_{𝑹}) \leftrightarrow (f <_{𝑹} g \land g <_{𝑹} h))$
42		breq2	$⊢ [⟨v, u⟩] ~_{𝑹} = h \to (f <_{𝑹} [⟨v, u⟩] ~_{𝑹} \leftrightarrow f <_{𝑹} h)$
43	41 42	imbi12d	$⊢ [⟨v, u⟩] ~_{𝑹} = h \to (((f <_{𝑹} g \land g <_{𝑹} [⟨v, u⟩] ~_{𝑹}) \to f <_{𝑹} [⟨v, u⟩] ~_{𝑹}) \leftrightarrow ((f <_{𝑹} g \land g <_{𝑹} h) \to f <_{𝑹} h))$
44		ovex	$⊢ x +_{𝑷} w \in V$
45		ovex	$⊢ y +_{𝑷} z \in V$
46		ltapr	$⊢ h \in 𝑷 \to (f <_{𝑷} g \leftrightarrow (h +_{𝑷} f) <_{𝑷} (h +_{𝑷} g))$
47		vex	$⊢ u \in V$
48		addcompr	$⊢ f +_{𝑷} g = g +_{𝑷} f$
49	44 45 46 47 48	caovord2	$⊢ u \in 𝑷 \to ((x +_{𝑷} w) <_{𝑷} (y +_{𝑷} z) \leftrightarrow ((x +_{𝑷} w) +_{𝑷} u) <_{𝑷} ((y +_{𝑷} z) +_{𝑷} u))$
50		addasspr	$⊢ (x +_{𝑷} w) +_{𝑷} u = x +_{𝑷} (w +_{𝑷} u)$
51		addasspr	$⊢ (y +_{𝑷} z) +_{𝑷} u = y +_{𝑷} (z +_{𝑷} u)$
52	50 51	breq12i	$⊢ ((x +_{𝑷} w) +_{𝑷} u) <_{𝑷} ((y +_{𝑷} z) +_{𝑷} u) \leftrightarrow (x +_{𝑷} (w +_{𝑷} u)) <_{𝑷} (y +_{𝑷} (z +_{𝑷} u))$
53	49 52	syl6bb	$⊢ u \in 𝑷 \to ((x +_{𝑷} w) <_{𝑷} (y +_{𝑷} z) \leftrightarrow (x +_{𝑷} (w +_{𝑷} u)) <_{𝑷} (y +_{𝑷} (z +_{𝑷} u)))$
54	14 53	syl5bb	$⊢ u \in 𝑷 \to ([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \leftrightarrow (x +_{𝑷} (w +_{𝑷} u)) <_{𝑷} (y +_{𝑷} (z +_{𝑷} u)))$
55		ltsrpr	$⊢ [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹} \leftrightarrow (z +_{𝑷} u) <_{𝑷} (w +_{𝑷} v)$
56		ltapr	$⊢ y \in 𝑷 \to ((z +_{𝑷} u) <_{𝑷} (w +_{𝑷} v) \leftrightarrow (y +_{𝑷} (z +_{𝑷} u)) <_{𝑷} (y +_{𝑷} (w +_{𝑷} v)))$
57	55 56	syl5bb	$⊢ y \in 𝑷 \to ([⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹} \leftrightarrow (y +_{𝑷} (z +_{𝑷} u)) <_{𝑷} (y +_{𝑷} (w +_{𝑷} v)))$
58	54 57	bi2anan9r	$⊢ (y \in 𝑷 \land u \in 𝑷) \to (([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \land [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹}) \leftrightarrow ((x +_{𝑷} (w +_{𝑷} u)) <_{𝑷} (y +_{𝑷} (z +_{𝑷} u)) \land (y +_{𝑷} (z +_{𝑷} u)) <_{𝑷} (y +_{𝑷} (w +_{𝑷} v))))$
59		ltrelpr	$⊢ <_{𝑷} \subseteq 𝑷 \times 𝑷$
60	17 59	sotri	$⊢ ((x +_{𝑷} (w +_{𝑷} u)) <_{𝑷} (y +_{𝑷} (z +_{𝑷} u)) \land (y +_{𝑷} (z +_{𝑷} u)) <_{𝑷} (y +_{𝑷} (w +_{𝑷} v))) \to (x +_{𝑷} (w +_{𝑷} u)) <_{𝑷} (y +_{𝑷} (w +_{𝑷} v))$
61		dmplp	$⊢ dom +_{𝑷} = 𝑷 \times 𝑷$
62		0npr	$⊢ \neg \emptyset \in 𝑷$
63		ltapr	$⊢ w \in 𝑷 \to ((x +_{𝑷} u) <_{𝑷} (y +_{𝑷} v) \leftrightarrow (w +_{𝑷} (x +_{𝑷} u)) <_{𝑷} (w +_{𝑷} (y +_{𝑷} v)))$
64	61 59 62 63	ndmovordi	$⊢ (w +_{𝑷} (x +_{𝑷} u)) <_{𝑷} (w +_{𝑷} (y +_{𝑷} v)) \to (x +_{𝑷} u) <_{𝑷} (y +_{𝑷} v)$
65		vex	$⊢ x \in V$
66		vex	$⊢ w \in V$
67		addasspr	$⊢ (f +_{𝑷} g) +_{𝑷} h = f +_{𝑷} (g +_{𝑷} h)$
68	65 66 47 48 67	caov12	$⊢ x +_{𝑷} (w +_{𝑷} u) = w +_{𝑷} (x +_{𝑷} u)$
69		vex	$⊢ y \in V$
70		vex	$⊢ v \in V$
71	69 66 70 48 67	caov12	$⊢ y +_{𝑷} (w +_{𝑷} v) = w +_{𝑷} (y +_{𝑷} v)$
72	68 71	breq12i	$⊢ (x +_{𝑷} (w +_{𝑷} u)) <_{𝑷} (y +_{𝑷} (w +_{𝑷} v)) \leftrightarrow (w +_{𝑷} (x +_{𝑷} u)) <_{𝑷} (w +_{𝑷} (y +_{𝑷} v))$
73		ltsrpr	$⊢ [⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹} \leftrightarrow (x +_{𝑷} u) <_{𝑷} (y +_{𝑷} v)$
74	64 72 73	3imtr4i	$⊢ (x +_{𝑷} (w +_{𝑷} u)) <_{𝑷} (y +_{𝑷} (w +_{𝑷} v)) \to [⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹}$
75	60 74	syl	$⊢ ((x +_{𝑷} (w +_{𝑷} u)) <_{𝑷} (y +_{𝑷} (z +_{𝑷} u)) \land (y +_{𝑷} (z +_{𝑷} u)) <_{𝑷} (y +_{𝑷} (w +_{𝑷} v))) \to [⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹}$
76	58 75	syl6bi	$⊢ (y \in 𝑷 \land u \in 𝑷) \to (([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \land [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹}) \to [⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹})$
77	76	ad2ant2l	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (v \in 𝑷 \land u \in 𝑷)) \to (([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \land [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹}) \to [⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹})$
78	77	3adant2	$⊢ ((x \in 𝑷 \land y \in 𝑷) \land (z \in 𝑷 \land w \in 𝑷) \land (v \in 𝑷 \land u \in 𝑷)) \to (([⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨z, w⟩] ~_{𝑹} \land [⟨z, w⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹}) \to [⟨x, y⟩] ~_{𝑹} <_{𝑹} [⟨v, u⟩] ~_{𝑹})$
79	1 36 39 43 78	3ecoptocl	$⊢ (f \in 𝑹 \land g \in 𝑹 \land h \in 𝑹) \to ((f <_{𝑹} g \land g <_{𝑹} h) \to f <_{𝑹} h)$
80	33 79	isso2i	$⊢ <_{𝑹} Or 𝑹$

Metamath Proof Explorer

Theorem ltsosr

Proof