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 ( 𝑁 ∈ ℕ0 → ( 𝐼 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 = 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 elfzelz ⊢ ( 𝐼 ∈ ( 0 ... 𝑁 ) → 𝐼 ∈ ℤ )
2 1fzopredsuc ⊢ ( 𝑁 ∈ ℕ0 → ( 0 ... 𝑁 ) = ( ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) ∪ { 𝑁 } ) )
3 2 eleq2d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐼 ∈ ( 0 ... 𝑁 ) ↔ 𝐼 ∈ ( ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) ∪ { 𝑁 } ) ) )
4 elun ⊢ ( 𝐼 ∈ ( ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) ∪ { 𝑁 } ) ↔ ( 𝐼 ∈ ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) ∨ 𝐼 ∈ { 𝑁 } ) )
5 elun ⊢ ( 𝐼 ∈ ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) ↔ ( 𝐼 ∈ { 0 } ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ) )
6 5 orbi1i ⊢ ( ( 𝐼 ∈ ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) ∨ 𝐼 ∈ { 𝑁 } ) ↔ ( ( 𝐼 ∈ { 0 } ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ) ∨ 𝐼 ∈ { 𝑁 } ) )
7 4 6 bitri ⊢ ( 𝐼 ∈ ( ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) ∪ { 𝑁 } ) ↔ ( ( 𝐼 ∈ { 0 } ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ) ∨ 𝐼 ∈ { 𝑁 } ) )
8 elsng ⊢ ( 𝐼 ∈ ℤ → ( 𝐼 ∈ { 0 } ↔ 𝐼 = 0 ) )
9 8 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ ) → ( 𝐼 ∈ { 0 } ↔ 𝐼 = 0 ) )
10 9 orbi1d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ ) → ( ( 𝐼 ∈ { 0 } ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ) ↔ ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ) ) )
11 elsng ⊢ ( 𝐼 ∈ ℤ → ( 𝐼 ∈ { 𝑁 } ↔ 𝐼 = 𝑁 ) )
12 11 adantl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ ) → ( 𝐼 ∈ { 𝑁 } ↔ 𝐼 = 𝑁 ) )
13 10 12 orbi12d ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ ) → ( ( ( 𝐼 ∈ { 0 } ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ) ∨ 𝐼 ∈ { 𝑁 } ) ↔ ( ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ) ∨ 𝐼 = 𝑁 ) ) )
14 7 13 syl5bb ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ ) → ( 𝐼 ∈ ( ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) ∪ { 𝑁 } ) ↔ ( ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ) ∨ 𝐼 = 𝑁 ) ) )
15 df-3or ⊢ ( ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 = 𝑁 ) ↔ ( ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ) ∨ 𝐼 = 𝑁 ) )
16 15 biimpri ⊢ ( ( ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ) ∨ 𝐼 = 𝑁 ) → ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 = 𝑁 ) )
17 14 16 syl6bi ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝐼 ∈ ℤ ) → ( 𝐼 ∈ ( ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) ∪ { 𝑁 } ) → ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 = 𝑁 ) ) )
18 17 ex ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐼 ∈ ℤ → ( 𝐼 ∈ ( ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) ∪ { 𝑁 } ) → ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 = 𝑁 ) ) ) )
19 18 com23 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐼 ∈ ( ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) ∪ { 𝑁 } ) → ( 𝐼 ∈ ℤ → ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 = 𝑁 ) ) ) )
20 3 19 sylbid ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐼 ∈ ( 0 ... 𝑁 ) → ( 𝐼 ∈ ℤ → ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 = 𝑁 ) ) ) )
21 1 20 mpdi ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐼 ∈ ( 0 ... 𝑁 ) → ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 = 𝑁 ) ) )
22 c0ex ⊢ 0 ∈ V
23 22 snid ⊢ 0 ∈ { 0 }
24 23 a1i ⊢ ( 𝐼 = 0 → 0 ∈ { 0 } )
25 eleq1 ⊢ ( 𝐼 = 0 → ( 𝐼 ∈ { 0 } ↔ 0 ∈ { 0 } ) )
26 24 25 mpbird ⊢ ( 𝐼 = 0 → 𝐼 ∈ { 0 } )
27 26 a1i ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐼 = 0 → 𝐼 ∈ { 0 } ) )
28 idd ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐼 ∈ ( 1 ..^ 𝑁 ) → 𝐼 ∈ ( 1 ..^ 𝑁 ) ) )
29 snidg ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ { 𝑁 } )
30 eleq1 ⊢ ( 𝐼 = 𝑁 → ( 𝐼 ∈ { 𝑁 } ↔ 𝑁 ∈ { 𝑁 } ) )
31 29 30 syl5ibrcom ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐼 = 𝑁 → 𝐼 ∈ { 𝑁 } ) )
32 27 28 31 3orim123d ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 = 𝑁 ) → ( 𝐼 ∈ { 0 } ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 ∈ { 𝑁 } ) ) )
33 32 imp ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 = 𝑁 ) ) → ( 𝐼 ∈ { 0 } ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 ∈ { 𝑁 } ) )
34 df-3or ⊢ ( ( 𝐼 ∈ { 0 } ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 ∈ { 𝑁 } ) ↔ ( ( 𝐼 ∈ { 0 } ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ) ∨ 𝐼 ∈ { 𝑁 } ) )
35 33 34 sylib ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 = 𝑁 ) ) → ( ( 𝐼 ∈ { 0 } ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ) ∨ 𝐼 ∈ { 𝑁 } ) )
36 35 7 sylibr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 = 𝑁 ) ) → 𝐼 ∈ ( ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) ∪ { 𝑁 } ) )
37 3 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 = 𝑁 ) ) → ( 𝐼 ∈ ( 0 ... 𝑁 ) ↔ 𝐼 ∈ ( ( { 0 } ∪ ( 1 ..^ 𝑁 ) ) ∪ { 𝑁 } ) ) )
38 36 37 mpbird ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 = 𝑁 ) ) → 𝐼 ∈ ( 0 ... 𝑁 ) )
39 38 ex ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 = 𝑁 ) → 𝐼 ∈ ( 0 ... 𝑁 ) ) )
40 21 39 impbid ⊢ ( 𝑁 ∈ ℕ0 → ( 𝐼 ∈ ( 0 ... 𝑁 ) ↔ ( 𝐼 = 0 ∨ 𝐼 ∈ ( 1 ..^ 𝑁 ) ∨ 𝐼 = 𝑁 ) ) )