This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wwlktovf1o

Description: Lemma 4 for wrd2f1tovbij . (Contributed by Alexander van der Vekens, 28-Jul-2018)

Ref Expression
Hypotheses wwlktovf1o.d ⊢ D = w ∈ Word V | w = 2 ∧ w ⁡ 0 = P ∧ w ⁡ 0 w ⁡ 1 ∈ X
wwlktovf1o.r ⊢ R = n ∈ V | P n ∈ X
wwlktovf1o.f ⊢ F = t ∈ D ⟼ t ⁡ 1
Assertion wwlktovf1o ⊢ P ∈ V → F : D ⟶ 1-1 onto R

Proof

Step Hyp Ref Expression
1 wwlktovf1o.d ⊢ D = w ∈ Word V | w = 2 ∧ w ⁡ 0 = P ∧ w ⁡ 0 w ⁡ 1 ∈ X
2 wwlktovf1o.r ⊢ R = n ∈ V | P n ∈ X
3 wwlktovf1o.f ⊢ F = t ∈ D ⟼ t ⁡ 1
4 1 2 3 wwlktovf1 ⊢ F : D ⟶ 1-1 R
5 4 a1i ⊢ P ∈ V → F : D ⟶ 1-1 R
6 1 2 3 wwlktovfo ⊢ P ∈ V → F : D ⟶ onto R
7 df-f1o ⊢ F : D ⟶ 1-1 onto R ↔ F : D ⟶ 1-1 R ∧ F : D ⟶ onto R
8 5 6 7 sylanbrc ⊢ P ∈ V → F : D ⟶ 1-1 onto R