Step |
Hyp |
Ref |
Expression |
1 |
|
uzid |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) ) |
2 |
|
elfzp1 |
⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 𝑀 ) → ( 𝑚 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) ↔ ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ∨ 𝑚 = ( 𝑀 + 1 ) ) ) ) |
3 |
1 2
|
syl |
⊢ ( 𝑀 ∈ ℤ → ( 𝑚 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) ↔ ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ∨ 𝑚 = ( 𝑀 + 1 ) ) ) ) |
4 |
|
fzsn |
⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... 𝑀 ) = { 𝑀 } ) |
5 |
4
|
eleq2d |
⊢ ( 𝑀 ∈ ℤ → ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↔ 𝑚 ∈ { 𝑀 } ) ) |
6 |
|
velsn |
⊢ ( 𝑚 ∈ { 𝑀 } ↔ 𝑚 = 𝑀 ) |
7 |
5 6
|
bitrdi |
⊢ ( 𝑀 ∈ ℤ → ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ↔ 𝑚 = 𝑀 ) ) |
8 |
7
|
orbi1d |
⊢ ( 𝑀 ∈ ℤ → ( ( 𝑚 ∈ ( 𝑀 ... 𝑀 ) ∨ 𝑚 = ( 𝑀 + 1 ) ) ↔ ( 𝑚 = 𝑀 ∨ 𝑚 = ( 𝑀 + 1 ) ) ) ) |
9 |
3 8
|
bitrd |
⊢ ( 𝑀 ∈ ℤ → ( 𝑚 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) ↔ ( 𝑚 = 𝑀 ∨ 𝑚 = ( 𝑀 + 1 ) ) ) ) |
10 |
|
vex |
⊢ 𝑚 ∈ V |
11 |
10
|
elpr |
⊢ ( 𝑚 ∈ { 𝑀 , ( 𝑀 + 1 ) } ↔ ( 𝑚 = 𝑀 ∨ 𝑚 = ( 𝑀 + 1 ) ) ) |
12 |
9 11
|
bitr4di |
⊢ ( 𝑀 ∈ ℤ → ( 𝑚 ∈ ( 𝑀 ... ( 𝑀 + 1 ) ) ↔ 𝑚 ∈ { 𝑀 , ( 𝑀 + 1 ) } ) ) |
13 |
12
|
eqrdv |
⊢ ( 𝑀 ∈ ℤ → ( 𝑀 ... ( 𝑀 + 1 ) ) = { 𝑀 , ( 𝑀 + 1 ) } ) |