Theorem wwlktovf1o

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

	Ref	Expression
Hypotheses	wwlktovf1o.d	⊢ 𝐷 = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) }
	wwlktovf1o.r	⊢ 𝑅 = { 𝑛 ∈ 𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 }
	wwlktovf1o.f	⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝑡 ‘ 1 ) )
Assertion	wwlktovf1o	⊢ ( 𝑃 ∈ 𝑉 → 𝐹 : 𝐷 –1-1-onto→ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		wwlktovf1o.d	⊢ 𝐷 = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) }
2		wwlktovf1o.r	⊢ 𝑅 = { 𝑛 ∈ 𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 }
3		wwlktovf1o.f	⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝑡 ‘ 1 ) )
4	1 2 3	wwlktovf1	⊢ 𝐹 : 𝐷 –1-1→ 𝑅
5	4	a1i	⊢ ( 𝑃 ∈ 𝑉 → 𝐹 : 𝐷 –1-1→ 𝑅 )
6	1 2 3	wwlktovfo	⊢ ( 𝑃 ∈ 𝑉 → 𝐹 : 𝐷 –onto→ 𝑅 )
7		df-f1o	⊢ ( 𝐹 : 𝐷 –1-1-onto→ 𝑅 ↔ ( 𝐹 : 𝐷 –1-1→ 𝑅 ∧ 𝐹 : 𝐷 –onto→ 𝑅 ) )
8	5 6 7	sylanbrc	⊢ ( 𝑃 ∈ 𝑉 → 𝐹 : 𝐷 –1-1-onto→ 𝑅 )