mrsubff1

Description: When restricted to complete mappings, the substitution-producing function is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mrsubvr.v	$⊢ V = mVR (T)$
	mrsubvr.r	$⊢ R = mREx (T)$
	mrsubvr.s	$⊢ S = mRSubst (T)$
Assertion	mrsubff1	$⊢ T \in W \to ({S ↾}_{(R^{V})}) : R^{V} \underset{1-1}{⟶} R^{R}$

Proof

Step	Hyp	Ref	Expression
1		mrsubvr.v	$⊢ V = mVR (T)$
2		mrsubvr.r	$⊢ R = mREx (T)$
3		mrsubvr.s	$⊢ S = mRSubst (T)$
4	1 2 3	mrsubff	$⊢ T \in W \to S : R ↑_{𝑝𝑚} V ⟶ R^{R}$
5		mapsspm	$⊢ R^{V} \subseteq R ↑_{𝑝𝑚} V$
6	5	a1i	$⊢ T \in W \to R^{V} \subseteq R ↑_{𝑝𝑚} V$
7	4 6	fssresd	$⊢ T \in W \to ({S ↾}_{(R^{V})}) : R^{V} ⟶ R^{R}$
8		fveq1	$⊢ S (f) = S (g) \to S (f) (⟨“ v ”⟩) = S (g) (⟨“ v ”⟩)$
9		simplrl	$⊢ ((T \in W \land (f \in (R^{V}) \land g \in (R^{V}))) \land v \in V) \to f \in (R^{V})$
10		elmapi	$⊢ f \in (R^{V}) \to f : V ⟶ R$
11	9 10	syl	$⊢ ((T \in W \land (f \in (R^{V}) \land g \in (R^{V}))) \land v \in V) \to f : V ⟶ R$
12		ssidd	$⊢ ((T \in W \land (f \in (R^{V}) \land g \in (R^{V}))) \land v \in V) \to V \subseteq V$
13		simpr	$⊢ ((T \in W \land (f \in (R^{V}) \land g \in (R^{V}))) \land v \in V) \to v \in V$
14	1 2 3	mrsubvr	$⊢ (f : V ⟶ R \land V \subseteq V \land v \in V) \to S (f) (⟨“ v ”⟩) = f (v)$
15	11 12 13 14	syl3anc	$⊢ ((T \in W \land (f \in (R^{V}) \land g \in (R^{V}))) \land v \in V) \to S (f) (⟨“ v ”⟩) = f (v)$
16		simplrr	$⊢ ((T \in W \land (f \in (R^{V}) \land g \in (R^{V}))) \land v \in V) \to g \in (R^{V})$
17		elmapi	$⊢ g \in (R^{V}) \to g : V ⟶ R$
18	16 17	syl	$⊢ ((T \in W \land (f \in (R^{V}) \land g \in (R^{V}))) \land v \in V) \to g : V ⟶ R$
19	1 2 3	mrsubvr	$⊢ (g : V ⟶ R \land V \subseteq V \land v \in V) \to S (g) (⟨“ v ”⟩) = g (v)$
20	18 12 13 19	syl3anc	$⊢ ((T \in W \land (f \in (R^{V}) \land g \in (R^{V}))) \land v \in V) \to S (g) (⟨“ v ”⟩) = g (v)$
21	15 20	eqeq12d	$⊢ ((T \in W \land (f \in (R^{V}) \land g \in (R^{V}))) \land v \in V) \to (S (f) (⟨“ v ”⟩) = S (g) (⟨“ v ”⟩) \leftrightarrow f (v) = g (v))$
22	8 21	imbitrid	$⊢ ((T \in W \land (f \in (R^{V}) \land g \in (R^{V}))) \land v \in V) \to (S (f) = S (g) \to f (v) = g (v))$
23	22	ralrimdva	$⊢ (T \in W \land (f \in (R^{V}) \land g \in (R^{V}))) \to (S (f) = S (g) \to \forall v \in V f (v) = g (v))$
24		fvres	$⊢ f \in (R^{V}) \to ({S ↾}_{(R^{V})}) (f) = S (f)$
25		fvres	$⊢ g \in (R^{V}) \to ({S ↾}_{(R^{V})}) (g) = S (g)$
26	24 25	eqeqan12d	$⊢ (f \in (R^{V}) \land g \in (R^{V})) \to (({S ↾}_{(R^{V})}) (f) = ({S ↾}_{(R^{V})}) (g) \leftrightarrow S (f) = S (g))$
27	26	adantl	$⊢ (T \in W \land (f \in (R^{V}) \land g \in (R^{V}))) \to (({S ↾}_{(R^{V})}) (f) = ({S ↾}_{(R^{V})}) (g) \leftrightarrow S (f) = S (g))$
28		ffn	$⊢ f : V ⟶ R \to f Fn V$
29		ffn	$⊢ g : V ⟶ R \to g Fn V$
30		eqfnfv	$⊢ (f Fn V \land g Fn V) \to (f = g \leftrightarrow \forall v \in V f (v) = g (v))$
31	28 29 30	syl2an	$⊢ (f : V ⟶ R \land g : V ⟶ R) \to (f = g \leftrightarrow \forall v \in V f (v) = g (v))$
32	10 17 31	syl2an	$⊢ (f \in (R^{V}) \land g \in (R^{V})) \to (f = g \leftrightarrow \forall v \in V f (v) = g (v))$
33	32	adantl	$⊢ (T \in W \land (f \in (R^{V}) \land g \in (R^{V}))) \to (f = g \leftrightarrow \forall v \in V f (v) = g (v))$
34	23 27 33	3imtr4d	$⊢ (T \in W \land (f \in (R^{V}) \land g \in (R^{V}))) \to (({S ↾}_{(R^{V})}) (f) = ({S ↾}_{(R^{V})}) (g) \to f = g)$
35	34	ralrimivva	$⊢ T \in W \to \forall f \in (R^{V}) \forall g \in (R^{V}) (({S ↾}_{(R^{V})}) (f) = ({S ↾}_{(R^{V})}) (g) \to f = g)$
36		dff13	$⊢ ({S ↾}_{(R^{V})}) : R^{V} \underset{1-1}{⟶} R^{R} \leftrightarrow (({S ↾}_{(R^{V})}) : R^{V} ⟶ R^{R} \land \forall f \in (R^{V}) \forall g \in (R^{V}) (({S ↾}_{(R^{V})}) (f) = ({S ↾}_{(R^{V})}) (g) \to f = g))$
37	7 35 36	sylanbrc	$⊢ T \in W \to ({S ↾}_{(R^{V})}) : R^{V} \underset{1-1}{⟶} R^{R}$

Metamath Proof Explorer

Theorem mrsubff1

Proof