Theorem wwlktovf

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

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

Proof

Step	Hyp	Ref	Expression
1		wwlktovf1o.d	⊢ 𝐷 = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) }
2		wwlktovf1o.r	⊢ 𝑅 = { 𝑛 ∈ 𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 }
3		wwlktovf1o.f	⊢ 𝐹 = ( 𝑡 ∈ 𝐷 ↦ ( 𝑡 ‘ 1 ) )
4		wrdf	⊢ ( 𝑡 ∈ Word 𝑉 → 𝑡 : ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ⟶ 𝑉 )
5		oveq2	⊢ ( ( ♯ ‘ 𝑡 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝑡 ) ) = ( 0 ..^ 2 ) )
6	5	feq2d	⊢ ( ( ♯ ‘ 𝑡 ) = 2 → ( 𝑡 : ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ⟶ 𝑉 ↔ 𝑡 : ( 0 ..^ 2 ) ⟶ 𝑉 ) )
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	⊢ ( ( 𝑡 : ( 0 ..^ 2 ) ⟶ 𝑉 ∧ 1 ∈ ( 0 ..^ 2 ) ) → ( 𝑡 ‘ 1 ) ∈ 𝑉 )
13	11 12	mpan2	⊢ ( 𝑡 : ( 0 ..^ 2 ) ⟶ 𝑉 → ( 𝑡 ‘ 1 ) ∈ 𝑉 )
14	6 13	syl6bi	⊢ ( ( ♯ ‘ 𝑡 ) = 2 → ( 𝑡 : ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ⟶ 𝑉 → ( 𝑡 ‘ 1 ) ∈ 𝑉 ) )
15	14	3ad2ant1	⊢ ( ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) → ( 𝑡 : ( 0 ..^ ( ♯ ‘ 𝑡 ) ) ⟶ 𝑉 → ( 𝑡 ‘ 1 ) ∈ 𝑉 ) )
16	4 15	mpan9	⊢ ( ( 𝑡 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) ) → ( 𝑡 ‘ 1 ) ∈ 𝑉 )
17		preq1	⊢ ( ( 𝑡 ‘ 0 ) = 𝑃 → { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } = { 𝑃 , ( 𝑡 ‘ 1 ) } )
18	17	eleq1d	⊢ ( ( 𝑡 ‘ 0 ) = 𝑃 → ( { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ↔ { 𝑃 , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) )
19	18	biimpa	⊢ ( ( ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) → { 𝑃 , ( 𝑡 ‘ 1 ) } ∈ 𝑋 )
20	19	3adant1	⊢ ( ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) → { 𝑃 , ( 𝑡 ‘ 1 ) } ∈ 𝑋 )
21	20	adantl	⊢ ( ( 𝑡 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) ) → { 𝑃 , ( 𝑡 ‘ 1 ) } ∈ 𝑋 )
22	16 21	jca	⊢ ( ( 𝑡 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) ) → ( ( 𝑡 ‘ 1 ) ∈ 𝑉 ∧ { 𝑃 , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) )
23		fveqeq2	⊢ ( 𝑤 = 𝑡 → ( ( ♯ ‘ 𝑤 ) = 2 ↔ ( ♯ ‘ 𝑡 ) = 2 ) )
24		fveq1	⊢ ( 𝑤 = 𝑡 → ( 𝑤 ‘ 0 ) = ( 𝑡 ‘ 0 ) )
25	24	eqeq1d	⊢ ( 𝑤 = 𝑡 → ( ( 𝑤 ‘ 0 ) = 𝑃 ↔ ( 𝑡 ‘ 0 ) = 𝑃 ) )
26		fveq1	⊢ ( 𝑤 = 𝑡 → ( 𝑤 ‘ 1 ) = ( 𝑡 ‘ 1 ) )
27	24 26	preq12d	⊢ ( 𝑤 = 𝑡 → { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } = { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } )
28	27	eleq1d	⊢ ( 𝑤 = 𝑡 → ( { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ↔ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) )
29	23 25 28	3anbi123d	⊢ ( 𝑤 = 𝑡 → ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) ↔ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) ) )
30	29 1	elrab2	⊢ ( 𝑡 ∈ 𝐷 ↔ ( 𝑡 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑡 ) = 2 ∧ ( 𝑡 ‘ 0 ) = 𝑃 ∧ { ( 𝑡 ‘ 0 ) , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) ) )
31		preq2	⊢ ( 𝑛 = ( 𝑡 ‘ 1 ) → { 𝑃 , 𝑛 } = { 𝑃 , ( 𝑡 ‘ 1 ) } )
32	31	eleq1d	⊢ ( 𝑛 = ( 𝑡 ‘ 1 ) → ( { 𝑃 , 𝑛 } ∈ 𝑋 ↔ { 𝑃 , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) )
33	32 2	elrab2	⊢ ( ( 𝑡 ‘ 1 ) ∈ 𝑅 ↔ ( ( 𝑡 ‘ 1 ) ∈ 𝑉 ∧ { 𝑃 , ( 𝑡 ‘ 1 ) } ∈ 𝑋 ) )
34	22 30 33	3imtr4i	⊢ ( 𝑡 ∈ 𝐷 → ( 𝑡 ‘ 1 ) ∈ 𝑅 )
35	3 34	fmpti	⊢ 𝐹 : 𝐷 ⟶ 𝑅