Metamath Proof Explorer


Theorem frnfsuppbi

Description: Two ways of saying that a function with known codomain is finitely supported. (Contributed by AV, 8-Jul-2019)

Ref Expression
Assertion frnfsuppbi I V Z W F : I S finSupp Z F F -1 S Z Fin

Proof

Step Hyp Ref Expression
1 ffun F : I S Fun F
2 1 adantl I V Z W F : I S Fun F
3 fex F : I S I V F V
4 3 expcom I V F : I S F V
5 4 adantr I V Z W F : I S F V
6 5 imp I V Z W F : I S F V
7 simplr I V Z W F : I S Z W
8 funisfsupp Fun F F V Z W finSupp Z F F supp Z Fin
9 2 6 7 8 syl3anc I V Z W F : I S finSupp Z F F supp Z Fin
10 frnsuppeq I V Z W F : I S F supp Z = F -1 S Z
11 10 imp I V Z W F : I S F supp Z = F -1 S Z
12 11 eleq1d I V Z W F : I S F supp Z Fin F -1 S Z Fin
13 9 12 bitrd I V Z W F : I S finSupp Z F F -1 S Z Fin
14 13 ex I V Z W F : I S finSupp Z F F -1 S Z Fin