msubff1

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

	Ref	Expression
Hypotheses	msubff1.v	$⊢ V = mVR (T)$
	msubff1.r	$⊢ R = mREx (T)$
	msubff1.s	$⊢ S = mSubst (T)$
	msubff1.e	$⊢ E = mEx (T)$
Assertion	msubff1	$⊢ T \in mFS \to ({S ↾}_{(R^{V})}) : R^{V} \underset{1-1}{⟶} E^{E}$

Proof

Step	Hyp	Ref	Expression
1		msubff1.v	$⊢ V = mVR (T)$
2		msubff1.r	$⊢ R = mREx (T)$
3		msubff1.s	$⊢ S = mSubst (T)$
4		msubff1.e	$⊢ E = mEx (T)$
5	1 2 3 4	msubff	$⊢ T \in mFS \to S : R ↑_{𝑝𝑚} V ⟶ E^{E}$
6		mapsspm	$⊢ R^{V} \subseteq R ↑_{𝑝𝑚} V$
7	6	a1i	$⊢ T \in mFS \to R^{V} \subseteq R ↑_{𝑝𝑚} V$
8	5 7	fssresd	$⊢ T \in mFS \to ({S ↾}_{(R^{V})}) : R^{V} ⟶ E^{E}$
9		eqid	$⊢ mRSubst (T) = mRSubst (T)$
10	1 2 9	mrsubff	$⊢ T \in mFS \to mRSubst (T) : R ↑_{𝑝𝑚} V ⟶ R^{R}$
11	10	ad2antrr	$⊢ ((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \to mRSubst (T) : R ↑_{𝑝𝑚} V ⟶ R^{R}$
12		simplrl	$⊢ ((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \to f \in (R^{V})$
13	6 12	sseldi	$⊢ ((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \to f \in (R ↑_{𝑝𝑚} V)$
14	11 13	ffvelrnd	$⊢ ((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \to mRSubst (T) (f) \in (R^{R})$
15		elmapi	$⊢ mRSubst (T) (f) \in (R^{R}) \to mRSubst (T) (f) : R ⟶ R$
16		ffn	$⊢ mRSubst (T) (f) : R ⟶ R \to mRSubst (T) (f) Fn R$
17	14 15 16	3syl	$⊢ ((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \to mRSubst (T) (f) Fn R$
18		simplrr	$⊢ ((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \to g \in (R^{V})$
19	6 18	sseldi	$⊢ ((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \to g \in (R ↑_{𝑝𝑚} V)$
20	11 19	ffvelrnd	$⊢ ((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \to mRSubst (T) (g) \in (R^{R})$
21		elmapi	$⊢ mRSubst (T) (g) \in (R^{R}) \to mRSubst (T) (g) : R ⟶ R$
22		ffn	$⊢ mRSubst (T) (g) : R ⟶ R \to mRSubst (T) (g) Fn R$
23	20 21 22	3syl	$⊢ ((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \to mRSubst (T) (g) Fn R$
24		simplrr	$⊢ (((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \land r \in R) \to S (f) = S (g)$
25	24	fveq1d	$⊢ (((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \land r \in R) \to S (f) (⟨mType (T) (v), r⟩) = S (g) (⟨mType (T) (v), r⟩)$
26	12	adantr	$⊢ (((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \land r \in R) \to f \in (R^{V})$
27		elmapi	$⊢ f \in (R^{V}) \to f : V ⟶ R$
28	26 27	syl	$⊢ (((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \land r \in R) \to f : V ⟶ R$
29		ssidd	$⊢ (((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \land r \in R) \to V \subseteq V$
30		eqid	$⊢ mTC (T) = mTC (T)$
31		eqid	$⊢ mType (T) = mType (T)$
32	1 30 31	mtyf2	$⊢ T \in mFS \to mType (T) : V ⟶ mTC (T)$
33	32	ad3antrrr	$⊢ (((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \land r \in R) \to mType (T) : V ⟶ mTC (T)$
34		simplrl	$⊢ (((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \land r \in R) \to v \in V$
35	33 34	ffvelrnd	$⊢ (((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \land r \in R) \to mType (T) (v) \in mTC (T)$
36		opelxpi	$⊢ (mType (T) (v) \in mTC (T) \land r \in R) \to ⟨mType (T) (v), r⟩ \in (mTC (T) \times R)$
37	35 36	sylancom	$⊢ (((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \land r \in R) \to ⟨mType (T) (v), r⟩ \in (mTC (T) \times R)$
38	30 4 2	mexval	$⊢ E = mTC (T) \times R$
39	37 38	eleqtrrdi	$⊢ (((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \land r \in R) \to ⟨mType (T) (v), r⟩ \in E$
40	1 2 3 4 9	msubval	$⊢ (f : V ⟶ R \land V \subseteq V \land ⟨mType (T) (v), r⟩ \in E) \to S (f) (⟨mType (T) (v), r⟩) = ⟨1^{st} (⟨mType (T) (v), r⟩), mRSubst (T) (f) (2^{nd} (⟨mType (T) (v), r⟩))⟩$
41	28 29 39 40	syl3anc	$⊢ (((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \land r \in R) \to S (f) (⟨mType (T) (v), r⟩) = ⟨1^{st} (⟨mType (T) (v), r⟩), mRSubst (T) (f) (2^{nd} (⟨mType (T) (v), r⟩))⟩$
42	18	adantr	$⊢ (((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \land r \in R) \to g \in (R^{V})$
43		elmapi	$⊢ g \in (R^{V}) \to g : V ⟶ R$
44	42 43	syl	$⊢ (((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \land r \in R) \to g : V ⟶ R$
45	1 2 3 4 9	msubval	$⊢ (g : V ⟶ R \land V \subseteq V \land ⟨mType (T) (v), r⟩ \in E) \to S (g) (⟨mType (T) (v), r⟩) = ⟨1^{st} (⟨mType (T) (v), r⟩), mRSubst (T) (g) (2^{nd} (⟨mType (T) (v), r⟩))⟩$
46	44 29 39 45	syl3anc	$⊢ (((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \land r \in R) \to S (g) (⟨mType (T) (v), r⟩) = ⟨1^{st} (⟨mType (T) (v), r⟩), mRSubst (T) (g) (2^{nd} (⟨mType (T) (v), r⟩))⟩$
47	25 41 46	3eqtr3d	$⊢ (((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \land r \in R) \to ⟨1^{st} (⟨mType (T) (v), r⟩), mRSubst (T) (f) (2^{nd} (⟨mType (T) (v), r⟩))⟩ = ⟨1^{st} (⟨mType (T) (v), r⟩), mRSubst (T) (g) (2^{nd} (⟨mType (T) (v), r⟩))⟩$
48		fvex	$⊢ 1^{st} (⟨mType (T) (v), r⟩) \in V$
49		fvex	$⊢ mRSubst (T) (f) (2^{nd} (⟨mType (T) (v), r⟩)) \in V$
50	48 49	opth	$⊢ ⟨1^{st} (⟨mType (T) (v), r⟩), mRSubst (T) (f) (2^{nd} (⟨mType (T) (v), r⟩))⟩ = ⟨1^{st} (⟨mType (T) (v), r⟩), mRSubst (T) (g) (2^{nd} (⟨mType (T) (v), r⟩))⟩ \leftrightarrow (1^{st} (⟨mType (T) (v), r⟩) = 1^{st} (⟨mType (T) (v), r⟩) \land mRSubst (T) (f) (2^{nd} (⟨mType (T) (v), r⟩)) = mRSubst (T) (g) (2^{nd} (⟨mType (T) (v), r⟩)))$
51	50	simprbi	$⊢ ⟨1^{st} (⟨mType (T) (v), r⟩), mRSubst (T) (f) (2^{nd} (⟨mType (T) (v), r⟩))⟩ = ⟨1^{st} (⟨mType (T) (v), r⟩), mRSubst (T) (g) (2^{nd} (⟨mType (T) (v), r⟩))⟩ \to mRSubst (T) (f) (2^{nd} (⟨mType (T) (v), r⟩)) = mRSubst (T) (g) (2^{nd} (⟨mType (T) (v), r⟩))$
52	47 51	syl	$⊢ (((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \land r \in R) \to mRSubst (T) (f) (2^{nd} (⟨mType (T) (v), r⟩)) = mRSubst (T) (g) (2^{nd} (⟨mType (T) (v), r⟩))$
53		fvex	$⊢ mType (T) (v) \in V$
54		vex	$⊢ r \in V$
55	53 54	op2nd	$⊢ 2^{nd} (⟨mType (T) (v), r⟩) = r$
56	55	fveq2i	$⊢ mRSubst (T) (f) (2^{nd} (⟨mType (T) (v), r⟩)) = mRSubst (T) (f) (r)$
57	55	fveq2i	$⊢ mRSubst (T) (g) (2^{nd} (⟨mType (T) (v), r⟩)) = mRSubst (T) (g) (r)$
58	52 56 57	3eqtr3g	$⊢ (((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \land r \in R) \to mRSubst (T) (f) (r) = mRSubst (T) (g) (r)$
59	17 23 58	eqfnfvd	$⊢ ((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \to mRSubst (T) (f) = mRSubst (T) (g)$
60	1 2 9	mrsubff1	$⊢ T \in mFS \to ({mRSubst (T) ↾}_{(R^{V})}) : R^{V} \underset{1-1}{⟶} R^{R}$
61		f1fveq	$⊢ (({mRSubst (T) ↾}_{(R^{V})}) : R^{V} \underset{1-1}{⟶} R^{R} \land (f \in (R^{V}) \land g \in (R^{V}))) \to (({mRSubst (T) ↾}_{(R^{V})}) (f) = ({mRSubst (T) ↾}_{(R^{V})}) (g) \leftrightarrow f = g)$
62	60 61	sylan	$⊢ (T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \to (({mRSubst (T) ↾}_{(R^{V})}) (f) = ({mRSubst (T) ↾}_{(R^{V})}) (g) \leftrightarrow f = g)$
63		fvres	$⊢ f \in (R^{V}) \to ({mRSubst (T) ↾}_{(R^{V})}) (f) = mRSubst (T) (f)$
64		fvres	$⊢ g \in (R^{V}) \to ({mRSubst (T) ↾}_{(R^{V})}) (g) = mRSubst (T) (g)$
65	63 64	eqeqan12d	$⊢ (f \in (R^{V}) \land g \in (R^{V})) \to (({mRSubst (T) ↾}_{(R^{V})}) (f) = ({mRSubst (T) ↾}_{(R^{V})}) (g) \leftrightarrow mRSubst (T) (f) = mRSubst (T) (g))$
66	65	adantl	$⊢ (T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \to (({mRSubst (T) ↾}_{(R^{V})}) (f) = ({mRSubst (T) ↾}_{(R^{V})}) (g) \leftrightarrow mRSubst (T) (f) = mRSubst (T) (g))$
67	62 66	bitr3d	$⊢ (T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \to (f = g \leftrightarrow mRSubst (T) (f) = mRSubst (T) (g))$
68	67	adantr	$⊢ ((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \to (f = g \leftrightarrow mRSubst (T) (f) = mRSubst (T) (g))$
69	59 68	mpbird	$⊢ ((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \to f = g$
70	69	fveq1d	$⊢ ((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land (v \in V \land S (f) = S (g))) \to f (v) = g (v)$
71	70	expr	$⊢ ((T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \land v \in V) \to (S (f) = S (g) \to f (v) = g (v))$
72	71	ralrimdva	$⊢ (T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \to (S (f) = S (g) \to \forall v \in V f (v) = g (v))$
73		fvres	$⊢ f \in (R^{V}) \to ({S ↾}_{(R^{V})}) (f) = S (f)$
74		fvres	$⊢ g \in (R^{V}) \to ({S ↾}_{(R^{V})}) (g) = S (g)$
75	73 74	eqeqan12d	$⊢ (f \in (R^{V}) \land g \in (R^{V})) \to (({S ↾}_{(R^{V})}) (f) = ({S ↾}_{(R^{V})}) (g) \leftrightarrow S (f) = S (g))$
76	75	adantl	$⊢ (T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \to (({S ↾}_{(R^{V})}) (f) = ({S ↾}_{(R^{V})}) (g) \leftrightarrow S (f) = S (g))$
77		ffn	$⊢ f : V ⟶ R \to f Fn V$
78		ffn	$⊢ g : V ⟶ R \to g Fn V$
79		eqfnfv	$⊢ (f Fn V \land g Fn V) \to (f = g \leftrightarrow \forall v \in V f (v) = g (v))$
80	77 78 79	syl2an	$⊢ (f : V ⟶ R \land g : V ⟶ R) \to (f = g \leftrightarrow \forall v \in V f (v) = g (v))$
81	27 43 80	syl2an	$⊢ (f \in (R^{V}) \land g \in (R^{V})) \to (f = g \leftrightarrow \forall v \in V f (v) = g (v))$
82	81	adantl	$⊢ (T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \to (f = g \leftrightarrow \forall v \in V f (v) = g (v))$
83	72 76 82	3imtr4d	$⊢ (T \in mFS \land (f \in (R^{V}) \land g \in (R^{V}))) \to (({S ↾}_{(R^{V})}) (f) = ({S ↾}_{(R^{V})}) (g) \to f = g)$
84	83	ralrimivva	$⊢ T \in mFS \to \forall f \in (R^{V}) \forall g \in (R^{V}) (({S ↾}_{(R^{V})}) (f) = ({S ↾}_{(R^{V})}) (g) \to f = g)$
85		dff13	$⊢ ({S ↾}_{(R^{V})}) : R^{V} \underset{1-1}{⟶} E^{E} \leftrightarrow (({S ↾}_{(R^{V})}) : R^{V} ⟶ E^{E} \land \forall f \in (R^{V}) \forall g \in (R^{V}) (({S ↾}_{(R^{V})}) (f) = ({S ↾}_{(R^{V})}) (g) \to f = g))$
86	8 84 85	sylanbrc	$⊢ T \in mFS \to ({S ↾}_{(R^{V})}) : R^{V} \underset{1-1}{⟶} E^{E}$

Metamath Proof Explorer

Theorem msubff1

Proof