elmsubrn

Description: Characterization of substitution in terms of raw substitution, without reference to the generating functions. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	elmsubrn.e	$⊢ E = mEx (T)$
	elmsubrn.o	$⊢ O = mRSubst (T)$
	elmsubrn.s	$⊢ S = mSubst (T)$
Assertion	elmsubrn	$⊢ ran S = ran (f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩))$

Proof

Step	Hyp	Ref	Expression
1		elmsubrn.e	$⊢ E = mEx (T)$
2		elmsubrn.o	$⊢ O = mRSubst (T)$
3		elmsubrn.s	$⊢ S = mSubst (T)$
4		eqid	$⊢ mVR (T) = mVR (T)$
5		eqid	$⊢ mREx (T) = mREx (T)$
6	4 5 3 1 2	msubffval	$⊢ T \in V \to S = (g \in (mREx (T) ↑_{𝑝𝑚} mVR (T)) ⟼ (e \in E ⟼ ⟨1^{st} (e), O (g) (2^{nd} (e))⟩))$
7	4 5 2	mrsubff	$⊢ T \in V \to O : mREx (T) ↑_{𝑝𝑚} mVR (T) ⟶ {mREx (T)}^{mREx (T)}$
8	7	ffnd	$⊢ T \in V \to O Fn (mREx (T) ↑_{𝑝𝑚} mVR (T))$
9		fnfvelrn	$⊢ (O Fn (mREx (T) ↑_{𝑝𝑚} mVR (T)) \land g \in (mREx (T) ↑_{𝑝𝑚} mVR (T))) \to O (g) \in ran O$
10	8 9	sylan	$⊢ (T \in V \land g \in (mREx (T) ↑_{𝑝𝑚} mVR (T))) \to O (g) \in ran O$
11	7	feqmptd	$⊢ T \in V \to O = (g \in (mREx (T) ↑_{𝑝𝑚} mVR (T)) ⟼ O (g))$
12		eqidd	$⊢ T \in V \to (f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩)) = (f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩))$
13		fveq1	$⊢ f = O (g) \to f (2^{nd} (e)) = O (g) (2^{nd} (e))$
14	13	opeq2d	$⊢ f = O (g) \to ⟨1^{st} (e), f (2^{nd} (e))⟩ = ⟨1^{st} (e), O (g) (2^{nd} (e))⟩$
15	14	mpteq2dv	$⊢ f = O (g) \to (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩) = (e \in E ⟼ ⟨1^{st} (e), O (g) (2^{nd} (e))⟩)$
16	10 11 12 15	fmptco	$⊢ T \in V \to (f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩)) \circ O = (g \in (mREx (T) ↑_{𝑝𝑚} mVR (T)) ⟼ (e \in E ⟼ ⟨1^{st} (e), O (g) (2^{nd} (e))⟩))$
17	6 16	eqtr4d	$⊢ T \in V \to S = (f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩)) \circ O$
18	17	rneqd	$⊢ T \in V \to ran S = ran ((f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩)) \circ O)$
19		rnco	$⊢ ran ((f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩)) \circ O) = ran ({(f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩)) ↾}_{ran O})$
20		ssid	$⊢ ran O \subseteq ran O$
21		resmpt	$⊢ ran O \subseteq ran O \to {(f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩)) ↾}_{ran O} = (f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩))$
22	20 21	ax-mp	$⊢ {(f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩)) ↾}_{ran O} = (f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩))$
23	22	rneqi	$⊢ ran ({(f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩)) ↾}_{ran O}) = ran (f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩))$
24	19 23	eqtri	$⊢ ran ((f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩)) \circ O) = ran (f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩))$
25	18 24	eqtrdi	$⊢ T \in V \to ran S = ran (f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩))$
26		mpt0	$⊢ (f \in \emptyset ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩)) = \emptyset$
27	26	eqcomi	$⊢ \emptyset = (f \in \emptyset ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩))$
28		fvprc	$⊢ \neg T \in V \to mSubst (T) = \emptyset$
29	3 28	syl5eq	$⊢ \neg T \in V \to S = \emptyset$
30	2	rnfvprc	$⊢ \neg T \in V \to ran O = \emptyset$
31	30	mpteq1d	$⊢ \neg T \in V \to (f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩)) = (f \in \emptyset ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩))$
32	27 29 31	3eqtr4a	$⊢ \neg T \in V \to S = (f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩))$
33	32	rneqd	$⊢ \neg T \in V \to ran S = ran (f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩))$
34	25 33	pm2.61i	$⊢ ran S = ran (f \in ran O ⟼ (e \in E ⟼ ⟨1^{st} (e), f (2^{nd} (e))⟩))$

Metamath Proof Explorer

Theorem elmsubrn

Proof