elmsubrn - Mathbox for Mario Carneiro

	Mathbox for Mario Carneiro		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > elmsubrn		Structured version Visualization version GIF version

Theorem elmsubrn 36020

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

**Hypotheses**
Ref	Expression
elmsubrn.e	⊢ 𝐸 = (mEx‘𝑇)
elmsubrn.o	⊢ 𝑂 = (mRSubst‘𝑇)
elmsubrn.s	⊢ 𝑆 = (mSubst‘𝑇)

**Assertion**
Ref	Expression
elmsubrn	⊢ ran 𝑆 = ran (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))

Distinct variable groups: 𝑒,𝑓,𝐸 𝑒,𝑂,𝑓 𝑇,𝑒 Allowed substitution hints: 𝑆(𝑒,𝑓) 𝑇(𝑓)

Proof of Theorem elmsubrn Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2763	. . . . . 6 ⊢ (mVR‘𝑇) = (mVR‘𝑇)
2		eqid 2763	. . . . . 6 ⊢ (mREx‘𝑇) = (mREx‘𝑇)
3		elmsubrn.s	. . . . . 6 ⊢ 𝑆 = (mSubst‘𝑇)
4		elmsubrn.e	. . . . . 6 ⊢ 𝐸 = (mEx‘𝑇)
5		elmsubrn.o	. . . . . 6 ⊢ 𝑂 = (mRSubst‘𝑇)
6	1, 2, 3, 4, 5	msubffval 36015	. . . . 5 ⊢ (𝑇 ∈ V → 𝑆 = (𝑔 ∈ ((mREx‘𝑇) ↑_pm (mVR‘𝑇)) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), ((𝑂‘𝑔)‘(2^nd ‘𝑒))⟩)))
7	1, 2, 5	mrsubff 36004	. . . . . . . 8 ⊢ (𝑇 ∈ V → 𝑂:((mREx‘𝑇) ↑_pm (mVR‘𝑇))⟶((mREx‘𝑇) ↑_m (mREx‘𝑇)))
8	7	ffnd 6706	. . . . . . 7 ⊢ (𝑇 ∈ V → 𝑂 Fn ((mREx‘𝑇) ↑_pm (mVR‘𝑇)))
9		fnfvelrn 7075	. . . . . . 7 ⊢ ((𝑂 Fn ((mREx‘𝑇) ↑_pm (mVR‘𝑇)) ∧ 𝑔 ∈ ((mREx‘𝑇) ↑_pm (mVR‘𝑇))) → (𝑂‘𝑔) ∈ ran 𝑂)
10	8, 9	sylan 591	. . . . . 6 ⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ ((mREx‘𝑇) ↑_pm (mVR‘𝑇))) → (𝑂‘𝑔) ∈ ran 𝑂)
11	7	feqmptd 6949	. . . . . 6 ⊢ (𝑇 ∈ V → 𝑂 = (𝑔 ∈ ((mREx‘𝑇) ↑_pm (mVR‘𝑇)) ↦ (𝑂‘𝑔)))
12		eqidd 2764	. . . . . 6 ⊢ (𝑇 ∈ V → (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) = (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)))
13		fveq1 6880	. . . . . . . 8 ⊢ (𝑓 = (𝑂‘𝑔) → (𝑓‘(2^nd ‘𝑒)) = ((𝑂‘𝑔)‘(2^nd ‘𝑒)))
14	13	opeq2d 4845	. . . . . . 7 ⊢ (𝑓 = (𝑂‘𝑔) → ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩ = ⟨(1^st ‘𝑒), ((𝑂‘𝑔)‘(2^nd ‘𝑒))⟩)
15	14	mpteq2dv 5205	. . . . . 6 ⊢ (𝑓 = (𝑂‘𝑔) → (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩) = (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), ((𝑂‘𝑔)‘(2^nd ‘𝑒))⟩))
16	10, 11, 12, 15	fmptco 7125	. . . . 5 ⊢ (𝑇 ∈ V → ((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) ∘ 𝑂) = (𝑔 ∈ ((mREx‘𝑇) ↑_pm (mVR‘𝑇)) ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), ((𝑂‘𝑔)‘(2^nd ‘𝑒))⟩)))
17	6, 16	eqtr4d 2801	. . . 4 ⊢ (𝑇 ∈ V → 𝑆 = ((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) ∘ 𝑂))
18	17	rneqd 5928	. . 3 ⊢ (𝑇 ∈ V → ran 𝑆 = ran ((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) ∘ 𝑂))
19		rnco 6253	. . . 4 ⊢ ran ((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) ∘ 𝑂) = ran ((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) ↾ ran 𝑂)
20		ssid 3959	. . . . . 6 ⊢ ran 𝑂 ⊆ ran 𝑂
21		resmpt 6039	. . . . . 6 ⊢ (ran 𝑂 ⊆ ran 𝑂 → ((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) ↾ ran 𝑂) = (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)))
22	20, 21	ax-mp 5	. . . . 5 ⊢ ((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) ↾ ran 𝑂) = (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))
23	22	rneqi 5927	. . . 4 ⊢ ran ((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) ↾ ran 𝑂) = ran (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))
24	19, 23	eqtri 2786	. . 3 ⊢ ran ((𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) ∘ 𝑂) = ran (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))
25	18, 24	eqtrdi 2814	. 2 ⊢ (𝑇 ∈ V → ran 𝑆 = ran (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)))
26		mpt0 6677	. . . . 5 ⊢ (𝑓 ∈ ∅ ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) = ∅
27	26	eqcomi 2772	. . . 4 ⊢ ∅ = (𝑓 ∈ ∅ ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))
28		fvprc 6873	. . . . 5 ⊢ (¬ 𝑇 ∈ V → (mSubst‘𝑇) = ∅)
29	3, 28	eqtrid 2810	. . . 4 ⊢ (¬ 𝑇 ∈ V → 𝑆 = ∅)
30	5	rnfvprc 6875	. . . . 5 ⊢ (¬ 𝑇 ∈ V → ran 𝑂 = ∅)
31	30	mpteq1d 5201	. . . 4 ⊢ (¬ 𝑇 ∈ V → (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)) = (𝑓 ∈ ∅ ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)))
32	27, 29, 31	3eqtr4a 2824	. . 3 ⊢ (¬ 𝑇 ∈ V → 𝑆 = (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)))
33	32	rneqd 5928	. 2 ⊢ (¬ 𝑇 ∈ V → ran 𝑆 = ran (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩)))
34	25, 33	pm2.61i 184	1 ⊢ ran 𝑆 = ran (𝑓 ∈ ran 𝑂 ↦ (𝑒 ∈ 𝐸 ↦ ⟨(1^st ‘𝑒), (𝑓‘(2^nd ‘𝑒))⟩))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 = wceq 1570 ∈ wcel 2143 Vcvv 3455 ⊆ wss 3905 ∅c0 4286 ⟨cop 4595 ↦ cmpt 5192 ran crn 5662 ↾ cres 5663 ∘ ccom 5665 Fn wfn 6531 ‘cfv 6536 (class class class)co 7410 1^st c1st 7980 2^nd c2nd 7981 ↑_m cmap 8820 ↑_pm cpm 8821 mVRcmvar 35953 mRExcmrex 35958 mExcmex 35959 mRSubstcmrsub 35962 mSubstcmsub 35963

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-er 8690 df-map 8822 df-pm 8823 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-card 9921 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-nn 12229 df-2 12298 df-n0 12500 df-z 12587 df-uz 12858 df-fz 13531 df-fzo 13679 df-seq 14034 df-hash 14363 df-word 14547 df-concat 14604 df-s1 14630 df-struct 17202 df-sets 17219 df-slot 17237 df-ndx 17249 df-base 17265 df-ress 17286 df-plusg 17318 df-0g 17489 df-gsum 17490 df-mgm 18693 df-sgrp 18772 df-mnd 18788 df-submnd 18837 df-frmd 18903 df-mrex 35978 df-mrsub 35982 df-msub 35983

This theorem is referenced by: msubco 36023 msubvrs 36052

W3C validator