msubrn - Mathbox for Mario Carneiro

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

Theorem msubrn 36384

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.)

**Hypotheses**
Ref	Expression
msubff.v	⊢ 𝑉 = (mVR‘𝑇)
msubff.r	⊢ 𝑅 = (mREx‘𝑇)
msubff.s	⊢ 𝑆 = (mSubst‘𝑇)

**Assertion**
Ref	Expression
msubrn	⊢ ran 𝑆 = (𝑆 “ (𝑅 ↑_m 𝑉))

Proof of Theorem msubrn Dummy variables 𝑒 𝑓 𝑔 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		msubff.v	. . . . . 6 ⊢ 𝑉 = (mVR‘𝑇)
2		msubff.r	. . . . . 6 ⊢ 𝑅 = (mREx‘𝑇)
3		msubff.s	. . . . . 6 ⊢ 𝑆 = (mSubst‘𝑇)
4		eqid 2760	. . . . . 6 ⊢ (mEx‘𝑇) = (mEx‘𝑇)
5		eqid 2760	. . . . . 6 ⊢ (mRSubst‘𝑇) = (mRSubst‘𝑇)
6	1, 2, 3, 4, 5	msubffval 36378	. . . . 5 ⊢ (𝑇 ∈ V → 𝑆 = (𝑓 ∈ (𝑅 ↑_pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2^nd ‘𝑒))⟩)))
7	6	rneqd 5921	. . . 4 ⊢ (𝑇 ∈ V → ran 𝑆 = ran (𝑓 ∈ (𝑅 ↑_pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2^nd ‘𝑒))⟩)))
8	1, 2, 5	mrsubff 36367	. . . . . . . . . 10 ⊢ (𝑇 ∈ V → (mRSubst‘𝑇):(𝑅 ↑_pm 𝑉)⟶(𝑅 ↑_m 𝑅))
9	8	adantr 486	. . . . . . . . 9 ⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑_pm 𝑉)) → (mRSubst‘𝑇):(𝑅 ↑_pm 𝑉)⟶(𝑅 ↑_m 𝑅))
10	9	ffund 6719	. . . . . . . 8 ⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑_pm 𝑉)) → Fun (mRSubst‘𝑇))
11	8	ffnd 6715	. . . . . . . . . 10 ⊢ (𝑇 ∈ V → (mRSubst‘𝑇) Fn (𝑅 ↑_pm 𝑉))
12		fnfvelrn 7085	. . . . . . . . . 10 ⊢ (((mRSubst‘𝑇) Fn (𝑅 ↑_pm 𝑉) ∧ 𝑓 ∈ (𝑅 ↑_pm 𝑉)) → ((mRSubst‘𝑇)‘𝑓) ∈ ran (mRSubst‘𝑇))
13	11, 12	sylan 592	. . . . . . . . 9 ⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑_pm 𝑉)) → ((mRSubst‘𝑇)‘𝑓) ∈ ran (mRSubst‘𝑇))
14	1, 2, 5	mrsubrn 36368	. . . . . . . . 9 ⊢ ran (mRSubst‘𝑇) = ((mRSubst‘𝑇) “ (𝑅 ↑_m 𝑉))
15	13, 14	eleqtrdi 2870	. . . . . . . 8 ⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑_pm 𝑉)) → ((mRSubst‘𝑇)‘𝑓) ∈ ((mRSubst‘𝑇) “ (𝑅 ↑_m 𝑉)))
16		fvelima 6955	. . . . . . . 8 ⊢ ((Fun (mRSubst‘𝑇) ∧ ((mRSubst‘𝑇)‘𝑓) ∈ ((mRSubst‘𝑇) “ (𝑅 ↑_m 𝑉))) → ∃𝑔 ∈ (𝑅 ↑_m 𝑉)((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓))
17	10, 15, 16	syl2anc 596	. . . . . . 7 ⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑_pm 𝑉)) → ∃𝑔 ∈ (𝑅 ↑_m 𝑉)((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓))
18		elmapi 8876	. . . . . . . . . . . . 13 ⊢ (𝑔 ∈ (𝑅 ↑_m 𝑉) → 𝑔:𝑉⟶𝑅)
19	18	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑_m 𝑉)) → 𝑔:𝑉⟶𝑅)
20		ssid 3931	. . . . . . . . . . . 12 ⊢ 𝑉 ⊆ 𝑉
21	1, 2, 3, 4, 5	msubfval 36379	. . . . . . . . . . . 12 ⊢ ((𝑔:𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉) → (𝑆‘𝑔) = (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2^nd ‘𝑒))⟩))
22	19, 20, 21	sylancl 598	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑_m 𝑉)) → (𝑆‘𝑔) = (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2^nd ‘𝑒))⟩))
23		fvex 6903	. . . . . . . . . . . . . . . 16 ⊢ (mEx‘𝑇) ∈ V
24	23	mptex 7233	. . . . . . . . . . . . . . 15 ⊢ (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2^nd ‘𝑒))⟩) ∈ V
25		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (𝑓 ∈ (𝑅 ↑_pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2^nd ‘𝑒))⟩)) = (𝑓 ∈ (𝑅 ↑_pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2^nd ‘𝑒))⟩))
26	24, 25	fnmpti 6687	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ (𝑅 ↑_pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2^nd ‘𝑒))⟩)) Fn (𝑅 ↑_pm 𝑉)
27	6	fneq1d 6637	. . . . . . . . . . . . . 14 ⊢ (𝑇 ∈ V → (𝑆 Fn (𝑅 ↑_pm 𝑉) ↔ (𝑓 ∈ (𝑅 ↑_pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2^nd ‘𝑒))⟩)) Fn (𝑅 ↑_pm 𝑉)))
28	26, 27	mpbiri 261	. . . . . . . . . . . . 13 ⊢ (𝑇 ∈ V → 𝑆 Fn (𝑅 ↑_pm 𝑉))
29	28	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑_m 𝑉)) → 𝑆 Fn (𝑅 ↑_pm 𝑉))
30		mapsspm 8911	. . . . . . . . . . . . 13 ⊢ (𝑅 ↑_m 𝑉) ⊆ (𝑅 ↑_pm 𝑉)
31	30	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑_m 𝑉)) → (𝑅 ↑_m 𝑉) ⊆ (𝑅 ↑_pm 𝑉))
32		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑_m 𝑉)) → 𝑔 ∈ (𝑅 ↑_m 𝑉))
33		fnfvima 7243	. . . . . . . . . . . 12 ⊢ ((𝑆 Fn (𝑅 ↑_pm 𝑉) ∧ (𝑅 ↑_m 𝑉) ⊆ (𝑅 ↑_pm 𝑉) ∧ 𝑔 ∈ (𝑅 ↑_m 𝑉)) → (𝑆‘𝑔) ∈ (𝑆 “ (𝑅 ↑_m 𝑉)))
34	29, 31, 32, 33	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑_m 𝑉)) → (𝑆‘𝑔) ∈ (𝑆 “ (𝑅 ↑_m 𝑉)))
35	22, 34	eqeltrrd 2861	. . . . . . . . . 10 ⊢ ((𝑇 ∈ V ∧ 𝑔 ∈ (𝑅 ↑_m 𝑉)) → (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2^nd ‘𝑒))⟩) ∈ (𝑆 “ (𝑅 ↑_m 𝑉)))
36	35	adantlr 728	. . . . . . . . 9 ⊢ (((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑_pm 𝑉)) ∧ 𝑔 ∈ (𝑅 ↑_m 𝑉)) → (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2^nd ‘𝑒))⟩) ∈ (𝑆 “ (𝑅 ↑_m 𝑉)))
37		fveq1 6889	. . . . . . . . . . . 12 ⊢ (((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → (((mRSubst‘𝑇)‘𝑔)‘(2^nd ‘𝑒)) = (((mRSubst‘𝑇)‘𝑓)‘(2^nd ‘𝑒)))
38	37	opeq2d 4846	. . . . . . . . . . 11 ⊢ (((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2^nd ‘𝑒))⟩ = ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2^nd ‘𝑒))⟩)
39	38	mpteq2dv 5198	. . . . . . . . . 10 ⊢ (((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2^nd ‘𝑒))⟩) = (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2^nd ‘𝑒))⟩))
40	39	eleq1d 2845	. . . . . . . . 9 ⊢ (((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → ((𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑔)‘(2^nd ‘𝑒))⟩) ∈ (𝑆 “ (𝑅 ↑_m 𝑉)) ↔ (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2^nd ‘𝑒))⟩) ∈ (𝑆 “ (𝑅 ↑_m 𝑉))))
41	36, 40	syl5ibcom 248	. . . . . . . 8 ⊢ (((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑_pm 𝑉)) ∧ 𝑔 ∈ (𝑅 ↑_m 𝑉)) → (((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2^nd ‘𝑒))⟩) ∈ (𝑆 “ (𝑅 ↑_m 𝑉))))
42	41	rexlimdva 3163	. . . . . . 7 ⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑_pm 𝑉)) → (∃𝑔 ∈ (𝑅 ↑_m 𝑉)((mRSubst‘𝑇)‘𝑔) = ((mRSubst‘𝑇)‘𝑓) → (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2^nd ‘𝑒))⟩) ∈ (𝑆 “ (𝑅 ↑_m 𝑉))))
43	17, 42	mpd 16	. . . . . 6 ⊢ ((𝑇 ∈ V ∧ 𝑓 ∈ (𝑅 ↑_pm 𝑉)) → (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2^nd ‘𝑒))⟩) ∈ (𝑆 “ (𝑅 ↑_m 𝑉)))
44	43	fmpttd 7120	. . . . 5 ⊢ (𝑇 ∈ V → (𝑓 ∈ (𝑅 ↑_pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2^nd ‘𝑒))⟩)):(𝑅 ↑_pm 𝑉)⟶(𝑆 “ (𝑅 ↑_m 𝑉)))
45	44	frnd 6723	. . . 4 ⊢ (𝑇 ∈ V → ran (𝑓 ∈ (𝑅 ↑_pm 𝑉) ↦ (𝑒 ∈ (mEx‘𝑇) ↦ ⟨(1^st ‘𝑒), (((mRSubst‘𝑇)‘𝑓)‘(2^nd ‘𝑒))⟩)) ⊆ (𝑆 “ (𝑅 ↑_m 𝑉)))
46	7, 45	eqsstrd 3943	. . 3 ⊢ (𝑇 ∈ V → ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑_m 𝑉)))
47	3	rnfvprc 6884	. . . 4 ⊢ (¬ 𝑇 ∈ V → ran 𝑆 = ∅)
48		0ss 4349	. . . 4 ⊢ ∅ ⊆ (𝑆 “ (𝑅 ↑_m 𝑉))
49	47, 48	eqsstrdi 3953	. . 3 ⊢ (¬ 𝑇 ∈ V → ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑_m 𝑉)))
50	46, 49	pm2.61i 184	. 2 ⊢ ran 𝑆 ⊆ (𝑆 “ (𝑅 ↑_m 𝑉))
51		imassrn 6200	. 2 ⊢ (𝑆 “ (𝑅 ↑_m 𝑉)) ⊆ ran 𝑆
52	50, 51	eqssi 3925	1 ⊢ ran 𝑆 = (𝑆 “ (𝑅 ↑_m 𝑉))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 ∧ wa 401 = wceq 1569 ∈ wcel 2144 ∃wrex 3086 Vcvv 3450 ⊆ wss 3896 ∅c0 4277 ⟨cop 4834 ↦ cmpt 5185 ran crn 5652 “ cima 5654 Fun wfun 6537 Fn wfn 6538 ⟶wf 6539 ‘cfv 6543 (class class class)co 7424 1^st c1st 8003 2^nd c2nd 8004 ↑_m cmap 8854 ↑_pm cpm 8855 mVRcmvar 36316 mRExcmrex 36321 mExcmex 36322 mRSubstcmrsub 36325 mSubstcmsub 36326

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5327 ax-pr 5391 ax-un 7755 ax-cnex 11263 ax-resscn 11264 ax-1cn 11265 ax-icn 11266 ax-addcl 11267 ax-addrcl 11268 ax-mulcl 11269 ax-mulrcl 11270 ax-mulcom 11271 ax-addass 11272 ax-mulass 11273 ax-distr 11274 ax-i2m1 11275 ax-1ne0 11276 ax-1rid 11277 ax-rnegex 11278 ax-rrecex 11279 ax-cnre 11280 ax-pre-lttri 11281 ax-pre-lttrn 11282 ax-pre-ltadd 11283 ax-pre-mulgt0 11284

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6307 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6497 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7381 df-ov 7427 df-oprab 7428 df-mpo 7429 df-om 7882 df-1st 8005 df-2nd 8006 df-frecs 8306 df-wrecs 8337 df-recs 8386 df-rdg 8425 df-1o 8483 df-er 8724 df-map 8856 df-pm 8857 df-en 8981 df-dom 8982 df-sdom 8983 df-fin 8984 df-card 10027 df-pnf 11352 df-mnf 11353 df-xr 11354 df-ltxr 11355 df-le 11356 df-sub 11550 df-neg 11551 df-nn 12343 df-2 12412 df-n0 12614 df-z 12701 df-uz 12973 df-fz 13647 df-fzo 13796 df-seq 14152 df-hash 14482 df-word 14666 df-concat 14723 df-s1 14750 df-struct 17334 df-sets 17351 df-slot 17369 df-ndx 17381 df-base 17397 df-ress 17418 df-plusg 17450 df-0g 17621 df-gsum 17622 df-mgm 18825 df-sgrp 18917 df-mnd 18933 df-submnd 18988 df-frmd 19054 df-mrex 36341 df-mrsub 36345 df-msub 36346

This theorem is used by: msubff1o 36412

W3C validator