Description: A nonempty mapping has a prefix. (Contributed by Stefan O'Rear, 10-Oct-2014) (Revised by Stefan O'Rear, 5-May-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | mapfzcons.1 | ⊢ 𝑀 = ( 𝑁 + 1 ) | |
| Assertion | mapfzcons1cl | ⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 1 ... 𝑀 ) ) → ( 𝐴 ↾ ( 1 ... 𝑁 ) ) ∈ ( 𝐵 ↑m ( 1 ... 𝑁 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mapfzcons.1 | ⊢ 𝑀 = ( 𝑁 + 1 ) | |
| 2 | fzssp1 | ⊢ ( 1 ... 𝑁 ) ⊆ ( 1 ... ( 𝑁 + 1 ) ) | |
| 3 | 1 | oveq2i | ⊢ ( 1 ... 𝑀 ) = ( 1 ... ( 𝑁 + 1 ) ) |
| 4 | 2 3 | sseqtrri | ⊢ ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝑀 ) |
| 5 | elmapssres | ⊢ ( ( 𝐴 ∈ ( 𝐵 ↑m ( 1 ... 𝑀 ) ) ∧ ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝑀 ) ) → ( 𝐴 ↾ ( 1 ... 𝑁 ) ) ∈ ( 𝐵 ↑m ( 1 ... 𝑁 ) ) ) | |
| 6 | 4 5 | mpan2 | ⊢ ( 𝐴 ∈ ( 𝐵 ↑m ( 1 ... 𝑀 ) ) → ( 𝐴 ↾ ( 1 ... 𝑁 ) ) ∈ ( 𝐵 ↑m ( 1 ... 𝑁 ) ) ) |