Theorem mrsubff1

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

	Ref	Expression
Hypotheses	mrsubvr.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	mrsubvr.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
	mrsubvr.s	⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
Assertion	mrsubff1	⊢ ( 𝑇 ∈ 𝑊 → ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1→ ( 𝑅 ↑m 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		mrsubvr.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
2		mrsubvr.r	⊢ 𝑅 = ( mREx ‘ 𝑇 )
3		mrsubvr.s	⊢ 𝑆 = ( mRSubst ‘ 𝑇 )
4	1 2 3	mrsubff	⊢ ( 𝑇 ∈ 𝑊 → 𝑆 : ( 𝑅 ↑pm 𝑉 ) ⟶ ( 𝑅 ↑m 𝑅 ) )
5		mapsspm	⊢ ( 𝑅 ↑m 𝑉 ) ⊆ ( 𝑅 ↑pm 𝑉 )
6	5	a1i	⊢ ( 𝑇 ∈ 𝑊 → ( 𝑅 ↑m 𝑉 ) ⊆ ( 𝑅 ↑pm 𝑉 ) )
7	4 6	fssresd	⊢ ( 𝑇 ∈ 𝑊 → ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) ⟶ ( 𝑅 ↑m 𝑅 ) )
8		fveq1	⊢ ( ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) → ( ( 𝑆 ‘ 𝑓 ) ‘ ⟨“ 𝑣 ”⟩ ) = ( ( 𝑆 ‘ 𝑔 ) ‘ ⟨“ 𝑣 ”⟩ ) )
9		simplrl	⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) )
10		elmapi	⊢ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) → 𝑓 : 𝑉 ⟶ 𝑅 )
11	9 10	syl	⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑓 : 𝑉 ⟶ 𝑅 )
12		ssidd	⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑉 ⊆ 𝑉 )
13		simpr	⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
14	1 2 3	mrsubvr	⊢ ( ( 𝑓 : 𝑉 ⟶ 𝑅 ∧ 𝑉 ⊆ 𝑉 ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑆 ‘ 𝑓 ) ‘ ⟨“ 𝑣 ”⟩ ) = ( 𝑓 ‘ 𝑣 ) )
15	11 12 13 14	syl3anc	⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑆 ‘ 𝑓 ) ‘ ⟨“ 𝑣 ”⟩ ) = ( 𝑓 ‘ 𝑣 ) )
16		simplrr	⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) )
17		elmapi	⊢ ( 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) → 𝑔 : 𝑉 ⟶ 𝑅 )
18	16 17	syl	⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → 𝑔 : 𝑉 ⟶ 𝑅 )
19	1 2 3	mrsubvr	⊢ ( ( 𝑔 : 𝑉 ⟶ 𝑅 ∧ 𝑉 ⊆ 𝑉 ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑆 ‘ 𝑔 ) ‘ ⟨“ 𝑣 ”⟩ ) = ( 𝑔 ‘ 𝑣 ) )
20	18 12 13 19	syl3anc	⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑆 ‘ 𝑔 ) ‘ ⟨“ 𝑣 ”⟩ ) = ( 𝑔 ‘ 𝑣 ) )
21	15 20	eqeq12d	⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( ( 𝑆 ‘ 𝑓 ) ‘ ⟨“ 𝑣 ”⟩ ) = ( ( 𝑆 ‘ 𝑔 ) ‘ ⟨“ 𝑣 ”⟩ ) ↔ ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) )
22	8 21	imbitrid	⊢ ( ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) ∧ 𝑣 ∈ 𝑉 ) → ( ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) → ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) )
23	22	ralrimdva	⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) → ∀ 𝑣 ∈ 𝑉 ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) )
24		fvres	⊢ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) → ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( 𝑆 ‘ 𝑓 ) )
25		fvres	⊢ ( 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) → ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) = ( 𝑆 ‘ 𝑔 ) )
26	24 25	eqeqan12d	⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) ↔ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) )
27	26	adantl	⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) ↔ ( 𝑆 ‘ 𝑓 ) = ( 𝑆 ‘ 𝑔 ) ) )
28		ffn	⊢ ( 𝑓 : 𝑉 ⟶ 𝑅 → 𝑓 Fn 𝑉 )
29		ffn	⊢ ( 𝑔 : 𝑉 ⟶ 𝑅 → 𝑔 Fn 𝑉 )
30		eqfnfv	⊢ ( ( 𝑓 Fn 𝑉 ∧ 𝑔 Fn 𝑉 ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑣 ∈ 𝑉 ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) )
31	28 29 30	syl2an	⊢ ( ( 𝑓 : 𝑉 ⟶ 𝑅 ∧ 𝑔 : 𝑉 ⟶ 𝑅 ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑣 ∈ 𝑉 ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) )
32	10 17 31	syl2an	⊢ ( ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑣 ∈ 𝑉 ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) )
33	32	adantl	⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( 𝑓 = 𝑔 ↔ ∀ 𝑣 ∈ 𝑉 ( 𝑓 ‘ 𝑣 ) = ( 𝑔 ‘ 𝑣 ) ) )
34	23 27 33	3imtr4d	⊢ ( ( 𝑇 ∈ 𝑊 ∧ ( 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∧ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ) ) → ( ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) → 𝑓 = 𝑔 ) )
35	34	ralrimivva	⊢ ( 𝑇 ∈ 𝑊 → ∀ 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∀ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ( ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) → 𝑓 = 𝑔 ) )
36		dff13	⊢ ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1→ ( 𝑅 ↑m 𝑅 ) ↔ ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) ⟶ ( 𝑅 ↑m 𝑅 ) ∧ ∀ 𝑓 ∈ ( 𝑅 ↑m 𝑉 ) ∀ 𝑔 ∈ ( 𝑅 ↑m 𝑉 ) ( ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑓 ) = ( ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) ‘ 𝑔 ) → 𝑓 = 𝑔 ) ) )
37	7 35 36	sylanbrc	⊢ ( 𝑇 ∈ 𝑊 → ( 𝑆 ↾ ( 𝑅 ↑m 𝑉 ) ) : ( 𝑅 ↑m 𝑉 ) –1-1→ ( 𝑅 ↑m 𝑅 ) )