Metamath Proof Explorer

Theorem el1fzopredsuc

Description: An element of an open integer interval starting at 1 joined by 0 and a successor at the beginning and the end is either 0 or an element of the open integer interval or the successor. (Contributed by AV, 14-Jul-2020)

Ref Expression
Assertion el1fzopredsuc 
|- ( N e. NN0 -> ( I e. ( 0 ... N ) <-> ( I = 0 \/ I e. ( 1 ..^ N ) \/ I = N ) ) )

Proof

Step Hyp Ref Expression
1 elfzelz 
 |-  ( I e. ( 0 ... N ) -> I e. ZZ )
2 1fzopredsuc 
 |-  ( N e. NN0 -> ( 0 ... N ) = ( ( { 0 } u. ( 1 ..^ N ) ) u. { N } ) )
3 2 eleq2d 
 |-  ( N e. NN0 -> ( I e. ( 0 ... N ) <-> I e. ( ( { 0 } u. ( 1 ..^ N ) ) u. { N } ) ) )
4 elun 
 |-  ( I e. ( ( { 0 } u. ( 1 ..^ N ) ) u. { N } ) <-> ( I e. ( { 0 } u. ( 1 ..^ N ) ) \/ I e. { N } ) )
5 elun 
 |-  ( I e. ( { 0 } u. ( 1 ..^ N ) ) <-> ( I e. { 0 } \/ I e. ( 1 ..^ N ) ) )
6 5 orbi1i 
 |-  ( ( I e. ( { 0 } u. ( 1 ..^ N ) ) \/ I e. { N } ) <-> ( ( I e. { 0 } \/ I e. ( 1 ..^ N ) ) \/ I e. { N } ) )
7 4 6 bitri 
 |-  ( I e. ( ( { 0 } u. ( 1 ..^ N ) ) u. { N } ) <-> ( ( I e. { 0 } \/ I e. ( 1 ..^ N ) ) \/ I e. { N } ) )
8 elsng 
 |-  ( I e. ZZ -> ( I e. { 0 } <-> I = 0 ) )
9 8 adantl 
 |-  ( ( N e. NN0 /\ I e. ZZ ) -> ( I e. { 0 } <-> I = 0 ) )
10 9 orbi1d 
 |-  ( ( N e. NN0 /\ I e. ZZ ) -> ( ( I e. { 0 } \/ I e. ( 1 ..^ N ) ) <-> ( I = 0 \/ I e. ( 1 ..^ N ) ) ) )
11 elsng 
 |-  ( I e. ZZ -> ( I e. { N } <-> I = N ) )
12 11 adantl 
 |-  ( ( N e. NN0 /\ I e. ZZ ) -> ( I e. { N } <-> I = N ) )
13 10 12 orbi12d 
 |-  ( ( N e. NN0 /\ I e. ZZ ) -> ( ( ( I e. { 0 } \/ I e. ( 1 ..^ N ) ) \/ I e. { N } ) <-> ( ( I = 0 \/ I e. ( 1 ..^ N ) ) \/ I = N ) ) )
14 7 13 bitrid 
 |-  ( ( N e. NN0 /\ I e. ZZ ) -> ( I e. ( ( { 0 } u. ( 1 ..^ N ) ) u. { N } ) <-> ( ( I = 0 \/ I e. ( 1 ..^ N ) ) \/ I = N ) ) )
15 df-3or 
 |-  ( ( I = 0 \/ I e. ( 1 ..^ N ) \/ I = N ) <-> ( ( I = 0 \/ I e. ( 1 ..^ N ) ) \/ I = N ) )
16 15 biimpri 
 |-  ( ( ( I = 0 \/ I e. ( 1 ..^ N ) ) \/ I = N ) -> ( I = 0 \/ I e. ( 1 ..^ N ) \/ I = N ) )
17 14 16 biimtrdi 
 |-  ( ( N e. NN0 /\ I e. ZZ ) -> ( I e. ( ( { 0 } u. ( 1 ..^ N ) ) u. { N } ) -> ( I = 0 \/ I e. ( 1 ..^ N ) \/ I = N ) ) )
