Theorem mvhf1

Description: The function mapping variables to variable expressions is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016)

	Ref	Expression
Hypotheses	mvhf.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
	mvhf.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
	mvhf.h	⊢ 𝐻 = ( mVH ‘ 𝑇 )
Assertion	mvhf1	⊢ ( 𝑇 ∈ mFS → 𝐻 : 𝑉 –1-1→ 𝐸 )

Proof

Step	Hyp	Ref	Expression
1		mvhf.v	⊢ 𝑉 = ( mVR ‘ 𝑇 )
2		mvhf.e	⊢ 𝐸 = ( mEx ‘ 𝑇 )
3		mvhf.h	⊢ 𝐻 = ( mVH ‘ 𝑇 )
4	1 2 3	mvhf	⊢ ( 𝑇 ∈ mFS → 𝐻 : 𝑉 ⟶ 𝐸 )
5		eqid	⊢ ( mType ‘ 𝑇 ) = ( mType ‘ 𝑇 )
6	1 5 3	mvhval	⊢ ( 𝑣 ∈ 𝑉 → ( 𝐻 ‘ 𝑣 ) = ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ )
7	1 5 3	mvhval	⊢ ( 𝑤 ∈ 𝑉 → ( 𝐻 ‘ 𝑤 ) = ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑤 ) , ⟨“ 𝑤 ”⟩ ⟩ )
8	6 7	eqeqan12d	⊢ ( ( 𝑣 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉 ) → ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) ↔ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ = ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑤 ) , ⟨“ 𝑤 ”⟩ ⟩ ) )
9	8	adantl	⊢ ( ( 𝑇 ∈ mFS ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉 ) ) → ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) ↔ ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ = ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑤 ) , ⟨“ 𝑤 ”⟩ ⟩ ) )
10		fvex	⊢ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) ∈ V
11		s1cli	⊢ ⟨“ 𝑣 ”⟩ ∈ Word V
12	11	elexi	⊢ ⟨“ 𝑣 ”⟩ ∈ V
13	10 12	opth	⊢ ( ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ = ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑤 ) , ⟨“ 𝑤 ”⟩ ⟩ ↔ ( ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) = ( ( mType ‘ 𝑇 ) ‘ 𝑤 ) ∧ ⟨“ 𝑣 ”⟩ = ⟨“ 𝑤 ”⟩ ) )
14	13	simprbi	⊢ ( ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ = ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑤 ) , ⟨“ 𝑤 ”⟩ ⟩ → ⟨“ 𝑣 ”⟩ = ⟨“ 𝑤 ”⟩ )
15		s111	⊢ ( ( 𝑣 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉 ) → ( ⟨“ 𝑣 ”⟩ = ⟨“ 𝑤 ”⟩ ↔ 𝑣 = 𝑤 ) )
16	15	adantl	⊢ ( ( 𝑇 ∈ mFS ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉 ) ) → ( ⟨“ 𝑣 ”⟩ = ⟨“ 𝑤 ”⟩ ↔ 𝑣 = 𝑤 ) )
17	14 16	syl5ib	⊢ ( ( 𝑇 ∈ mFS ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉 ) ) → ( ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ = ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑤 ) , ⟨“ 𝑤 ”⟩ ⟩ → 𝑣 = 𝑤 ) )
18	9 17	sylbid	⊢ ( ( 𝑇 ∈ mFS ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉 ) ) → ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) → 𝑣 = 𝑤 ) )
19	18	ralrimivva	⊢ ( 𝑇 ∈ mFS → ∀ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) → 𝑣 = 𝑤 ) )
20		dff13	⊢ ( 𝐻 : 𝑉 –1-1→ 𝐸 ↔ ( 𝐻 : 𝑉 ⟶ 𝐸 ∧ ∀ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) → 𝑣 = 𝑤 ) ) )
21	4 19 20	sylanbrc	⊢ ( 𝑇 ∈ mFS → 𝐻 : 𝑉 –1-1→ 𝐸 )