Metamath Proof Explorer

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 imbitrid ⊢ ( ( 𝑇 ∈ mFS ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉 ) ) → ( ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑣 ) , ⟨“ 𝑣 ”⟩ ⟩ = ⟨ ( ( mType ‘ 𝑇 ) ‘ 𝑤 ) , ⟨“ 𝑤 ”⟩ ⟩ → 𝑣 = 𝑤 ) )
18 9 17 sylbid ⊢ ( ( 𝑇 ∈ mFS ∧ ( 𝑣 ∈ 𝑉 ∧ 𝑤 ∈ 𝑉 ) ) → ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) → 𝑣 = 𝑤 ) )
19 18 ralrimivva ⊢ ( 𝑇 ∈ mFS → ∀ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) → 𝑣 = 𝑤 ) )
20 dff13 ⊢ ( 𝐻 : 𝑉 –1-1→ 𝐸 ↔ ( 𝐻 : 𝑉 ⟶ 𝐸 ∧ ∀ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ 𝑉 ( ( 𝐻 ‘ 𝑣 ) = ( 𝐻 ‘ 𝑤 ) → 𝑣 = 𝑤 ) ) )
21 4 19 20 sylanbrc ⊢ ( 𝑇 ∈ mFS → 𝐻 : 𝑉 –1-1→ 𝐸 )