Theorem ltsosr 3997

Description: Signed real 'less than' is a strict ordering.

Assertion

Ref	Expression
ltsosr	|- <R Or R.

Proof of Theorem ltsosr

Step	Hyp	Ref	Expression
1		df-nr 3961	. . 3 |- R. = ((P. X. P.)/. ~R )
2		breq1 2065	. . . . 5 |- ([<.x, y>.] ~R = f -> ([<.x, y>.] ~R <R [<.z, w>.] ~R <-> f <R [<.z, w>.] ~R ))
3		cleq1 1107	. . . . . . 7 |- ([<.x, y>.] ~R = f -> ([<.x, y>.] ~R = [<.z, w>.] ~R <-> f = [<.z, w>.] ~R ))
4		breq2 2066	. . . . . . 7 |- ([<.x, y>.] ~R = f -> ([<.z, w>.] ~R <R [<.x, y>.] ~R <-> [<.z, w>.] ~R <R f))
5	3, 4	orbi12d 475	. . . . . 6 |- ([<.x, y>.] ~R = f -> (([<.x, y>.] ~R = [<.z, w>.] ~R \/ [<.z, w>.] ~R <R [<.x, y>.] ~R ) <-> (f = [<.z, w>.] ~R \/ [<.z, w>.] ~R <R f)))
6	5	negbid 463	. . . . 5 |- ([<.x, y>.] ~R = f -> (-. ([<.x, y>.] ~R = [<.z, w>.] ~R \/ [<.z, w>.] ~R <R [<.x, y>.] ~R ) <-> -. (f = [<.z, w>.] ~R \/ [<.z, w>.] ~R <R f)))
7	2, 6	bibi12d 477	. . . 4 |- ([<.x, y>.] ~R = f -> (([<.x, y>.] ~R <R [<.z, w>.] ~R <-> -. ([<.x, y>.] ~R = [<.z, w>.] ~R \/ [<.z, w>.] ~R <R [<.x, y>.] ~R )) <-> (f <R [<.z, w>.] ~R <-> -. (f = [<.z, w>.] ~R \/ [<.z, w>.] ~R <R f))))
8	2	anbi1d 469	. . . . 5 |- ([<.x, y>.] ~R = f -> (([<.x, y>.] ~R <R [<.z, w>.] ~R /\ [<.z, w>.] ~R <R [<.v, u>.] ~R ) <-> (f <R [<.z, w>.] ~R /\ [<.z, w>.] ~R <R [<.v, u>.] ~R )))
9		breq1 2065	. . . . 5 |- ([<.x, y>.] ~R = f -> ([<.x, y>.] ~R <R [<.v, u>.] ~R <-> f <R [<.v, u>.] ~R ))
10	8, 9	imbi12d 474	. . . 4 |- ([<.x, y>.] ~R = f -> ((([<.x, y>.] ~R <R [<.z, w>.] ~R /\ [<.z, w>.] ~R <R [<.v, u>.] ~R ) -> [<.x, y>.] ~R <R [<.v, u>.] ~R ) <-> ((f <R [<.z, w>.] ~R /\ [<.z, w>.] ~R <R [<.v, u>.] ~R ) -> f <R [<.v, u>.] ~R )))
11	7, 10	anbi12d 476	. . 3 |- ([<.x, y>.] ~R = f -> ((([<.x, y>.] ~R <R [<.z, w>.] ~R <-> -. ([<.x, y>.] ~R = [<.z, w>.] ~R \/ [<.z, w>.] ~R <R [<.x, y>.] ~R )) /\ (([<.x, y>.] ~R <R [<.z, w>.] ~R /\ [<.z, w>.] ~R <R [<.v, u>.] ~R ) -> [<.x, y>.] ~R <R [<.v, u>.] ~R )) <-> ((f <R [<.z, w>.] ~R <-> -. (f = [<.z, w>.] ~R \/ [<.z, w>.] ~R <R f)) /\ ((f <R [<.z, w>.] ~R /\ [<.z, w>.] ~R <R [<.v, u>.] ~R ) -> f <R [<.v, u>.] ~R ))))
12		breq2 2066	. . . . 5 |- ([<.z, w>.] ~R = g -> (f <R [<.z, w>.] ~R <-> f <R g))
13		cleq2 1110	. . . . . . 7 |- ([<.z, w>.] ~R = g -> (f = [<.z, w>.] ~R <-> f = g))
14		breq1 2065	. . . . . . 7 |- ([<.z, w>.] ~R = g -> ([<.z, w>.] ~R <R f <-> g <R f))
15	13, 14	orbi12d 475	. . . . . 6 |- ([<.z, w>.] ~R = g -> ((f = [<.z, w>.] ~R \/ [<.z, w>.] ~R <R f) <-> (f = g \/ g <R f)))
16	15	negbid 463	. . . . 5 |- ([<.z, w>.] ~R = g -> (-. (f = [<.z, w>.] ~R \/ [<.z, w>.] ~R <R f) <-> -. (f = g \/ g <R f)))
17	12, 16	bibi12d 477	. . . 4 |- ([<.z, w>.] ~R = g -> ((f <R [<.z, w>.] ~R <-> -. (f = [<.z, w>.] ~R \/ [<.z, w>.] ~R <R f)) <-> (f <R g <-> -. (f = g \/ g <R f))))
18		breq1 2065	. . . . . 6 |- ([<.z, w>.] ~R = g -> ([<.z, w>.] ~R <R [<.v, u>.] ~R <-> g <R [<.v, u>.] ~R ))
19	12, 18	anbi12d 476	. . . . 5 |- ([<.z, w>.] ~R = g -> ((f <R [<.z, w>.] ~R /\ [<.z, w>.] ~R <R [<.v, u>.] ~R ) <-> (f <R g /\ g <R [<.v, u>.] ~R )))
20	19	imbi1d 465	. . . 4 |- ([<.z, w>.] ~R = g -> (((f <R [<.z, w>.] ~R /\ [<.z, w>.] ~R <R [<.v, u>.] ~R ) -> f <R [<.v, u>.] ~R ) <-> ((f <R g /\ g <R [<.v, u>.] ~R ) -> f <R [<.v, u>.] ~R )))
21	17, 20	anbi12d 476	. . 3 |- ([<.z, w>.] ~R = g -> (((f <R [<.z, w>.] ~R <-> -. (f = [<.z, w>.] ~R \/ [<.z, w>.] ~R <R f)) /\ ((f <R [<.z, w>.] ~R /\ [<.z, w>.] ~R <R [<.v, u>.] ~R ) -> f <R [<.v, u>.] ~R )) <-> ((f <R g <-> -. (f = g \/ g <R f)) /\ ((f <R g /\ g <R [<.v, u>.] ~R ) -> f <R [<.v, u>.] ~R ))))
22		breq2 2066	. . . . . 6 |- ([<.v, u>.] ~R = h -> (g <R [<.v, u>.] ~R <-> g <R h))
23	22	anbi2d 468	. . . . 5 |- ([<.v, u>.] ~R = h -> ((f <R g /\ g <R [<.v, u>.] ~R ) <-> (f <R g /\ g <R h)))
24		breq2 2066	. . . . 5 |- ([<.v, u>.] ~R = h -> (f <R [<.v, u>.] ~R <-> f <R h))
25	23, 24	imbi12d 474	. . . 4 |- ([<.v, u>.] ~R = h -> (((f <R g /\ g <R [<.v, u>.] ~R ) -> f <R [<.v, u>.] ~R ) <-> ((f <R g /\ g <R h) -> f <R h)))
26	25	anbi2d 468	. . 3 |- ([<.v, u>.] ~R = h -> (((f <R g <-> -. (f = g \/ g <R f)) /\ ((f <R g /\ g <R [<.v, u>.] ~R ) -> f <R [<.v, u>.] ~R )) <-> ((f <R g <-> -. (f = g \/ g <R f)) /\ ((f <R g /\ g <R h) -> f <R h))))
27		ltsopr 3930	. . . . . . . . . 10 |- <P Or P.
28		sotric 2148	. . . . . . . . . 10 |- (( <P Or P. /\ ((x +P. w) e. P. /\ (y +P. z) e. P.)) -> ((x +P. w) <P (y +P. z) <-> -. ((x +P. w) = (y +P. z) \/ (y +P. z) <P (x +P. w))))
29	27, 28	mpan 518	. . . . . . . . 9 |- (((x +P. w) e. P. /\ (y +P. z) e. P.) -> ((x +P. w) <P (y +P. z) <-> -. ((x +P. w) = (y +P. z) \/ (y +P. z) <P (x +P. w))))
30		addclpr 3914	. . . . . . . . 9 |- ((x e. P. /\ w e. P.) -> (x +P. w) e. P.)
31		addclpr 3914	. . . . . . . . 9 |- ((y e. P. /\ z e. P.) -> (y +P. z) e. P.)
32	29, 30, 31	syl2an 349	. . . . . . . 8 |- (((x e. P. /\ w e. P.) /\ (y e. P. /\ z e. P.)) -> ((x +P. w) <P (y +P. z) <-> -. ((x +P. w) = (y +P. z) \/ (y +P. z) <P (x +P. w))))
33	32	an42s 391	. . . . . . 7 |- (((x e. P. /\ y e. P.) /\ (z e. P. /\ w e. P.)) -> ((x +P. w) <P (y +P. z) <-> -. ((x +P. w) = (y +P. z) \/ (y +P. z) <P (x +P. w))))
34		enreceq 3971	. . . . . . . . 9 |- (((x e. P. /\ y e. P.) /\ (z e. P. /\ w e. P.)) -> ([<.x, y>.] ~R = [<.z, w>.] ~R <-> (x +P. w) = (y +P. z)))
35		visset 1350	. . . . . . . . . . . 12 |- z e. V
36		visset 1350	. . . . . . . . . . . 12 |-