Theorem axlttrn 6863

Description: Ordering on reals is transitive. Axiom 23 of 27 for real and complex numbers, derived from ZF set theory. (This restates pre-axlttrn 6804 with ordering on the extended reals.)

Assertion

Ref	Expression
axlttrn	|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A < B /\ B < C) -> A < C))

Proof of Theorem axlttrn

Step	Hyp	Ref	Expression
1		pre-axlttrn 6804	. 2 |- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A <R B /\ B <R C) -> A <R C))
2		ltxrlt 6859	. . . 4 |- ((A e. RR /\ B e. RR) -> (A < B <-> A <R B))
3	2	3adant3 1140	. . 3 |- ((A e. RR /\ B e. RR /\ C e. RR) -> (A < B <-> A <R B))
4		ltxrlt 6859	. . . 4 |- ((B e. RR /\ C e. RR) -> (B < C <-> B <R C))
5	4	3adant1 1138	. . 3 |- ((A e. RR /\ B e. RR /\ C e. RR) -> (B < C <-> B <R C))
6	3, 5	anbi12d 763	. 2 |- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A < B /\ B < C) <-> (A <R B /\ B <R C)))
7		ltxrlt 6859	. . 3 |- ((A e. RR /\ C e. RR) -> (A < C <-> A <R C))
8	7	3adant2 1139	. 2 |- ((A e. RR /\ B e. RR /\ C e. RR) -> (A < C <-> A <R C))
9	1, 6, 8	3imtr4d 330	1 |- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A < B /\ B < C) -> A < C))

Syntax hints:   -> wi 3   <-> wb 219   /\ wa 337   /\ w3a 1102   e. wcel 1588   class class class wbr 3507  RRcr 6751   <R cltrr 6756   < clt 6845

This theorem is referenced by:  lttr 6867  ltso 6871  lelttr 6882  ltletr 6883  lttrd 6888  xrlttr 6912  lttri 6944  mulgt1 7359  recgt1i 7416  recreclt 7418  nnge1 7459  sup2 7600  lt0nnn0 7666  nn0ltp1le 7677  zltp1le 7732  recnz 7746  gtndiv 7748  ioojoin 7931  expordi 8229  expnbnd 8285  sqrlem6 8312  fsumsplit 8676  climmullem5 8780  caucvglem2 8814  caucvglem4 8816  georeclim 8900  geoisumr 8903  cvgratlem1ALT 8907  cvgratlem1 8910  ivthlem7 8947  sin01gt0 9140  cos01gt0 9141  bcthlem1 10143  bcthlem21 10163  bcthlem25 10167  projlem26 11678  projlem28 11680  cntrsetlem 15791  lvsovso 15832

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929  ax-inf2 5964

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-nel 2269  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-f1 4144  df-fo 4145  df-f1o 4146  df-fv 4147  df-opr 4983  df-oprab 4984  df-1st 5126  df-2nd 5127  df-rdg 5304  df-1o 5344  df-oadd 5346  df-omul 5347  df-er 5479  df-ec 5481  df-qs 5484  df-en 5588  df-dom 5589  df-sdom 5590  df-ni 6518  df-pli 6519  df-mi 6520  df-lti 6521  df-plpq 6553  df-mpq 6554  df-enq 6555  df-nq 6556  df-plq 6557  df-mq 6558  df-rq 6559  df-ltq 6560  df-1q 6561  df-np 6604  df-1p 6605  df-plp 6606  df-ltp 6608  df-enr 6684  df-nr 6685  df-ltr 6688  df-0r 6689  df-c 6758  df-r 6762  df-lt 6765  df-pnf 6846  df-mnf 6847  df-xr 6848  df-ltxr 6849

Copyright terms: Public domain