Theorem itlso 2151

Description: A irreflexive, transitive, linear relation is a strict ordering.

Hypotheses

Ref	Expression
itlso.1	|- (x e. A -> -. xRx)
itlso.2	|- ((x e. A /\ y e. A /\ z e. A) -> ((xRy /\ yRz) -> xRz))
itlso.3	|- ((x e. A /\ y e. A) -> (xRy \/ x = y \/ yRx))

Assertion

Ref	Expression
itlso	|- R Or A

Distinct variable group(s):   x,y,z,R   x,A,y,z

Proof of Theorem itlso

Step	Hyp	Ref	Expression
1		itlso.1	. . . . . . . 8 |- (x e. A -> -. xRx)
2	1	adantr 306	. . . . . . 7 |- ((x e. A /\ y e. A) -> -. xRx)
3	2	3adant3 599	. . . . . 6 |- ((x e. A /\ y e. A /\ z e. A) -> -. xRx)
4		itlso.2	. . . . . 6 |- ((x e. A /\ y e. A /\ z e. A) -> ((xRy /\ yRz) -> xRz))
5	3, 4	jca 236	. . . . 5 |- ((x e. A /\ y e. A /\ z e. A) -> (-. xRx /\ ((xRy /\ yRz) -> xRz)))
6	5	rgen3 1265	. . . 4 |- A.x e. A A.y e. A A.z e. A (-. xRx /\ ((xRy /\ yRz) -> xRz))
7		df-po 2128	. . . 4 |- (R Po A <-> A.x e. A A.y e. A A.z e. A (-. xRx /\ ((xRy /\ yRz) -> xRz)))
8	6, 7	mpbir 165	. . 3 |- R Po A
9		itlso.3	. . . 4 |- ((x e. A /\ y e. A) -> (xRy \/ x = y \/ yRx))
10	9	rgen2 1248	. . 3 |- A.x e. A A.y e. A (xRy \/ x = y \/ yRx)
11	8, 10	pm3.2i 234	. 2 |- (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx))
12		df-so 2138	. 2 |- (R Or A <-> (R Po A /\ A.x e. A A.y e. A (xRy \/ x = y \/ yRx)))
13	11, 12	mpbir 165	1 |- R Or A

Syntax hints:  -. wn 1   -> wi 2   /\ wa 196   \/ w3o 580   /\ w3a 581   = weq 797   e. wcel 1092  A.wral 1201   class class class wbr 2054   Po wpo 2058   Or wor 2059

This theorem is referenced by:  so 2152  ltsopr 3930

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-3an 583  df-ex 679  df-sb 853  df-cleq 1097  df-clel 1099  df-ral 1205  df-po 2128  df-so 2138

metamath.org