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 ⊢ V = mVR ⁡ T
mvhf.e ⊢ E = mEx ⁡ T
mvhf.h ⊢ H = mVH ⁡ T
Assertion mvhf1 ⊢ T ∈ mFS → H : V ⟶ 1-1 E

Proof

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