Description: Definition of the codomain extractor for an arrow. (Contributed by FL, 26-Oct-2007) (Revised by Mario Carneiro, 11-Jan-2017)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-coda | ⊢ coda = ( 2nd ∘ 1st ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | ccoda | ⊢ coda | |
| 1 | c2nd | ⊢ 2nd | |
| 2 | c1st | ⊢ 1st | |
| 3 | 1 2 | ccom | ⊢ ( 2nd ∘ 1st ) |
| 4 | 0 3 | wceq | ⊢ coda = ( 2nd ∘ 1st ) |