This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ffvelcdm ⊢ ( ( 𝑡 : ( 0 ..^ 2 ) ⟶ 𝑉 ∧ 1 ∈ ( 0 ..^ 2 ) ) → ( 𝑡 ‘ 1 ) ∈ 𝑉 )
13 11 12 mpan2 ⊢ ( 𝑡 : ( 0 ..^ 2 ) ⟶ 𝑉 → ( 𝑡 ‘ 1 ) ∈ 𝑉 )
14 6 13 biimtrdi ⊢ ( ( ♯ ‘ 𝑡 ) = 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 ⊢ 𝐹 : 𝐷 ⟶ 𝑅