fcobijfs2

Description: Composing finitely supported functions with a bijection yields a bijection between sets of finitely supported functions. See also fcobijfs and mapfien . (Contributed by Thierry Arnoux, 10-Jan-2026)

	Ref	Expression
Hypotheses	fcobijfs2.1	$⊢ φ \to G : R \underset{1-1 onto}{⟶} S$
	fcobijfs2.2	$⊢ φ \to R \in U$
	fcobijfs2.3	$⊢ φ \to S \in V$
	fcobijfs2.4	$⊢ φ \to T \in W$
	fcobijfs2.5	$⊢ φ \to O \in T$
	fcobijfs2.7	$⊢ X = \{g \in (T^{S}) \| {finSupp}_{O} (g)\}$
	fcobijfs2.8	$⊢ Y = \{h \in (T^{R}) \| {finSupp}_{O} (h)\}$
Assertion	fcobijfs2	$⊢ φ \to (f \in X ⟼ f \circ G) : X \underset{1-1 onto}{⟶} Y$

Proof

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

Metamath Proof Explorer

Theorem fcobijfs2

Proof