Metamath Proof Explorer


Theorem lenco

Description: Length of a mapped word is unchanged. (Contributed by Stefan O'Rear, 27-Aug-2015)

Ref Expression
Assertion lenco W Word A F : A B F W = W

Proof

Step Hyp Ref Expression
1 simpr W Word A F : A B F : A B
2 wrdf W Word A W : 0 ..^ W A
3 2 adantr W Word A F : A B W : 0 ..^ W A
4 fco F : A B W : 0 ..^ W A F W : 0 ..^ W B
5 1 3 4 syl2anc W Word A F : A B F W : 0 ..^ W B
6 ffn F W : 0 ..^ W B F W Fn 0 ..^ W
7 hashfn F W Fn 0 ..^ W F W = 0 ..^ W
8 5 6 7 3syl W Word A F : A B F W = 0 ..^ W
9 ffn W : 0 ..^ W A W Fn 0 ..^ W
10 hashfn W Fn 0 ..^ W W = 0 ..^ W
11 3 9 10 3syl W Word A F : A B W = 0 ..^ W
12 8 11 eqtr4d W Word A F : A B F W = W