Metamath Proof Explorer

Theorem wwlktovf

Description: Lemma 1 for wrd2f1tovbij . (Contributed by Alexander van der Vekens, 27-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 wwlktovf ⊢ F : D ⟶ 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 wrdf ⊢ t ∈ Word V → t : 0 ..^ t ⟶ V
5 oveq2 ⊢ t = 2 → 0 ..^ t = 0 ..^ 2
6 5 feq2d ⊢ t = 2 → t : 0 ..^ t ⟶ V ↔ t : 0 ..^ 2 ⟶ V
7 1nn0 ⊢ 1 ∈ ℕ 0
8 2nn ⊢ 2 ∈ ℕ
9 1lt2 ⊢ 1 < 2
10 elfzo0 ⊢ 1 ∈ 0 ..^ 2 ↔ 1 ∈ ℕ 0 ∧ 2 ∈ ℕ ∧ 1 < 2
11 7 8 9 10 mpbir3an ⊢ 1 ∈ 0 ..^ 2
12 ffvelrn ⊢ t : 0 ..^ 2 ⟶ V ∧ 1 ∈ 0 ..^ 2 → t ⁡ 1 ∈ V
13 11 12 mpan2 ⊢ t : 0 ..^ 2 ⟶ V → t ⁡ 1 ∈ V
14 6 13 syl6bi ⊢ t = 2 → t : 0 ..^ t ⟶ V → t ⁡ 1 ∈ V
15 14 3ad2ant1 ⊢ t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X → t : 0 ..^ t ⟶ V → t ⁡ 1 ∈ V
16 4 15 mpan9 ⊢ t ∈ Word V ∧ t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X → t ⁡ 1 ∈ V
17 preq1 ⊢ t ⁡ 0 = P → t ⁡ 0 t ⁡ 1 = P t ⁡ 1
18 17 eleq1d ⊢ t ⁡ 0 = P → t ⁡ 0 t ⁡ 1 ∈ X ↔ P t ⁡ 1 ∈ X
19 18 biimpa ⊢ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X → P t ⁡ 1 ∈ X
20 19 3adant1 ⊢ t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X → P t ⁡ 1 ∈ X
21 20 adantl ⊢ t ∈ Word V ∧ t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X → P t ⁡ 1 ∈ X
22 16 21 jca ⊢ t ∈ Word V ∧ t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X → t ⁡ 1 ∈ V ∧ P t ⁡ 1 ∈ X
23 fveqeq2 ⊢ w = t → w = 2 ↔ t = 2
24 fveq1 ⊢ w = t → w ⁡ 0 = t ⁡ 0
25 24 eqeq1d ⊢ w = t → w ⁡ 0 = P ↔ t ⁡ 0 = P
26 fveq1 ⊢ w = t → w ⁡ 1 = t ⁡ 1
27 24 26 preq12d ⊢ w = t → w ⁡ 0 w ⁡ 1 = t ⁡ 0 t ⁡ 1
28 27 eleq1d ⊢ w = t → w ⁡ 0 w ⁡ 1 ∈ X ↔ t ⁡ 0 t ⁡ 1 ∈ X
29 23 25 28 3anbi123d ⊢ w = t → w = 2 ∧ w ⁡ 0 = P ∧ w ⁡ 0 w ⁡ 1 ∈ X ↔ t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X
30 29 1 elrab2 ⊢ t ∈ D ↔ t ∈ Word V ∧ t = 2 ∧ t ⁡ 0 = P ∧ t ⁡ 0 t ⁡ 1 ∈ X
31 preq2 ⊢ n = t ⁡ 1 → P n = P t ⁡ 1
32 31 eleq1d ⊢ n = t ⁡ 1 → P n ∈ X ↔ P t ⁡ 1 ∈ X
33 32 2 elrab2 ⊢ t ⁡ 1 ∈ R ↔ t ⁡ 1 ∈ V ∧ P t ⁡ 1 ∈ X
34 22 30 33 3imtr4i ⊢ t ∈ D → t ⁡ 1 ∈ R
35 3 34 fmpti ⊢ F : D ⟶ R