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	$⊢ φ \to G : S \underset{1-1 onto}{⟶} T$
	fcobij.2	$⊢ φ \to R \in U$
	fcobij.3	$⊢ φ \to S \in V$
	fcobij.4	$⊢ φ \to T \in W$
	fcobijfs.5	$⊢ φ \to O \in S$
	fcobijfs.6	$⊢ Q = G (O)$
	fcobijfs.7	$⊢ X = \{g \in (S^{R}) \| {finSupp}_{O} (g)\}$
	fcobijfs.8	$⊢ Y = \{h \in (T^{R}) \| {finSupp}_{Q} (h)\}$
Assertion	fcobijfs	$⊢ φ \to (f \in X ⟼ G \circ f) : X \underset{1-1 onto}{⟶} Y$

Proof

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

Metamath Proof Explorer

Theorem fcobijfs

Proof