Theorem ltsosr 5203

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 5167	. . 3 |- R. = ((P. X. P.)/. ~R )
2		breq1 2622	. . . . 5 |- ([<.x, y>.] ~R = f -> ([<.x, y>.] ~R <R [<.z, w>.] ~R <-> f <R [<.z, w>.] ~R ))
3		eqeq1 1481	. . . . . . 7 |- ([<.x, y>.] ~R = f -> ([<.x, y>.] ~R = [<.z, w>.] ~R <-> f = [<.z, w>.] ~R ))
4		breq2 2623	. . . . . . 7 |- ([<.x, y>.] ~R = f -> ([<.z, w>.] ~R <R [<.x, y>.] ~R <-> [<.z, w>.] ~R <R f))
5	3, 4	orbi12d 627	. . . . . 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 611	. . . . 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 629	. . . 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 617	. . . . 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 2622	. . . . 5 |- ([<.x, y>.] ~R = f -> ([<.x, y>.] ~R <R [<.v, u>.] ~R <-> f <R [<.v, u>.] ~R ))
10	8, 9	imbi12d 626	. . . 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 628	. . 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 2623	. . . . 5 |- ([<.z, w>.] ~R = g -> (f <R [<.z, w>.] ~R <-> f <R g))
13		eqeq2 1484	. . . . . . 7 |- ([<.z, w>.] ~R = g -> (f = [<.z, w>.] ~R <-> f = g))
14		breq1 2622	. . . . . . 7 |- ([<.z, w>.] ~R = g -> ([<.z, w>.] ~R <R f <-> g <R f))
15	13, 14	orbi12d 627	. . . . . 6 |- ([<.z, w>.] ~R = g -> ((f = [<.z, w>.] ~R \/ [<.z, w>.] ~R <R f) <-> (f = g \/ g <R f)))
16	15	negbid 611	. . . . 5 |- ([<.z, w>.] ~R = g -> (-. (f = [<.z, w>.] ~R \/ [<.z, w>.] ~R <R f) <-> -. (f = g \/ g <R f)))
17	12, 16	bibi12d 629	. . . 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 2622	. . . . . 6 |- ([<.z, w>.] ~R = g -> ([<.z, w>.] ~R <R [<.v, u>.] ~R <-> g <R [<.v, u>.] ~R ))
19	12, 18	anbi12d 628	. . . . 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 613	. . . 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 628	. . 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 2623	. . . . . 6 |- ([<.v, u>.] ~R = h -> (g <R [<.v, u>.] ~R <-> g <R h))
23	22	anbi2d 616	. . . . 5 |- ([<.v, u>.] ~R = h -> ((f <R g /\ g <R [<.v, u>.] ~R ) <-> (f <R g /\ g <R h)))
24		breq2 2623	. . . . 5 |- ([<.v, u>.] ~R = h -> (f <R [<.v, u>.] ~R <-> f <R h))
25	23, 24	imbi12d 626	. . . 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 616	. . 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 5136	. . . . . . . . . 10 |- <P Or P.
28		sotric 2860	. . . . . . . . . 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 695	. . . . . . . . 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 5120	. . . . . . . . 9 |- ((x e. P. /\ w e. P.) -> (x +P. w) e. P.)
31		addclpr 5120	. . . . . . . . 9 |- ((y e. P. /\ z e. P.) -> (y +P. z) e. P.)
32	29, 30, 31	syl2an 454	. . . . . . . 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 509	. . . . . . 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 5177	. . . . . . . . 9 |- (((x e. P. /\ y e. P.) /\ (z e. P. /\ w e. P.)) -> ([<.