msubrn

Description: Although it is defined for partial mappings of variables, every partial substitution is a substitution on some complete mapping of the variables. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	msubff.v	$⊢ V = mVR (T)$
	msubff.r	$⊢ R = mREx (T)$
	msubff.s	$⊢ S = mSubst (T)$
Assertion	msubrn	$⊢ ran S = S [R^{V}]$

Proof

Step	Hyp	Ref	Expression
1		msubff.v	$⊢ V = mVR (T)$
2		msubff.r	$⊢ R = mREx (T)$
3		msubff.s	$⊢ S = mSubst (T)$
4		eqid	$⊢ mEx (T) = mEx (T)$
5		eqid	$⊢ mRSubst (T) = mRSubst (T)$
6	1 2 3 4 5	msubffval	$⊢ T \in V \to S = (f \in (R ↑_{𝑝𝑚} V) ⟼ (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (f) (2^{nd} (e))⟩))$
7	6	rneqd	$⊢ T \in V \to ran S = ran (f \in (R ↑_{𝑝𝑚} V) ⟼ (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (f) (2^{nd} (e))⟩))$
8	1 2 5	mrsubff	$⊢ T \in V \to mRSubst (T) : R ↑_{𝑝𝑚} V ⟶ R^{R}$
9	8	adantr	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to mRSubst (T) : R ↑_{𝑝𝑚} V ⟶ R^{R}$
10	9	ffund	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to Fun mRSubst (T)$
11	8	ffnd	$⊢ T \in V \to mRSubst (T) Fn (R ↑_{𝑝𝑚} V)$
12		fnfvelrn	$⊢ (mRSubst (T) Fn (R ↑_{𝑝𝑚} V) \land f \in (R ↑_{𝑝𝑚} V)) \to mRSubst (T) (f) \in ran mRSubst (T)$
13	11 12	sylan	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to mRSubst (T) (f) \in ran mRSubst (T)$
14	1 2 5	mrsubrn	$⊢ ran mRSubst (T) = mRSubst (T) [R^{V}]$
15	13 14	eleqtrdi	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to mRSubst (T) (f) \in mRSubst (T) [R^{V}]$
16		fvelima	$⊢ (Fun mRSubst (T) \land mRSubst (T) (f) \in mRSubst (T) [R^{V}]) \to \exists g \in (R^{V}) mRSubst (T) (g) = mRSubst (T) (f)$
17	10 15 16	syl2anc	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to \exists g \in (R^{V}) mRSubst (T) (g) = mRSubst (T) (f)$
18		elmapi	$⊢ g \in (R^{V}) \to g : V ⟶ R$
19	18	adantl	$⊢ (T \in V \land g \in (R^{V})) \to g : V ⟶ R$
20		ssid	$⊢ V \subseteq V$
21	1 2 3 4 5	msubfval	$⊢ (g : V ⟶ R \land V \subseteq V) \to S (g) = (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (g) (2^{nd} (e))⟩)$
22	19 20 21	sylancl	$⊢ (T \in V \land g \in (R^{V})) \to S (g) = (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (g) (2^{nd} (e))⟩)$
23		fvex	$⊢ mEx (T) \in V$
24	23	mptex	$⊢ (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (f) (2^{nd} (e))⟩) \in V$
25		eqid	$⊢ (f \in (R ↑_{𝑝𝑚} V) ⟼ (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (f) (2^{nd} (e))⟩)) = (f \in (R ↑_{𝑝𝑚} V) ⟼ (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (f) (2^{nd} (e))⟩))$
26	24 25	fnmpti	$⊢ (f \in (R ↑_{𝑝𝑚} V) ⟼ (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (f) (2^{nd} (e))⟩)) Fn (R ↑_{𝑝𝑚} V)$
27	6	fneq1d	$⊢ T \in V \to (S Fn (R ↑_{𝑝𝑚} V) \leftrightarrow (f \in (R ↑_{𝑝𝑚} V) ⟼ (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (f) (2^{nd} (e))⟩)) Fn (R ↑_{𝑝𝑚} V))$
28	26 27	mpbiri	$⊢ T \in V \to S Fn (R ↑_{𝑝𝑚} V)$
29	28	adantr	$⊢ (T \in V \land g \in (R^{V})) \to S Fn (R ↑_{𝑝𝑚} V)$
30		mapsspm	$⊢ R^{V} \subseteq R ↑_{𝑝𝑚} V$
31	30	a1i	$⊢ (T \in V \land g \in (R^{V})) \to R^{V} \subseteq R ↑_{𝑝𝑚} V$
32		simpr	$⊢ (T \in V \land g \in (R^{V})) \to g \in (R^{V})$
33		fnfvima	$⊢ (S Fn (R ↑_{𝑝𝑚} V) \land R^{V} \subseteq R ↑_{𝑝𝑚} V \land g \in (R^{V})) \to S (g) \in S [R^{V}]$
34	29 31 32 33	syl3anc	$⊢ (T \in V \land g \in (R^{V})) \to S (g) \in S [R^{V}]$
35	22 34	eqeltrrd	$⊢ (T \in V \land g \in (R^{V})) \to (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (g) (2^{nd} (e))⟩) \in S [R^{V}]$
36	35	adantlr	$⊢ ((T \in V \land f \in (R ↑_{𝑝𝑚} V)) \land g \in (R^{V})) \to (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (g) (2^{nd} (e))⟩) \in S [R^{V}]$
37		fveq1	$⊢ mRSubst (T) (g) = mRSubst (T) (f) \to mRSubst (T) (g) (2^{nd} (e)) = mRSubst (T) (f) (2^{nd} (e))$
38	37	opeq2d	$⊢ mRSubst (T) (g) = mRSubst (T) (f) \to ⟨1^{st} (e), mRSubst (T) (g) (2^{nd} (e))⟩ = ⟨1^{st} (e), mRSubst (T) (f) (2^{nd} (e))⟩$
39	38	mpteq2dv	$⊢ mRSubst (T) (g) = mRSubst (T) (f) \to (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (g) (2^{nd} (e))⟩) = (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (f) (2^{nd} (e))⟩)$
40	39	eleq1d	$⊢ mRSubst (T) (g) = mRSubst (T) (f) \to ((e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (g) (2^{nd} (e))⟩) \in S [R^{V}] \leftrightarrow (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (f) (2^{nd} (e))⟩) \in S [R^{V}])$
41	36 40	syl5ibcom	$⊢ ((T \in V \land f \in (R ↑_{𝑝𝑚} V)) \land g \in (R^{V})) \to (mRSubst (T) (g) = mRSubst (T) (f) \to (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (f) (2^{nd} (e))⟩) \in S [R^{V}])$
42	41	rexlimdva	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to (\exists g \in (R^{V}) mRSubst (T) (g) = mRSubst (T) (f) \to (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (f) (2^{nd} (e))⟩) \in S [R^{V}])$
43	17 42	mpd	$⊢ (T \in V \land f \in (R ↑_{𝑝𝑚} V)) \to (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (f) (2^{nd} (e))⟩) \in S [R^{V}]$
44	43	fmpttd	$⊢ T \in V \to (f \in (R ↑_{𝑝𝑚} V) ⟼ (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (f) (2^{nd} (e))⟩)) : R ↑_{𝑝𝑚} V ⟶ S [R^{V}]$
45	44	frnd	$⊢ T \in V \to ran (f \in (R ↑_{𝑝𝑚} V) ⟼ (e \in mEx (T) ⟼ ⟨1^{st} (e), mRSubst (T) (f) (2^{nd} (e))⟩)) \subseteq S [R^{V}]$
46	7 45	eqsstrd	$⊢ T \in V \to ran S \subseteq S [R^{V}]$
47	3	rnfvprc	$⊢ \neg T \in V \to ran S = \emptyset$
48		0ss	$⊢ \emptyset \subseteq S [R^{V}]$
49	47 48	eqsstrdi	$⊢ \neg T \in V \to ran S \subseteq S [R^{V}]$
50	46 49	pm2.61i	$⊢ ran S \subseteq S [R^{V}]$
51		imassrn	$⊢ S [R^{V}] \subseteq ran S$
52	50 51	eqssi	$⊢ ran S = S [R^{V}]$

Metamath Proof Explorer

Theorem msubrn

Proof