This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fzosplitsni

Description: Membership in a half-open range extended by a singleton. (Contributed by Stefan O'Rear, 23-Aug-2015)

Ref Expression
Assertion fzosplitsni 
|- ( B e. ( ZZ>= ` A ) -> ( C e. ( A ..^ ( B + 1 ) ) <-> ( C e. ( A ..^ B ) \/ C = B ) ) )

Proof

Step Hyp Ref Expression
1 fzosplitsn 
 |-  ( B e. ( ZZ>= ` A ) -> ( A ..^ ( B + 1 ) ) = ( ( A ..^ B ) u. { B } ) )
2 1 eleq2d 
 |-  ( B e. ( ZZ>= ` A ) -> ( C e. ( A ..^ ( B + 1 ) ) <-> C e. ( ( A ..^ B ) u. { B } ) ) )
3 elun 
 |-  ( C e. ( ( A ..^ B ) u. { B } ) <-> ( C e. ( A ..^ B ) \/ C e. { B } ) )
4 elsn2g 
 |-  ( B e. ( ZZ>= ` A ) -> ( C e. { B } <-> C = B ) )
5 4 orbi2d 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( C e. ( A ..^ B ) \/ C e. { B } ) <-> ( C e. ( A ..^ B ) \/ C = B ) ) )
6 3 5 bitrid 
 |-  ( B e. ( ZZ>= ` A ) -> ( C e. ( ( A ..^ B ) u. { B } ) <-> ( C e. ( A ..^ B ) \/ C = B ) ) )
7 2 6 bitrd 
 |-  ( B e. ( ZZ>= ` A ) -> ( C e. ( A ..^ ( B + 1 ) ) <-> ( C e. ( A ..^ B ) \/ C = B ) ) )