iocinico

*proof of iocinico

50::df-in          |- ( ( A (,] B ) i^i ( B [,) C ) )
	= { x | ( x e. ( A (,] B ) /\ x e. ( B [,) C ) ) }
*show x <_ B
56::elioc1         |- ( ( A e. RR* /\ B e. RR* )
	-> ( x e. ( A (,] B ) <-> ( x e. RR* /\ A < x /\ x <_ B ) ) )
57:56:3adant3 |- ( ( A e. RR* /\ B e. RR* /\ C e. RR* )
	-> ( x e. ( A (,] B ) <-> ( x e. RR* /\ A < x /\ x <_ B ) ) )
58::bi1  |- ( ( x e. ( A (,] B ) <-> ( x e. RR* /\ A < x /\ x <_ B ) )
	-> ( x e. ( A (,] B ) -> ( x e. RR* /\ A < x /\ x <_ B ) ) )
59::3simpb |- (  ( x e. RR* /\ A < x /\ x <_ B )
	-> ( x e. RR* /\ x <_ B ) )
60:58,59:syl6   |- ( ( x e. ( A (,] B ) <-> ( x e. RR* /\ A < x /\ x <_ B ) )
	-> ( x e. ( A (,] B ) -> ( x e. RR* /\ x <_ B ) ) )
61:57,60:syl  |- ( ( A e. RR* /\ B e. RR* /\ C e. RR* )
	-> ( x e. ( A (,] B ) -> ( x e. RR* /\ x <_ B ) ) )
* show B <_ x
62::elico1         |- ( ( B e. RR* /\ C e. RR* )
	-> ( x e. ( B [,) C ) <-> ( x e. RR* /\ B <_ x /\ x < C ) ) )
63:62:3adant1 |- ( ( A e. RR* /\ B e. RR* /\ C e. RR* )
	-> ( x e. ( B [,) C ) <-> ( x e. RR* /\ B <_ x /\ x < C ) ) )
64::bi1  |- ( ( x e. ( B [,) C ) <-> ( x e. RR* /\ B <_ x /\ x < C ) )
	-> ( x e. ( B [,) C ) -> ( x e. RR* /\ B <_ x /\ x < C ) ) )
65::3simpa |- (  ( x e. RR* /\ B <_ x /\ x < C )
	-> ( x e. RR* /\ B <_ x ) )
66:64,65:syl6   |- ( ( x e. ( B [,) C ) <-> ( x e. RR* /\ B <_ x /\ x < C ) )
	-> ( x e. ( B [,) C ) ->  ( x e. RR* /\ B <_ x ) ) )
67:63,66:syl  |- ( ( A e. RR* /\ B e. RR* /\ C e. RR* )
	-> ( x e. ( B [,) C ) ->  ( x e. RR* /\ B <_ x ) ) )
*combine these results
68:61,67:anim12d  |- ( ( A e. RR* /\ B e. RR* /\ C e. RR* )
	-> ( ( x e. ( A (,] B ) /\ x e. ( B [,) C ) )
	-> ( ( x e. RR* /\ x <_ B ) /\ ( x e. RR* /\ B <_ x ) ) ) )
69::simpll         |- ( ( ( x e. RR* /\ x <_ B ) /\ ( x e. RR* /\ B <_ x ) ) -> x e. RR* )
70::simprr         |- ( ( ( x e. RR* /\ x <_ B ) /\ ( x e. RR* /\ B <_ x ) ) -> B <_ x )
71::simplr         |- ( ( ( x e. RR* /\ x <_ B ) /\ ( x e. RR* /\ B <_ x ) ) -> x <_ B )
72:69,70,71:3jca  |- ( ( ( x e. RR* /\ x <_ B ) /\ ( x e. RR* /\ B <_ x ) )
	->  ( x e. RR* /\ B <_ x /\ x <_ B ) )
73:68,72:syl6    |- ( ( A e. RR* /\ B e. RR* /\ C e. RR* )
	-> ( ( x e. ( A (,] B ) /\ x e. ( B [,) C ) )
	->  ( x e. RR* /\ B <_ x /\ x <_ B ) ) )

*show one way subset
74::elicc1          |- ( ( B e. RR* /\ B e. RR* )
	-> ( x e. ( B [,] B ) <-> ( x e. RR* /\ B <_ x /\ x <_ B ) ) )
75:74:anidms   |- ( B e. RR*
	-> ( x e. ( B [,] B ) <-> ( x e. RR* /\ B <_ x /\ x <_ B ) ) )
76:75:3ad2ant2   |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* )
	-> ( x e. ( B [,] B ) <-> ( x e. RR* /\ B <_ x /\ x <_ B ) ) )
*
77:73,76:sylibrd    |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* )
	-> ( ( x e. ( A (,] B ) /\ x e. ( B [,) C ) )
	->   x e. ( B [,] B ) ) )
78::id  |- ( ( ( x e. ( A (,] B ) /\ x e. ( B [,) C ) )
	-> x e. ( B [,] B ) )
	-> ( ( x e. ( A (,] B ) /\ x e. ( B [,) C ) ) -> x e. ( B [,] B ) ) )
79:78:ss2abdv |- ( ( ( x e. ( A (,] B ) /\ x e. ( B [,) C ) )
	->   x e. ( B [,] B ) )
	->  { x | ( x e. ( A (,] B ) /\ x e. ( B [,) C ) ) }
	C_   { x | x e. ( B [,] B ) }  )
80:77,79:syl   |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* )
	->  { x | ( x e. ( A (,] B ) /\ x e. ( B [,) C ) ) }
	C_   { x | x e. ( B [,] B ) }  )
81:50,80:syl5eqss   |-  ( ( A e. RR* /\ B e. RR* /\ C e. RR* )
	-> ( ( A (,] B ) i^i ( B [,) C ) ) C_ { x | x e. ( B [,] B ) }  )
