Theorem wwlktovf1o

Description: Lemma 4 for wrd2f1tovbij . (Contributed by Alexander van der Vekens, 28-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	wwlktovf1o	$$⊢P\in V\to F:D\underset{1-1\; 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	wwlktovf1	$$⊢F:D\underset{1-1}{⟶}R$$
5	4	a1i	$$⊢P\in V\to F:D\underset{1-1}{⟶}R$$
6	1 2 3	wwlktovfo	$$⊢P\in V\to F:D\underset{onto}{⟶}R$$
7		df-f1o	$$⊢F:D\underset{1-1\; onto}{⟶}R\leftrightarrow \left(F:D\underset{1-1}{⟶}R\wedge F:D\underset{onto}{⟶}R\right)$$
8	5 6 7	sylanbrc	$$⊢P\in V\to F:D\underset{1-1\; onto}{⟶}R$$