# Metamath Proof Explorer

## Theorem wwlktovfo

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

Ref Expression
Hypotheses wrd2f1tovbij.d ${⊢}{D}=\left\{{w}\in \mathrm{Word}{V}|\left(\left|{w}\right|=2\wedge {w}\left(0\right)={P}\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {X}\right)\right\}$
wrd2f1tovbij.r ${⊢}{R}=\left\{{n}\in {V}|\left\{{P},{n}\right\}\in {X}\right\}$
wrd2f1tovbij.f ${⊢}{F}=\left({t}\in {D}⟼{t}\left(1\right)\right)$
Assertion wwlktovfo ${⊢}{P}\in {V}\to {F}:{D}\underset{onto}{⟶}{R}$

### Proof

Step Hyp Ref Expression
1 wrd2f1tovbij.d ${⊢}{D}=\left\{{w}\in \mathrm{Word}{V}|\left(\left|{w}\right|=2\wedge {w}\left(0\right)={P}\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {X}\right)\right\}$
2 wrd2f1tovbij.r ${⊢}{R}=\left\{{n}\in {V}|\left\{{P},{n}\right\}\in {X}\right\}$
3 wrd2f1tovbij.f ${⊢}{F}=\left({t}\in {D}⟼{t}\left(1\right)\right)$
4 1 2 3 wwlktovf ${⊢}{F}:{D}⟶{R}$
5 4 a1i ${⊢}{P}\in {V}\to {F}:{D}⟶{R}$
6 preq2 ${⊢}{n}={p}\to \left\{{P},{n}\right\}=\left\{{P},{p}\right\}$
7 6 eleq1d ${⊢}{n}={p}\to \left(\left\{{P},{n}\right\}\in {X}↔\left\{{P},{p}\right\}\in {X}\right)$
8 7 2 elrab2 ${⊢}{p}\in {R}↔\left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)$
9 simpl ${⊢}\left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\to {p}\in {V}$
10 9 anim2i ${⊢}\left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\to \left({P}\in {V}\wedge {p}\in {V}\right)$
11 eqidd ${⊢}\left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\to \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}=\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}$
12 wrdlen2i ${⊢}\left({P}\in {V}\wedge {p}\in {V}\right)\to \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}=\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\to \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\right)$
13 10 11 12 sylc ${⊢}\left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\to \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)$
14 prex ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{V}$
15 14 a1i ${⊢}\left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\to \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{V}$
16 eleq1 ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}↔{u}\in \mathrm{Word}{V}\right)$
17 16 biimpd ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\to {u}\in \mathrm{Word}{V}\right)$
18 17 adantr ${⊢}\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\to \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\to {u}\in \mathrm{Word}{V}\right)$
19 18 com12 ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\to \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\to {u}\in \mathrm{Word}{V}\right)$
20 19 adantr ${⊢}\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\to \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\to {u}\in \mathrm{Word}{V}\right)$
21 20 adantr ${⊢}\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\to \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\to {u}\in \mathrm{Word}{V}\right)$
22 21 impcom ${⊢}\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\wedge \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\right)\to {u}\in \mathrm{Word}{V}$
23 fveqeq2 ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left(\left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2↔\left|{u}\right|=2\right)$
24 23 biimpd ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left(\left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\to \left|{u}\right|=2\right)$
25 24 adantr ${⊢}\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\to \left(\left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\to \left|{u}\right|=2\right)$
26 25 com12 ${⊢}\left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\to \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\to \left|{u}\right|=2\right)$
27 26 adantl ${⊢}\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\to \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\to \left|{u}\right|=2\right)$
28 27 adantr ${⊢}\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\to \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\to \left|{u}\right|=2\right)$
29 28 impcom ${⊢}\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\wedge \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\right)\to \left|{u}\right|=2$
30 fveq1 ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={u}\left(0\right)$
31 30 eqeq1d ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}↔{u}\left(0\right)={P}\right)$
32 31 biimpd ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\to {u}\left(0\right)={P}\right)$
33 32 adantr ${⊢}\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\to \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\to {u}\left(0\right)={P}\right)$
34 33 com12 ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\to \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\to {u}\left(0\right)={P}\right)$
35 34 adantr ${⊢}\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\to \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\to {u}\left(0\right)={P}\right)$
36 35 adantl ${⊢}\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\to \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\to {u}\left(0\right)={P}\right)$
37 36 impcom ${⊢}\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\wedge \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\right)\to {u}\left(0\right)={P}$
38 fveq1 ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={u}\left(1\right)$
39 38 eqeq1d ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}↔{u}\left(1\right)={p}\right)$
40 31 39 anbi12d ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)↔\left({u}\left(0\right)={P}\wedge {u}\left(1\right)={p}\right)\right)$
41 preq12 ${⊢}\left({u}\left(0\right)={P}\wedge {u}\left(1\right)={p}\right)\to \left\{{u}\left(0\right),{u}\left(1\right)\right\}=\left\{{P},{p}\right\}$
42 41 eqcomd ${⊢}\left({u}\left(0\right)={P}\wedge {u}\left(1\right)={p}\right)\to \left\{{P},{p}\right\}=\left\{{u}\left(0\right),{u}\left(1\right)\right\}$
43 42 eleq1d ${⊢}\left({u}\left(0\right)={P}\wedge {u}\left(1\right)={p}\right)\to \left(\left\{{P},{p}\right\}\in {X}↔\left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)$
44 43 biimpd ${⊢}\left({u}\left(0\right)={P}\wedge {u}\left(1\right)={p}\right)\to \left(\left\{{P},{p}\right\}\in {X}\to \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)$
45 40 44 syl6bi ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\to \left(\left\{{P},{p}\right\}\in {X}\to \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)\right)$
46 45 com12 ${⊢}\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\to \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left(\left\{{P},{p}\right\}\in {X}\to \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)\right)$
47 46 adantl ${⊢}\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\to \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left(\left\{{P},{p}\right\}\in {X}\to \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)\right)$
48 47 com13 ${⊢}\left\{{P},{p}\right\}\in {X}\to \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left(\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\to \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)\right)$
49 48 ad2antll ${⊢}\left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\to \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left(\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\to \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)\right)$
50 49 impcom ${⊢}\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\to \left(\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\to \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)$
51 50 imp ${⊢}\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\wedge \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\right)\to \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}$
52 29 37 51 3jca ${⊢}\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\wedge \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\right)\to \left(\left|{u}\right|=2\wedge {u}\left(0\right)={P}\wedge \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)$
53 eqcom ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}↔{p}=\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)$
54 38 eqeq2d ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left({p}=\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)↔{p}={u}\left(1\right)\right)$
55 54 biimpd ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left({p}=\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)\to {p}={u}\left(1\right)\right)$
56 53 55 syl5bi ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\to {p}={u}\left(1\right)\right)$
57 56 com12 ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\to \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to {p}={u}\left(1\right)\right)$
58 57 ad2antll ${⊢}\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\to \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to {p}={u}\left(1\right)\right)$
59 58 com12 ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left(\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\to {p}={u}\left(1\right)\right)$
60 59 adantr ${⊢}\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\to \left(\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\to {p}={u}\left(1\right)\right)$
61 60 imp ${⊢}\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\wedge \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\right)\to {p}={u}\left(1\right)$
62 22 52 61 jca31 ${⊢}\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\wedge \left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\right)\wedge \left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\right)\to \left(\left({u}\in \mathrm{Word}{V}\wedge \left(\left|{u}\right|=2\wedge {u}\left(0\right)={P}\wedge \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)\right)\wedge {p}={u}\left(1\right)\right)$
63 62 exp31 ${⊢}\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}={u}\to \left(\left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\to \left(\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\to \left(\left({u}\in \mathrm{Word}{V}\wedge \left(\left|{u}\right|=2\wedge {u}\left(0\right)={P}\wedge \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)\right)\wedge {p}={u}\left(1\right)\right)\right)\right)$
64 63 eqcoms ${⊢}{u}=\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\to \left(\left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\to \left(\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\to \left(\left({u}\in \mathrm{Word}{V}\wedge \left(\left|{u}\right|=2\wedge {u}\left(0\right)={P}\wedge \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)\right)\wedge {p}={u}\left(1\right)\right)\right)\right)$
65 64 impcom ${⊢}\left(\left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\wedge {u}=\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right)\to \left(\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\to \left(\left({u}\in \mathrm{Word}{V}\wedge \left(\left|{u}\right|=2\wedge {u}\left(0\right)={P}\wedge \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)\right)\wedge {p}={u}\left(1\right)\right)\right)$
66 15 65 spcimedv ${⊢}\left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\to \left(\left(\left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\in \mathrm{Word}{V}\wedge \left|\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\right|=2\right)\wedge \left(\left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(0\right)={P}\wedge \left\{⟨0,{P}⟩,⟨1,{p}⟩\right\}\left(1\right)={p}\right)\right)\to \exists {u}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \mathrm{Word}{V}\wedge \left(\left|{u}\right|=2\wedge {u}\left(0\right)={P}\wedge \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)\right)\wedge {p}={u}\left(1\right)\right)\right)$
67 13 66 mpd ${⊢}\left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\to \exists {u}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \mathrm{Word}{V}\wedge \left(\left|{u}\right|=2\wedge {u}\left(0\right)={P}\wedge \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)\right)\wedge {p}={u}\left(1\right)\right)$
68 fveqeq2 ${⊢}{w}={u}\to \left(\left|{w}\right|=2↔\left|{u}\right|=2\right)$
69 fveq1 ${⊢}{w}={u}\to {w}\left(0\right)={u}\left(0\right)$
70 69 eqeq1d ${⊢}{w}={u}\to \left({w}\left(0\right)={P}↔{u}\left(0\right)={P}\right)$
71 fveq1 ${⊢}{w}={u}\to {w}\left(1\right)={u}\left(1\right)$
72 69 71 preq12d ${⊢}{w}={u}\to \left\{{w}\left(0\right),{w}\left(1\right)\right\}=\left\{{u}\left(0\right),{u}\left(1\right)\right\}$
73 72 eleq1d ${⊢}{w}={u}\to \left(\left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {X}↔\left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)$
74 68 70 73 3anbi123d ${⊢}{w}={u}\to \left(\left(\left|{w}\right|=2\wedge {w}\left(0\right)={P}\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {X}\right)↔\left(\left|{u}\right|=2\wedge {u}\left(0\right)={P}\wedge \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)\right)$
75 74 elrab ${⊢}{u}\in \left\{{w}\in \mathrm{Word}{V}|\left(\left|{w}\right|=2\wedge {w}\left(0\right)={P}\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {X}\right)\right\}↔\left({u}\in \mathrm{Word}{V}\wedge \left(\left|{u}\right|=2\wedge {u}\left(0\right)={P}\wedge \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)\right)$
76 75 anbi1i ${⊢}\left({u}\in \left\{{w}\in \mathrm{Word}{V}|\left(\left|{w}\right|=2\wedge {w}\left(0\right)={P}\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {X}\right)\right\}\wedge {p}={u}\left(1\right)\right)↔\left(\left({u}\in \mathrm{Word}{V}\wedge \left(\left|{u}\right|=2\wedge {u}\left(0\right)={P}\wedge \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)\right)\wedge {p}={u}\left(1\right)\right)$
77 76 exbii ${⊢}\exists {u}\phantom{\rule{.4em}{0ex}}\left({u}\in \left\{{w}\in \mathrm{Word}{V}|\left(\left|{w}\right|=2\wedge {w}\left(0\right)={P}\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {X}\right)\right\}\wedge {p}={u}\left(1\right)\right)↔\exists {u}\phantom{\rule{.4em}{0ex}}\left(\left({u}\in \mathrm{Word}{V}\wedge \left(\left|{u}\right|=2\wedge {u}\left(0\right)={P}\wedge \left\{{u}\left(0\right),{u}\left(1\right)\right\}\in {X}\right)\right)\wedge {p}={u}\left(1\right)\right)$
78 67 77 sylibr ${⊢}\left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\to \exists {u}\phantom{\rule{.4em}{0ex}}\left({u}\in \left\{{w}\in \mathrm{Word}{V}|\left(\left|{w}\right|=2\wedge {w}\left(0\right)={P}\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {X}\right)\right\}\wedge {p}={u}\left(1\right)\right)$
79 df-rex ${⊢}\exists {u}\in \left\{{w}\in \mathrm{Word}{V}|\left(\left|{w}\right|=2\wedge {w}\left(0\right)={P}\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {X}\right)\right\}\phantom{\rule{.4em}{0ex}}{p}={u}\left(1\right)↔\exists {u}\phantom{\rule{.4em}{0ex}}\left({u}\in \left\{{w}\in \mathrm{Word}{V}|\left(\left|{w}\right|=2\wedge {w}\left(0\right)={P}\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {X}\right)\right\}\wedge {p}={u}\left(1\right)\right)$
80 78 79 sylibr ${⊢}\left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\to \exists {u}\in \left\{{w}\in \mathrm{Word}{V}|\left(\left|{w}\right|=2\wedge {w}\left(0\right)={P}\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {X}\right)\right\}\phantom{\rule{.4em}{0ex}}{p}={u}\left(1\right)$
81 1 rexeqi ${⊢}\exists {u}\in {D}\phantom{\rule{.4em}{0ex}}{p}={u}\left(1\right)↔\exists {u}\in \left\{{w}\in \mathrm{Word}{V}|\left(\left|{w}\right|=2\wedge {w}\left(0\right)={P}\wedge \left\{{w}\left(0\right),{w}\left(1\right)\right\}\in {X}\right)\right\}\phantom{\rule{.4em}{0ex}}{p}={u}\left(1\right)$
82 80 81 sylibr ${⊢}\left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\to \exists {u}\in {D}\phantom{\rule{.4em}{0ex}}{p}={u}\left(1\right)$
83 fveq1 ${⊢}{t}={u}\to {t}\left(1\right)={u}\left(1\right)$
84 fvex ${⊢}{u}\left(1\right)\in \mathrm{V}$
85 83 3 84 fvmpt ${⊢}{u}\in {D}\to {F}\left({u}\right)={u}\left(1\right)$
86 85 eqeq2d ${⊢}{u}\in {D}\to \left({p}={F}\left({u}\right)↔{p}={u}\left(1\right)\right)$
87 86 rexbiia ${⊢}\exists {u}\in {D}\phantom{\rule{.4em}{0ex}}{p}={F}\left({u}\right)↔\exists {u}\in {D}\phantom{\rule{.4em}{0ex}}{p}={u}\left(1\right)$
88 82 87 sylibr ${⊢}\left({P}\in {V}\wedge \left({p}\in {V}\wedge \left\{{P},{p}\right\}\in {X}\right)\right)\to \exists {u}\in {D}\phantom{\rule{.4em}{0ex}}{p}={F}\left({u}\right)$
89 8 88 sylan2b ${⊢}\left({P}\in {V}\wedge {p}\in {R}\right)\to \exists {u}\in {D}\phantom{\rule{.4em}{0ex}}{p}={F}\left({u}\right)$
90 89 ralrimiva ${⊢}{P}\in {V}\to \forall {p}\in {R}\phantom{\rule{.4em}{0ex}}\exists {u}\in {D}\phantom{\rule{.4em}{0ex}}{p}={F}\left({u}\right)$
91 dffo3 ${⊢}{F}:{D}\underset{onto}{⟶}{R}↔\left({F}:{D}⟶{R}\wedge \forall {p}\in {R}\phantom{\rule{.4em}{0ex}}\exists {u}\in {D}\phantom{\rule{.4em}{0ex}}{p}={F}\left({u}\right)\right)$
92 5 90 91 sylanbrc ${⊢}{P}\in {V}\to {F}:{D}\underset{onto}{⟶}{R}$