82::abid2  |- { x | x e. ( B [,] B ) }  = ( B [,] B )
83:81,82:syl6sseq    |- ( ( A e. RR* /\ B e. RR* /\ C e. RR* )
	-> ( ( A (,] B ) i^i ( B [,) C ) ) C_ ( B [,] B )  )
84:83:adantr   |-  (  (  ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) )
	->  ( ( A (,] B ) i^i ( B [,) C ) ) C_ ( B [,] B )  )
85::iccid          |- ( B e. RR* -> ( B [,] B ) = { B } )
86:85:3ad2ant2   |-  (   ( A e. RR* /\ B e. RR* /\ C e. RR* )
	->  ( B [,] B ) = { B } )
87:86:adantr   |-  (  (  ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) )
	->  ( B [,] B ) = { B } )
88:84,87:sseqtrd    |-  (  (  ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) )
	->  ( ( A (,] B ) i^i ( B [,) C ) ) C_ { B }  )
*
*show B is in ( A (,] B)
89::simpl2         |- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> B e. RR* )
90::simprl         |- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> A < B )
91::xrleid  |- ( B e. RR* -> B <_ B )
92:89,91:syl       |- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> B <_ B )
93:89,90,92:3jca  |- (  (  ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) )
	-> ( B e. RR* /\ A < B /\ B <_ B ) )
94::elioc1         |- ( ( A e. RR* /\ B e. RR* )
	-> ( B e. ( A (,] B ) <-> ( B e. RR* /\ A < B /\ B <_ B ) ) )
95:94:3adant3   |- ( ( A e. RR* /\ B e. RR* /\ C e. RR* )
	-> ( B e. ( A (,] B ) <-> ( B e. RR* /\ A < B /\ B <_ B ) ) )
96:95:adantr   |- (  (  ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) )
	-> ( B e. ( A (,] B ) <-> ( B e. RR* /\ A < B /\ B <_ B ) ) )
97:93,96:mpbird    |- (  (  ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) )
	-> B e. ( A (,] B ) )
*show B is in ( B [,) C )
d1::simprr         |- ( ( ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) ) -> B < C )
200:89,92,d1:3jca |- (  (  ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) )
	-> ( B e. RR* /\ B <_ B /\ B < C ) )
210::elico1        |- ( ( B e. RR* /\ C e. RR* )
	-> ( B e. ( B [,) C ) <-> ( B e. RR* /\ B <_ B /\ B < C ) ) )
220:210:3adant1 |- ( ( A e. RR* /\ B e. RR* /\ C e. RR* )
	-> ( B e. ( B [,) C ) <-> ( B e. RR* /\ B <_ B /\ B < C ) ) )
230:220:adantr |- (  (  ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) )
	-> ( B e. ( B [,) C ) <-> ( B e. RR* /\ B <_ B /\ B < C ) ) )
240:200,230:mpbird |- (  (  ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) )
	->  B e. ( B [,) C ) )
*combine results
250:97,240:jca |- (  (  ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) )
	-> ( B e. ( A (,] B ) /\ B e. ( B [,) C ) ) )
260:97,240:bnj1153 |- (  (  ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) )
	-> B e. ( ( A (,] B ) i^i ( B [,) C ) ) )
270:260:snssd |- (  (  ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) )
	-> { B } C_  ( ( A (,] B ) i^i ( B [,) C ) ) )
*
qed:88,270:eqssd |- (  (  ( A e. RR* /\ B e. RR* /\ C e. RR* ) /\ ( A < B /\ B < C ) )
	-> ( ( A (,] B ) i^i ( B [,) C ) ) = { B } )

$d A x
$d B x
$d C x
$=    ( vx cxr wcel w3a clt wbr wa co wss cab wi cle wb syl6 syl 3jca
      adantr cioc cico cin cicc cv df-in elioc1 3adant3 3simpb elico1
      csn 3adant1 3simpa anim12d simpll simprr simplr elicc1 3ad2ant2
      bi1 anidms sylibrd ss2abdv syl5eqss abid2 syl6sseq wceq sseqtrd
      id iccid simpl2 simprl xrleid mpbird bnj1153 snssd eqssd ) AEFZ
      BEFZCEFZGZABHIZBCHIZJZJZABUAKZBCUBKZUCZBUKZWEWHBBUDKZWIWAWHWJLW
      DWAWHDUEZWJFZDMZWJWAWHWKWFFZWKWGFZJZDMZWMDWFWGUFWAWPWLNZWQWMLWA
      WPWKEFZBWKOIZWKBOIZGZWLWAWPWSXAJZWSWTJZJZXBWAWNXCWOXDWAWNWSAWKH
      IZXAGZPZWNXCNVRVSXHVTABWKUGUHXHWNXGXCWNXGUTWSXFXAUIQRWAWOWSWTWK
      CHIZGZPZWOXDNVSVTXKVRBCWKUJULXKWOXJXDWOXJUTWSWTXIUMQRUNXEWSWTXA
      WSXAXDUOXCWSWTUPWSXAXDUQSQVSVRWLXBPZVTVSXLBBWKURVAUSVBWRWPWLDWR
      VIVCRVDDWJVEVFTWAWJWIVGZWDVSVRXMVTBVJUSTVHWEBWHWEWFWGBWEBWFFZVS
      WBBBOIZGZWEVSWBXOVRVSVTWDVKZWAWBWCVLWEVSXOXQBVMRZSWAXNXPPZWDVRV
      SXSVTABBUGUHTVNWEBWGFZVSXOWCGZWEVSXOWCXQXRWAWBWCUPSWAXTYAPZWDVS
      VTYBVRBCBUJULTVNVOVPVQ $.
$)