Theorem nelioo5 15609

Description: Membership in an open interval of extended reals.

Assertion

Ref	Expression
nelioo5	|- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> (-. C e. (A(,)B) <-> (C <_ A \/ B <_ C)))

Proof of Theorem nelioo5

Step	Hyp	Ref	Expression
1		elioo5 7898	. . 3 |- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> (C e. (A(,)B) <-> (A < C /\ C < B)))
2	1	notbid 746	. 2 |- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> (-. C e. (A(,)B) <-> -. (A < C /\ C < B)))
3		ianor 420	. . 3 |- (-. (A < C /\ C < B) <-> (-. A < C \/ -. C < B))
4	3	a1i 8	. 2 |- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> (-. (A < C /\ C < B) <-> (-. A < C \/ -. C < B)))
5		xrlenlt 6860	. . . . . 6 |- ((C e. RR* /\ A e. RR*) -> (C <_ A <-> -. A < C))
6	5	ancoms 416	. . . . 5 |- ((A e. RR* /\ C e. RR*) -> (C <_ A <-> -. A < C))
7	6	bicomd 271	. . . 4 |- ((A e. RR* /\ C e. RR*) -> (-. A < C <-> C <_ A))
8	7	3adant2 1139	. . 3 |- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> (-. A < C <-> C <_ A))
9		xrlenlt 6860	. . . . 5 |- ((B e. RR* /\ C e. RR*) -> (B <_ C <-> -. C < B))
10	9	bicomd 271	. . . 4 |- ((B e. RR* /\ C e. RR*) -> (-. C < B <-> B <_ C))
11	10	3adant1 1138	. . 3 |- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> (-. C < B <-> B <_ C))
12	8, 11	orbi12d 762	. 2 |- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> ((-. A < C \/ -. C < B) <-> (C <_ A \/ B <_ C)))
13	2, 4, 12	3bitrd 735	1 |- ((A e. RR* /\ B e. RR* /\ C e. RR*) -> (-. C e. (A(,)B) <-> (C <_ A \/ B <_ C)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 219   \/ wo 336   /\ wa 337   /\ w3a 1102   e. wcel 1588   class class class wbr 3507  (class class class)co 4981   <_ cle 6841  RR*cxr 6844   < clt 6845  (,)cioo 7870

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-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-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-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-enr 6684  df-nr 6685  df-0r 6689  df-c 6758  df-r 6762  df-xr 6848  df-le 6850  df-ioo 7874

Copyright terms: Public domain