fcobij

Description: Composing functions with a bijection yields a bijection between sets of functions. (Contributed by Thierry Arnoux, 25-Aug-2017)

	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$
Assertion	fcobij	$⊢ φ \to (f \in (S^{R}) ⟼ G \circ f) : S^{R} \underset{1-1 onto}{⟶} T^{R}$

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		eqid	$⊢ (f \in (S^{R}) ⟼ G \circ f) = (f \in (S^{R}) ⟼ G \circ f)$
6		f1of	$⊢ G : S \underset{1-1 onto}{⟶} T \to G : S ⟶ T$
7	1 6	syl	$⊢ φ \to G : S ⟶ T$
8	7	adantr	$⊢ (φ \land f \in (S^{R})) \to G : S ⟶ T$
9	3 2	elmapd	$⊢ φ \to (f \in (S^{R}) \leftrightarrow f : R ⟶ S)$
10	9	biimpa	$⊢ (φ \land f \in (S^{R})) \to f : R ⟶ S$
11		fco	$⊢ (G : S ⟶ T \land f : R ⟶ S) \to (G \circ f) : R ⟶ T$
12	8 10 11	syl2anc	$⊢ (φ \land f \in (S^{R})) \to (G \circ f) : R ⟶ T$
13	4 2	elmapd	$⊢ φ \to (G \circ f \in (T^{R}) \leftrightarrow (G \circ f) : R ⟶ T)$
14	13	adantr	$⊢ (φ \land f \in (S^{R})) \to (G \circ f \in (T^{R}) \leftrightarrow (G \circ f) : R ⟶ T)$
15	12 14	mpbird	$⊢ (φ \land f \in (S^{R})) \to G \circ f \in (T^{R})$
16		f1ocnv	$⊢ G : S \underset{1-1 onto}{⟶} T \to G^{-1} : T \underset{1-1 onto}{⟶} S$
17		f1of	$⊢ G^{-1} : T \underset{1-1 onto}{⟶} S \to G^{-1} : T ⟶ S$
18	1 16 17	3syl	$⊢ φ \to G^{-1} : T ⟶ S$
19	18	adantr	$⊢ (φ \land h \in (T^{R})) \to G^{-1} : T ⟶ S$
20	4 2	elmapd	$⊢ φ \to (h \in (T^{R}) \leftrightarrow h : R ⟶ T)$
21	20	biimpa	$⊢ (φ \land h \in (T^{R})) \to h : R ⟶ T$
22		fco	$⊢ (G^{-1} : T ⟶ S \land h : R ⟶ T) \to (G^{-1} \circ h) : R ⟶ S$
23	19 21 22	syl2anc	$⊢ (φ \land h \in (T^{R})) \to (G^{-1} \circ h) : R ⟶ S$
24	3 2	elmapd	$⊢ φ \to (G^{-1} \circ h \in (S^{R}) \leftrightarrow (G^{-1} \circ h) : R ⟶ S)$
25	24	adantr	$⊢ (φ \land h \in (T^{R})) \to (G^{-1} \circ h \in (S^{R}) \leftrightarrow (G^{-1} \circ h) : R ⟶ S)$
26	23 25	mpbird	$⊢ (φ \land h \in (T^{R})) \to G^{-1} \circ h \in (S^{R})$
27		simpr	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land f = G^{-1} \circ h) \to f = G^{-1} \circ h$
28	27	coeq2d	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land f = G^{-1} \circ h) \to G \circ f = G \circ (G^{-1} \circ h)$
29		coass	$⊢ (G \circ G^{-1}) \circ h = G \circ (G^{-1} \circ h)$
30	28 29	eqtr4di	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land f = G^{-1} \circ h) \to G \circ f = (G \circ G^{-1}) \circ h$
31		simpll	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land f = G^{-1} \circ h) \to φ$
32		f1ococnv2	$⊢ G : S \underset{1-1 onto}{⟶} T \to G \circ G^{-1} = {I ↾}_{T}$
33	31 1 32	3syl	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land f = G^{-1} \circ h) \to G \circ G^{-1} = {I ↾}_{T}$
34	33	coeq1d	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land f = G^{-1} \circ h) \to (G \circ G^{-1}) \circ h = ({I ↾}_{T}) \circ h$
35		simplrr	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land f = G^{-1} \circ h) \to h \in (T^{R})$
36	31 35 21	syl2anc	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land f = G^{-1} \circ h) \to h : R ⟶ T$
37		fcoi2	$⊢ h : R ⟶ T \to ({I ↾}_{T}) \circ h = h$
38	36 37	syl	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land f = G^{-1} \circ h) \to ({I ↾}_{T}) \circ h = h$
39	30 34 38	3eqtrrd	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land f = G^{-1} \circ h) \to h = G \circ f$
40		simpr	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land h = G \circ f) \to h = G \circ f$
41	40	coeq2d	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land h = G \circ f) \to G^{-1} \circ h = G^{-1} \circ (G \circ f)$
42		coass	$⊢ (G^{-1} \circ G) \circ f = G^{-1} \circ (G \circ f)$
43	41 42	eqtr4di	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land h = G \circ f) \to G^{-1} \circ h = (G^{-1} \circ G) \circ f$
44		simpll	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land h = G \circ f) \to φ$
45		f1ococnv1	$⊢ G : S \underset{1-1 onto}{⟶} T \to G^{-1} \circ G = {I ↾}_{S}$
46	44 1 45	3syl	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land h = G \circ f) \to G^{-1} \circ G = {I ↾}_{S}$
47	46	coeq1d	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land h = G \circ f) \to (G^{-1} \circ G) \circ f = ({I ↾}_{S}) \circ f$
48		simplrl	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land h = G \circ f) \to f \in (S^{R})$
49	44 48 10	syl2anc	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land h = G \circ f) \to f : R ⟶ S$
50		fcoi2	$⊢ f : R ⟶ S \to ({I ↾}_{S}) \circ f = f$
51	49 50	syl	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land h = G \circ f) \to ({I ↾}_{S}) \circ f = f$
52	43 47 51	3eqtrrd	$⊢ ((φ \land (f \in (S^{R}) \land h \in (T^{R}))) \land h = G \circ f) \to f = G^{-1} \circ h$
53	39 52	impbida	$⊢ (φ \land (f \in (S^{R}) \land h \in (T^{R}))) \to (f = G^{-1} \circ h \leftrightarrow h = G \circ f)$
54	5 15 26 53	f1o2d	$⊢ φ \to (f \in (S^{R}) ⟼ G \circ f) : S^{R} \underset{1-1 onto}{⟶} T^{R}$

Metamath Proof Explorer

Theorem fcobij

Proof