18 17 ex 
 |-  ( N e. NN0 -> ( I e. ZZ -> ( I e. ( ( { 0 } u. ( 1 ..^ N ) ) u. { N } ) -> ( I = 0 \/ I e. ( 1 ..^ N ) \/ I = N ) ) ) )
19 18 com23 
 |-  ( N e. NN0 -> ( I e. ( ( { 0 } u. ( 1 ..^ N ) ) u. { N } ) -> ( I e. ZZ -> ( I = 0 \/ I e. ( 1 ..^ N ) \/ I = N ) ) ) )
20 3 19 sylbid 
 |-  ( N e. NN0 -> ( I e. ( 0 ... N ) -> ( I e. ZZ -> ( I = 0 \/ I e. ( 1 ..^ N ) \/ I = N ) ) ) )
21 1 20 mpdi 
 |-  ( N e. NN0 -> ( I e. ( 0 ... N ) -> ( I = 0 \/ I e. ( 1 ..^ N ) \/ I = N ) ) )
22 c0ex 
 |-  0 e. _V
23 22 snid 
 |-  0 e. { 0 }
24 23 a1i 
 |-  ( I = 0 -> 0 e. { 0 } )
25 eleq1 
 |-  ( I = 0 -> ( I e. { 0 } <-> 0 e. { 0 } ) )
26 24 25 mpbird 
 |-  ( I = 0 -> I e. { 0 } )
27 26 a1i 
 |-  ( N e. NN0 -> ( I = 0 -> I e. { 0 } ) )
28 idd 
 |-  ( N e. NN0 -> ( I e. ( 1 ..^ N ) -> I e. ( 1 ..^ N ) ) )
29 snidg 
 |-  ( N e. NN0 -> N e. { N } )
30 eleq1 
 |-  ( I = N -> ( I e. { N } <-> N e. { N } ) )
31 29 30 syl5ibrcom 
 |-  ( N e. NN0 -> ( I = N -> I e. { N } ) )
32 27 28 31 3orim123d 
 |-  ( N e. NN0 -> ( ( I = 0 \/ I e. ( 1 ..^ N ) \/ I = N ) -> ( I e. { 0 } \/ I e. ( 1 ..^ N ) \/ I e. { N } ) ) )
33 32 imp 
 |-  ( ( N e. NN0 /\ ( I = 0 \/ I e. ( 1 ..^ N ) \/ I = N ) ) -> ( I e. { 0 } \/ I e. ( 1 ..^ N ) \/ I e. { N } ) )
34 df-3or 
 |-  ( ( I e. { 0 } \/ I e. ( 1 ..^ N ) \/ I e. { N } ) <-> ( ( I e. { 0 } \/ I e. ( 1 ..^ N ) ) \/ I e. { N } ) )
35 33 34 sylib 
 |-  ( ( N e. NN0 /\ ( I = 0 \/ I e. ( 1 ..^ N ) \/ I = N ) ) -> ( ( I e. { 0 } \/ I e. ( 1 ..^ N ) ) \/ I e. { N } ) )
36 35 7 sylibr 
 |-  ( ( N e. NN0 /\ ( I = 0 \/ I e. ( 1 ..^ N ) \/ I = N ) ) -> I e. ( ( { 0 } u. ( 1 ..^ N ) ) u. { N } ) )
37 3 adantr 
 |-  ( ( N e. NN0 /\ ( I = 0 \/ I e. ( 1 ..^ N ) \/ I = N ) ) -> ( I e. ( 0 ... N ) <-> I e. ( ( { 0 } u. ( 1 ..^ N ) ) u. { N } ) ) )
38 36 37 mpbird 
 |-  ( ( N e. NN0 /\ ( I = 0 \/ I e. ( 1 ..^ N ) \/ I = N ) ) -> I e. ( 0 ... N ) )
39 38 ex 
 |-  ( N e. NN0 -> ( ( I = 0 \/ I e. ( 1 ..^ N ) \/ I = N ) -> I e. ( 0 ... N ) ) )
40 21 39 impbid 
 |-  ( N e. NN0 -> ( I e. ( 0 ... N ) <-> ( I = 0 \/ I e. ( 1 ..^ N ) \/ I = N ) ) )