Theorem msubff1 30707

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

Hypotheses

Ref	Expression
msubff1.v	⊢ 𝑉 = (mVR‘𝑇)
msubff1.r	⊢ 𝑅 = (mREx‘𝑇)
msubff1.s	⊢ 𝑆 = (mSubst‘𝑇)
msubff1.e	⊢ 𝐸 = (mEx‘𝑇)

Assertion

Ref	Expression
msubff1	⊢ (𝑇 ∈ mFS → (𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)–1-1→(𝐸 ↑𝑚 𝐸))

Proof of Theorem msubff1

Dummy variables 𝑓 𝑔 𝑟 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		msubff1.v	. . . 4 ⊢ 𝑉 = (mVR‘𝑇)
2		msubff1.r	. . . 4 ⊢ 𝑅 = (mREx‘𝑇)
3		msubff1.s	. . . 4 ⊢ 𝑆 = (mSubst‘𝑇)
4		msubff1.e	. . . 4 ⊢ 𝐸 = (mEx‘𝑇)
5	1, 2, 3, 4	msubff 30681	. . 3 ⊢ (𝑇 ∈ mFS → 𝑆:(𝑅 ↑pm 𝑉)⟶(𝐸 ↑𝑚 𝐸))
6		mapsspm 7777	. . . 4 ⊢ (𝑅 ↑𝑚 𝑉) ⊆ (𝑅 ↑pm 𝑉)
7	6	a1i 11	. . 3 ⊢ (𝑇 ∈ mFS → (𝑅 ↑𝑚 𝑉) ⊆ (𝑅 ↑pm 𝑉))
8	5, 7	fssresd 5984	. 2 ⊢ (𝑇 ∈ mFS → (𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)⟶(𝐸 ↑𝑚 𝐸))
9		eqid 2610	. . . . . . . . . . . . 13 ⊢ (mRSubst‘𝑇) = (mRSubst‘𝑇)
10	1, 2, 9	mrsubff 30663	. . . . . . . . . . . 12 ⊢ (𝑇 ∈ mFS → (mRSubst‘𝑇):(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅))
11	10	ad2antrr 758	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → (mRSubst‘𝑇):(𝑅 ↑pm 𝑉)⟶(𝑅 ↑𝑚 𝑅))
12		simplrl 796	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → 𝑓 ∈ (𝑅 ↑𝑚 𝑉))
13	6, 12	sseldi 3566	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → 𝑓 ∈ (𝑅 ↑pm 𝑉))
14	11, 13	ffvelrnd 6268	. . . . . . . . . 10 ⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → ((mRSubst‘𝑇)‘𝑓) ∈ (𝑅 ↑𝑚 𝑅))
15		elmapi 7765	. . . . . . . . . 10 ⊢ (((mRSubst‘𝑇)‘𝑓) ∈ (𝑅 ↑𝑚 𝑅) → ((mRSubst‘𝑇)‘𝑓):𝑅⟶𝑅)
16		ffn 5958	. . . . . . . . . 10 ⊢ (((mRSubst‘𝑇)‘𝑓):𝑅⟶𝑅 → ((mRSubst‘𝑇)‘𝑓) Fn 𝑅)
17	14, 15, 16	3syl 18	. . . . . . . . 9 ⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → ((mRSubst‘𝑇)‘𝑓) Fn 𝑅)
18		simplrr 797	. . . . . . . . . . . 12 ⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → 𝑔 ∈ (𝑅 ↑𝑚 𝑉))
19	6, 18	sseldi 3566	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → 𝑔 ∈ (𝑅 ↑pm 𝑉))
20	11, 19	ffvelrnd 6268	. . . . . . . . . 10 ⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → ((mRSubst‘𝑇)‘𝑔) ∈ (𝑅 ↑𝑚 𝑅))
21		elmapi 7765	. . . . . . . . . 10 ⊢ (((mRSubst‘𝑇)‘𝑔) ∈ (𝑅 ↑𝑚 𝑅) → ((mRSubst‘𝑇)‘𝑔):𝑅⟶𝑅)
22		ffn 5958	. . . . . . . . . 10 ⊢ (((mRSubst‘𝑇)‘𝑔):𝑅⟶𝑅 → ((mRSubst‘𝑇)‘𝑔) Fn 𝑅)
23	20, 21, 22	3syl 18	. . . . . . . . 9 ⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → ((mRSubst‘𝑇)‘𝑔) Fn 𝑅)
24		simplrr 797	. . . . . . . . . . . . 13 ⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → (𝑆‘𝑓) = (𝑆‘𝑔))
25	24	fveq1d 6105	. . . . . . . . . . . 12 ⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → ((𝑆‘𝑓)‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩) = ((𝑆‘𝑔)‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩))
26	12	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → 𝑓 ∈ (𝑅 ↑𝑚 𝑉))
27		elmapi 7765	. . . . . . . . . . . . . 14 ⊢ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) → 𝑓:𝑉⟶𝑅)
28	26, 27	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → 𝑓:𝑉⟶𝑅)
29		ssid 3587	. . . . . . . . . . . . . 14 ⊢ 𝑉 ⊆ 𝑉
30	29	a1i 11	. . . . . . . . . . . . 13 ⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → 𝑉 ⊆ 𝑉)
31		eqid 2610	. . . . . . . . . . . . . . . . . 18 ⊢ (mTC‘𝑇) = (mTC‘𝑇)
32		eqid 2610	. . . . . . . . . . . . . . . . . 18 ⊢ (mType‘𝑇) = (mType‘𝑇)
33	1, 31, 32	mtyf2 30702	. . . . . . . . . . . . . . . . 17 ⊢ (𝑇 ∈ mFS → (mType‘𝑇):𝑉⟶(mTC‘𝑇))
34	33	ad3antrrr 762	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → (mType‘𝑇):𝑉⟶(mTC‘𝑇))
35		simplrl 796	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → 𝑣 ∈ 𝑉)
36	34, 35	ffvelrnd 6268	. . . . . . . . . . . . . . 15 ⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → ((mType‘𝑇)‘𝑣) ∈ (mTC‘𝑇))
37		opelxpi 5072	. . . . . . . . . . . . . . 15 ⊢ ((((mType‘𝑇)‘𝑣) ∈ (mTC‘𝑇) ∧ 𝑟 ∈ 𝑅) → ⟨((mType‘𝑇)‘𝑣), 𝑟⟩ ∈ ((mTC‘𝑇) × 𝑅))
38	36, 37	sylancom 698	. . . . . . . . . . . . . 14 ⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → ⟨((mType‘𝑇)‘𝑣), 𝑟⟩ ∈ ((mTC‘𝑇) × 𝑅))
39	31, 4, 2	mexval 30653	. . . . . . . . . . . . . 14 ⊢ 𝐸 = ((mTC‘𝑇) × 𝑅)
40	38, 39	syl6eleqr 2699	. . . . . . . . . . . . 13 ⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → ⟨((mType‘𝑇)‘𝑣), 𝑟⟩ ∈ 𝐸)
41	1, 2, 3, 4, 9	msubval 30676	. . . . . . . . . . . . 13 ⊢ ((𝑓:𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉 ∧ ⟨((mType‘𝑇)‘𝑣), 𝑟⟩ ∈ 𝐸) → ((𝑆‘𝑓)‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩) = ⟨(1st ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩))⟩)
42	28, 30, 40, 41	syl3anc 1318	. . . . . . . . . . . 12 ⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → ((𝑆‘𝑓)‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩) = ⟨(1st ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩))⟩)
43	18	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → 𝑔 ∈ (𝑅 ↑𝑚 𝑉))
44		elmapi 7765	. . . . . . . . . . . . . 14 ⊢ (𝑔 ∈ (𝑅 ↑𝑚 𝑉) → 𝑔:𝑉⟶𝑅)
45	43, 44	syl 17	. . . . . . . . . . . . 13 ⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → 𝑔:𝑉⟶𝑅)
46	1, 2, 3, 4, 9	msubval 30676	. . . . . . . . . . . . 13 ⊢ ((𝑔:𝑉⟶𝑅 ∧ 𝑉 ⊆ 𝑉 ∧ ⟨((mType‘𝑇)‘𝑣), 𝑟⟩ ∈ 𝐸) → ((𝑆‘𝑔)‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩) = ⟨(1st ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩))⟩)
47	45, 30, 40, 46	syl3anc 1318	. . . . . . . . . . . 12 ⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → ((𝑆‘𝑔)‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩) = ⟨(1st ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩))⟩)
48	25, 42, 47	3eqtr3d 2652	. . . . . . . . . . 11 ⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → ⟨(1st ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩))⟩ = ⟨(1st ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩))⟩)
49		fvex 6113	. . . . . . . . . . . . 13 ⊢ (1st ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩) ∈ V
50		fvex 6113	. . . . . . . . . . . . 13 ⊢ (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩)) ∈ V
51	49, 50	opth 4871	. . . . . . . . . . . 12 ⊢ (⟨(1st ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩))⟩ = ⟨(1st ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩))⟩ ↔ ((1st ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩) = (1st ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩) ∧ (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩)) = (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩))))
52	51	simprbi 479	. . . . . . . . . . 11 ⊢ (⟨(1st ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩), (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩))⟩ = ⟨(1st ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩), (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩))⟩ → (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩)) = (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩)))
53	48, 52	syl 17	. . . . . . . . . 10 ⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩)) = (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩)))
54		fvex 6113	. . . . . . . . . . . 12 ⊢ ((mType‘𝑇)‘𝑣) ∈ V
55		vex 3176	. . . . . . . . . . . 12 ⊢ 𝑟 ∈ V
56	54, 55	op2nd 7068	. . . . . . . . . . 11 ⊢ (2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩) = 𝑟
57	56	fveq2i 6106	. . . . . . . . . 10 ⊢ (((mRSubst‘𝑇)‘𝑓)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩)) = (((mRSubst‘𝑇)‘𝑓)‘𝑟)
58	56	fveq2i 6106	. . . . . . . . . 10 ⊢ (((mRSubst‘𝑇)‘𝑔)‘(2nd ‘⟨((mType‘𝑇)‘𝑣), 𝑟⟩)) = (((mRSubst‘𝑇)‘𝑔)‘𝑟)
59	53, 57, 58	3eqtr3g 2667	. . . . . . . . 9 ⊢ ((((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) ∧ 𝑟 ∈ 𝑅) → (((mRSubst‘𝑇)‘𝑓)‘𝑟) = (((mRSubst‘𝑇)‘𝑔)‘𝑟))
60	17, 23, 59	eqfnfvd 6222	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → ((mRSubst‘𝑇)‘𝑓) = ((mRSubst‘𝑇)‘𝑔))
61	1, 2, 9	mrsubff1 30665	. . . . . . . . . . 11 ⊢ (𝑇 ∈ mFS → ((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)–1-1→(𝑅 ↑𝑚 𝑅))
62		f1fveq 6420	. . . . . . . . . . 11 ⊢ ((((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)–1-1→(𝑅 ↑𝑚 𝑅) ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) → ((((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = (((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) ↔ 𝑓 = 𝑔))
63	61, 62	sylan 487	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) → ((((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = (((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) ↔ 𝑓 = 𝑔))
64		fvres 6117	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) → (((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = ((mRSubst‘𝑇)‘𝑓))
65		fvres 6117	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ (𝑅 ↑𝑚 𝑉) → (((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) = ((mRSubst‘𝑇)‘𝑔))
66	64, 65	eqeqan12d 2626	. . . . . . . . . . 11 ⊢ ((𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) → ((((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = (((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) ↔ ((mRSubst‘𝑇)‘𝑓) = ((mRSubst‘𝑇)‘𝑔)))
67	66	adantl 481	. . . . . . . . . 10 ⊢ ((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) → ((((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = (((mRSubst‘𝑇) ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) ↔ ((mRSubst‘𝑇)‘𝑓) = ((mRSubst‘𝑇)‘𝑔)))
68	63, 67	bitr3d 269	. . . . . . . . 9 ⊢ ((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑓 = 𝑔 ↔ ((mRSubst‘𝑇)‘𝑓) = ((mRSubst‘𝑇)‘𝑔)))
69	68	adantr 480	. . . . . . . 8 ⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → (𝑓 = 𝑔 ↔ ((mRSubst‘𝑇)‘𝑓) = ((mRSubst‘𝑇)‘𝑔)))
70	60, 69	mpbird 246	. . . . . . 7 ⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → 𝑓 = 𝑔)
71	70	fveq1d 6105	. . . . . 6 ⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ (𝑣 ∈ 𝑉 ∧ (𝑆‘𝑓) = (𝑆‘𝑔))) → (𝑓‘𝑣) = (𝑔‘𝑣))
72	71	expr 641	. . . . 5 ⊢ (((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) ∧ 𝑣 ∈ 𝑉) → ((𝑆‘𝑓) = (𝑆‘𝑔) → (𝑓‘𝑣) = (𝑔‘𝑣)))
73	72	ralrimdva 2952	. . . 4 ⊢ ((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) → ((𝑆‘𝑓) = (𝑆‘𝑔) → ∀𝑣 ∈ 𝑉 (𝑓‘𝑣) = (𝑔‘𝑣)))
74		fvres 6117	. . . . . 6 ⊢ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) → ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = (𝑆‘𝑓))
75		fvres 6117	. . . . . 6 ⊢ (𝑔 ∈ (𝑅 ↑𝑚 𝑉) → ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) = (𝑆‘𝑔))
76	74, 75	eqeqan12d 2626	. . . . 5 ⊢ ((𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) → (((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) ↔ (𝑆‘𝑓) = (𝑆‘𝑔)))
77	76	adantl 481	. . . 4 ⊢ ((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) → (((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) ↔ (𝑆‘𝑓) = (𝑆‘𝑔)))
78		ffn 5958	. . . . . . 7 ⊢ (𝑓:𝑉⟶𝑅 → 𝑓 Fn 𝑉)
79		ffn 5958	. . . . . . 7 ⊢ (𝑔:𝑉⟶𝑅 → 𝑔 Fn 𝑉)
80		eqfnfv 6219	. . . . . . 7 ⊢ ((𝑓 Fn 𝑉 ∧ 𝑔 Fn 𝑉) → (𝑓 = 𝑔 ↔ ∀𝑣 ∈ 𝑉 (𝑓‘𝑣) = (𝑔‘𝑣)))
81	78, 79, 80	syl2an 493	. . . . . 6 ⊢ ((𝑓:𝑉⟶𝑅 ∧ 𝑔:𝑉⟶𝑅) → (𝑓 = 𝑔 ↔ ∀𝑣 ∈ 𝑉 (𝑓‘𝑣) = (𝑔‘𝑣)))
82	27, 44, 81	syl2an 493	. . . . 5 ⊢ ((𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉)) → (𝑓 = 𝑔 ↔ ∀𝑣 ∈ 𝑉 (𝑓‘𝑣) = (𝑔‘𝑣)))
83	82	adantl 481	. . . 4 ⊢ ((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) → (𝑓 = 𝑔 ↔ ∀𝑣 ∈ 𝑉 (𝑓‘𝑣) = (𝑔‘𝑣)))
84	73, 77, 83	3imtr4d 282	. . 3 ⊢ ((𝑇 ∈ mFS ∧ (𝑓 ∈ (𝑅 ↑𝑚 𝑉) ∧ 𝑔 ∈ (𝑅 ↑𝑚 𝑉))) → (((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) → 𝑓 = 𝑔))
85	84	ralrimivva 2954	. 2 ⊢ (𝑇 ∈ mFS → ∀𝑓 ∈ (𝑅 ↑𝑚 𝑉)∀𝑔 ∈ (𝑅 ↑𝑚 𝑉)(((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) → 𝑓 = 𝑔))
86		dff13 6416	. 2 ⊢ ((𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)–1-1→(𝐸 ↑𝑚 𝐸) ↔ ((𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)⟶(𝐸 ↑𝑚 𝐸) ∧ ∀𝑓 ∈ (𝑅 ↑𝑚 𝑉)∀𝑔 ∈ (𝑅 ↑𝑚 𝑉)(((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑓) = ((𝑆 ↾ (𝑅 ↑𝑚 𝑉))‘𝑔) → 𝑓 = 𝑔)))
87	8, 85, 86	sylanbrc 695	1 ⊢ (𝑇 ∈ mFS → (𝑆 ↾ (𝑅 ↑𝑚 𝑉)):(𝑅 ↑𝑚 𝑉)–1-1→(𝐸 ↑𝑚 𝐸))

Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896   ⊆ wss 3540  ⟨cop 4131   × cxp 5036   ↾ cres 5040   Fn wfn 5799  ⟶wf 5800  –1-1→wf1 5801  ‘cfv 5804  (class class class)co 6549  1^st c1st 7057  2^nd c2nd 7058   ↑_𝑚 cmap 7744   ↑_pm cpm 7745  mVRcmvar 30612  mTypecmty 30613  mTCcmtc 30615  mRExcmrex 30617  mExcmex 30618  mRSubstcmrsub 30621  mSubstcmsub 30622  mFScmfs 30627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-seq 12664  df-hash 12980  df-word 13154  df-concat 13156  df-s1 13157  df-struct 15697  df-ndx 15698  df-slot 15699  df-base 15700  df-sets 15701  df-ress 15702  df-plusg 15781  df-0g 15925  df-gsum 15926  df-mgm 17065  df-sgrp 17107  df-mnd 17118  df-submnd 17159  df-frmd 17209  df-mrex 30637  df-mex 30638  df-mrsub 30641  df-msub 30642  df-mfs 30647

This theorem is referenced by:  msubff1o  30708