Step |
Hyp |
Ref |
Expression |
1 |
|
uzid |
|- ( M e. ZZ -> M e. ( ZZ>= ` M ) ) |
2 |
|
elfzp1 |
|- ( M e. ( ZZ>= ` M ) -> ( m e. ( M ... ( M + 1 ) ) <-> ( m e. ( M ... M ) \/ m = ( M + 1 ) ) ) ) |
3 |
1 2
|
syl |
|- ( M e. ZZ -> ( m e. ( M ... ( M + 1 ) ) <-> ( m e. ( M ... M ) \/ m = ( M + 1 ) ) ) ) |
4 |
|
fzsn |
|- ( M e. ZZ -> ( M ... M ) = { M } ) |
5 |
4
|
eleq2d |
|- ( M e. ZZ -> ( m e. ( M ... M ) <-> m e. { M } ) ) |
6 |
|
velsn |
|- ( m e. { M } <-> m = M ) |
7 |
5 6
|
bitrdi |
|- ( M e. ZZ -> ( m e. ( M ... M ) <-> m = M ) ) |
8 |
7
|
orbi1d |
|- ( M e. ZZ -> ( ( m e. ( M ... M ) \/ m = ( M + 1 ) ) <-> ( m = M \/ m = ( M + 1 ) ) ) ) |
9 |
3 8
|
bitrd |
|- ( M e. ZZ -> ( m e. ( M ... ( M + 1 ) ) <-> ( m = M \/ m = ( M + 1 ) ) ) ) |
10 |
|
vex |
|- m e. _V |
11 |
10
|
elpr |
|- ( m e. { M , ( M + 1 ) } <-> ( m = M \/ m = ( M + 1 ) ) ) |
12 |
9 11
|
bitr4di |
|- ( M e. ZZ -> ( m e. ( M ... ( M + 1 ) ) <-> m e. { M , ( M + 1 ) } ) ) |
13 |
12
|
eqrdv |
|- ( M e. ZZ -> ( M ... ( M + 1 ) ) = { M , ( M + 1 ) } ) |