Metamath Proof Explorer


Theorem wwlktovf1

Description: Lemma 2 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 wwlktovf1 𝐹 : 𝐷1-1𝑅

Proof

Step Hyp Ref Expression
1 wwlktovf1o.d 𝐷 = { 𝑤 ∈ Word 𝑉 ∣ ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) }
2 wwlktovf1o.r 𝑅 = { 𝑛𝑉 ∣ { 𝑃 , 𝑛 } ∈ 𝑋 }
3 wwlktovf1o.f 𝐹 = ( 𝑡𝐷 ↦ ( 𝑡 ‘ 1 ) )
4 1 2 3 wwlktovf 𝐹 : 𝐷𝑅
5 fveq1 ( 𝑡 = 𝑥 → ( 𝑡 ‘ 1 ) = ( 𝑥 ‘ 1 ) )
6 fvex ( 𝑥 ‘ 1 ) ∈ V
7 5 3 6 fvmpt ( 𝑥𝐷 → ( 𝐹𝑥 ) = ( 𝑥 ‘ 1 ) )
8 fveq1 ( 𝑡 = 𝑦 → ( 𝑡 ‘ 1 ) = ( 𝑦 ‘ 1 ) )
9 fvex ( 𝑦 ‘ 1 ) ∈ V
10 8 3 9 fvmpt ( 𝑦𝐷 → ( 𝐹𝑦 ) = ( 𝑦 ‘ 1 ) )
11 7 10 eqeqan12d ( ( 𝑥𝐷𝑦𝐷 ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) ↔ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) )
12 fveqeq2 ( 𝑤 = 𝑥 → ( ( ♯ ‘ 𝑤 ) = 2 ↔ ( ♯ ‘ 𝑥 ) = 2 ) )
13 fveq1 ( 𝑤 = 𝑥 → ( 𝑤 ‘ 0 ) = ( 𝑥 ‘ 0 ) )
14 13 eqeq1d ( 𝑤 = 𝑥 → ( ( 𝑤 ‘ 0 ) = 𝑃 ↔ ( 𝑥 ‘ 0 ) = 𝑃 ) )
15 fveq1 ( 𝑤 = 𝑥 → ( 𝑤 ‘ 1 ) = ( 𝑥 ‘ 1 ) )
16 13 15 preq12d ( 𝑤 = 𝑥 → { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } = { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } )
17 16 eleq1d ( 𝑤 = 𝑥 → ( { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ↔ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) )
18 12 14 17 3anbi123d ( 𝑤 = 𝑥 → ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) ↔ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) )
19 18 1 elrab2 ( 𝑥𝐷 ↔ ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) )
20 fveqeq2 ( 𝑤 = 𝑦 → ( ( ♯ ‘ 𝑤 ) = 2 ↔ ( ♯ ‘ 𝑦 ) = 2 ) )
21 fveq1 ( 𝑤 = 𝑦 → ( 𝑤 ‘ 0 ) = ( 𝑦 ‘ 0 ) )
22 21 eqeq1d ( 𝑤 = 𝑦 → ( ( 𝑤 ‘ 0 ) = 𝑃 ↔ ( 𝑦 ‘ 0 ) = 𝑃 ) )
23 fveq1 ( 𝑤 = 𝑦 → ( 𝑤 ‘ 1 ) = ( 𝑦 ‘ 1 ) )
24 21 23 preq12d ( 𝑤 = 𝑦 → { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } = { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } )
25 24 eleq1d ( 𝑤 = 𝑦 → ( { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ↔ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) )
26 20 22 25 3anbi123d ( 𝑤 = 𝑦 → ( ( ( ♯ ‘ 𝑤 ) = 2 ∧ ( 𝑤 ‘ 0 ) = 𝑃 ∧ { ( 𝑤 ‘ 0 ) , ( 𝑤 ‘ 1 ) } ∈ 𝑋 ) ↔ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) )
27 26 1 elrab2 ( 𝑦𝐷 ↔ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) )
28 simpr1 ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) → ( ♯ ‘ 𝑥 ) = 2 )
29 simpr1 ( ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) → ( ♯ ‘ 𝑦 ) = 2 )
30 29 eqcomd ( ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) → 2 = ( ♯ ‘ 𝑦 ) )
31 28 30 sylan9eq ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
32 31 adantr ( ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) )
33 simpr2 ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) → ( 𝑥 ‘ 0 ) = 𝑃 )
34 simpr2 ( ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) → ( 𝑦 ‘ 0 ) = 𝑃 )
35 34 eqcomd ( ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) → 𝑃 = ( 𝑦 ‘ 0 ) )
36 33 35 sylan9eq ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) → ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) )
37 36 adantr ( ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) → ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) )
38 simpr ( ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) → ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) )
39 oveq2 ( ( ♯ ‘ 𝑥 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝑥 ) ) = ( 0 ..^ 2 ) )
40 fzo0to2pr ( 0 ..^ 2 ) = { 0 , 1 }
41 39 40 eqtrdi ( ( ♯ ‘ 𝑥 ) = 2 → ( 0 ..^ ( ♯ ‘ 𝑥 ) ) = { 0 , 1 } )
42 41 raleqdv ( ( ♯ ‘ 𝑥 ) = 2 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥𝑖 ) = ( 𝑦𝑖 ) ↔ ∀ 𝑖 ∈ { 0 , 1 } ( 𝑥𝑖 ) = ( 𝑦𝑖 ) ) )
43 c0ex 0 ∈ V
44 1ex 1 ∈ V
45 fveq2 ( 𝑖 = 0 → ( 𝑥𝑖 ) = ( 𝑥 ‘ 0 ) )
46 fveq2 ( 𝑖 = 0 → ( 𝑦𝑖 ) = ( 𝑦 ‘ 0 ) )
47 45 46 eqeq12d ( 𝑖 = 0 → ( ( 𝑥𝑖 ) = ( 𝑦𝑖 ) ↔ ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ) )
48 fveq2 ( 𝑖 = 1 → ( 𝑥𝑖 ) = ( 𝑥 ‘ 1 ) )
49 fveq2 ( 𝑖 = 1 → ( 𝑦𝑖 ) = ( 𝑦 ‘ 1 ) )
50 48 49 eqeq12d ( 𝑖 = 1 → ( ( 𝑥𝑖 ) = ( 𝑦𝑖 ) ↔ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) )
51 43 44 47 50 ralpr ( ∀ 𝑖 ∈ { 0 , 1 } ( 𝑥𝑖 ) = ( 𝑦𝑖 ) ↔ ( ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) )
52 42 51 bitrdi ( ( ♯ ‘ 𝑥 ) = 2 → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥𝑖 ) = ( 𝑦𝑖 ) ↔ ( ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) ) )
53 52 3ad2ant1 ( ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥𝑖 ) = ( 𝑦𝑖 ) ↔ ( ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) ) )
54 53 ad3antlr ( ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) → ( ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥𝑖 ) = ( 𝑦𝑖 ) ↔ ( ( 𝑥 ‘ 0 ) = ( 𝑦 ‘ 0 ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) ) )
55 37 38 54 mpbir2and ( ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) → ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥𝑖 ) = ( 𝑦𝑖 ) )
56 eqwrd ( ( 𝑥 ∈ Word 𝑉𝑦 ∈ Word 𝑉 ) → ( 𝑥 = 𝑦 ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥𝑖 ) = ( 𝑦𝑖 ) ) ) )
57 56 ad2ant2r ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) → ( 𝑥 = 𝑦 ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥𝑖 ) = ( 𝑦𝑖 ) ) ) )
58 57 adantr ( ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) → ( 𝑥 = 𝑦 ↔ ( ( ♯ ‘ 𝑥 ) = ( ♯ ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ ( ♯ ‘ 𝑥 ) ) ( 𝑥𝑖 ) = ( 𝑦𝑖 ) ) ) )
59 32 55 58 mpbir2and ( ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) ∧ ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) ) → 𝑥 = 𝑦 )
60 59 ex ( ( ( 𝑥 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑥 ) = 2 ∧ ( 𝑥 ‘ 0 ) = 𝑃 ∧ { ( 𝑥 ‘ 0 ) , ( 𝑥 ‘ 1 ) } ∈ 𝑋 ) ) ∧ ( 𝑦 ∈ Word 𝑉 ∧ ( ( ♯ ‘ 𝑦 ) = 2 ∧ ( 𝑦 ‘ 0 ) = 𝑃 ∧ { ( 𝑦 ‘ 0 ) , ( 𝑦 ‘ 1 ) } ∈ 𝑋 ) ) ) → ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) → 𝑥 = 𝑦 ) )
61 19 27 60 syl2anb ( ( 𝑥𝐷𝑦𝐷 ) → ( ( 𝑥 ‘ 1 ) = ( 𝑦 ‘ 1 ) → 𝑥 = 𝑦 ) )
62 11 61 sylbid ( ( 𝑥𝐷𝑦𝐷 ) → ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) )
63 62 rgen2 𝑥𝐷𝑦𝐷 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 )
64 dff13 ( 𝐹 : 𝐷1-1𝑅 ↔ ( 𝐹 : 𝐷𝑅 ∧ ∀ 𝑥𝐷𝑦𝐷 ( ( 𝐹𝑥 ) = ( 𝐹𝑦 ) → 𝑥 = 𝑦 ) ) )
65 4 63 64 mpbir2an 𝐹 : 𝐷1-1𝑅