# Metamath Proof Explorer

## Theorem s3fn

Description: A length 3 word is a function with a triple as domain. (Contributed by Alexander van der Vekens, 5-Dec-2017) (Revised by AV, 23-Jan-2021)

Ref Expression
Assertion s3fn ${⊢}\left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\to ⟨“{A}{B}{C}”⟩Fn\left\{0,1,2\right\}$

### Proof

Step Hyp Ref Expression
1 s3cl ${⊢}\left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\to ⟨“{A}{B}{C}”⟩\in \mathrm{Word}{V}$
2 wrdfn ${⊢}⟨“{A}{B}{C}”⟩\in \mathrm{Word}{V}\to ⟨“{A}{B}{C}”⟩Fn\left(0..^\left|⟨“{A}{B}{C}”⟩\right|\right)$
3 1 2 syl ${⊢}\left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\to ⟨“{A}{B}{C}”⟩Fn\left(0..^\left|⟨“{A}{B}{C}”⟩\right|\right)$
4 s3len ${⊢}\left|⟨“{A}{B}{C}”⟩\right|=3$
5 4 oveq2i ${⊢}\left(0..^\left|⟨“{A}{B}{C}”⟩\right|\right)=\left(0..^3\right)$
6 fzo0to3tp ${⊢}\left(0..^3\right)=\left\{0,1,2\right\}$
7 5 6 eqtr2i ${⊢}\left\{0,1,2\right\}=\left(0..^\left|⟨“{A}{B}{C}”⟩\right|\right)$
8 7 fneq2i ${⊢}⟨“{A}{B}{C}”⟩Fn\left\{0,1,2\right\}↔⟨“{A}{B}{C}”⟩Fn\left(0..^\left|⟨“{A}{B}{C}”⟩\right|\right)$
9 3 8 sylibr ${⊢}\left({A}\in {V}\wedge {B}\in {V}\wedge {C}\in {V}\right)\to ⟨“{A}{B}{C}”⟩Fn\left\{0,1,2\right\}$