Theorem wwlktovf1o

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

	Ref	Expression
Hypotheses	wwlktovf1o.d	|- D = { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) }
	wwlktovf1o.r	|- R = { n e. V | { P , n } e. X }
	wwlktovf1o.f	|- F = ( t e. D |-> ( t ` 1 ) )
Assertion	wwlktovf1o	|- ( P e. V -> F : D -1-1-onto-> R )

Proof

Step	Hyp	Ref	Expression
1		wwlktovf1o.d	|- D = { w e. Word V | ( ( # ` w ) = 2 /\ ( w ` 0 ) = P /\ { ( w ` 0 ) , ( w ` 1 ) } e. X ) }
2		wwlktovf1o.r	|- R = { n e. V | { P , n } e. X }
3		wwlktovf1o.f	|- F = ( t e. D |-> ( t ` 1 ) )
4	1 2 3	wwlktovf1	|- F : D -1-1-> R
5	4	a1i	|- ( P e. V -> F : D -1-1-> R )
6	1 2 3	wwlktovfo	|- ( P e. 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 e. V -> F : D -1-1-onto-> R )