Metamath Proof Explorer


Theorem fcobijfs

Description: Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also mapfien . (Contributed by Thierry Arnoux, 25-Aug-2017) (Revised by Thierry Arnoux, 1-Sep-2019)

Ref Expression
Hypotheses fcobij.1 φ G : S 1-1 onto T
fcobij.2 φ R U
fcobij.3 φ S V
fcobij.4 φ T W
fcobijfs.5 φ O S
fcobijfs.6 Q = G O
fcobijfs.7 X = g S R | finSupp O g
fcobijfs.8 Y = h T R | finSupp Q h
Assertion fcobijfs φ f X G f : X 1-1 onto Y

Proof

Step Hyp Ref Expression
1 fcobij.1 φ G : S 1-1 onto T
2 fcobij.2 φ R U
3 fcobij.3 φ S V
4 fcobij.4 φ T W
5 fcobijfs.5 φ O S
6 fcobijfs.6 Q = G O
7 fcobijfs.7 X = g S R | finSupp O g
8 fcobijfs.8 Y = h T R | finSupp Q h
9 breq1 h = g finSupp O h finSupp O g
10 9 cbvrabv h S R | finSupp O h = g S R | finSupp O g
11 7 10 eqtr4i X = h S R | finSupp O h
12 f1oi I R : R 1-1 onto R
13 12 a1i φ I R : R 1-1 onto R
14 11 8 6 13 1 2 3 2 4 5 mapfien φ f X G f I R : X 1-1 onto Y
15 7 ssrab3 X S R
16 15 sseli f X f S R
17 coass G f I R = G f I R
18 f1of G : S 1-1 onto T G : S T
19 1 18 syl φ G : S T
20 elmapi f S R f : R S
21 fco G : S T f : R S G f : R T
22 19 20 21 syl2an φ f S R G f : R T
23 fcoi1 G f : R T G f I R = G f
24 22 23 syl φ f S R G f I R = G f
25 17 24 eqtr3id φ f S R G f I R = G f
26 16 25 sylan2 φ f X G f I R = G f
27 26 mpteq2dva φ f X G f I R = f X G f
28 27 f1oeq1d φ f X G f I R : X 1-1 onto Y f X G f : X 1-1 onto Y
29 14 28 mpbid φ f X G f : X 1-1 onto Y