Metamath Proof Explorer

Theorem wrdlen2i

Description: Implications of a word of length two. (Contributed by AV, 27-Jul-2018) (Proof shortened by AV, 14-Oct-2018)

Ref Expression
Assertion wrdlen2i ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → ( 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 2 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑆 ∧ ( 𝑊 ‘ 1 ) = 𝑇 ) ) ) )

Proof

Step Hyp Ref Expression
1 c0ex ⊢ 0 ∈ V
2 1ex ⊢ 1 ∈ V
3 1 2 pm3.2i ⊢ ( 0 ∈ V ∧ 1 ∈ V )
4 simpl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) → ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) )
5 0ne1 ⊢ 0 ≠ 1
6 5 a1i ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) → 0 ≠ 1 )
7 fprg ⊢ ( ( ( 0 ∈ V ∧ 1 ∈ V ) ∧ ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ 0 ≠ 1 ) → { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : { 0 , 1 } ⟶ { 𝑆 , 𝑇 } )
8 3 4 6 7 mp3an2i ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) → { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : { 0 , 1 } ⟶ { 𝑆 , 𝑇 } )
9 fzo0to2pr ⊢ ( 0 ..^ 2 ) = { 0 , 1 }
10 9 eqcomi ⊢ { 0 , 1 } = ( 0 ..^ 2 )
11 10 a1i ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → { 0 , 1 } = ( 0 ..^ 2 ) )
12 11 feq2d ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : { 0 , 1 } ⟶ { 𝑆 , 𝑇 } ↔ { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : ( 0 ..^ 2 ) ⟶ { 𝑆 , 𝑇 } ) )
13 12 biimpa ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : { 0 , 1 } ⟶ { 𝑆 , 𝑇 } ) → { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : ( 0 ..^ 2 ) ⟶ { 𝑆 , 𝑇 } )
14 prssi ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → { 𝑆 , 𝑇 } ⊆ 𝑉 )
15 14 adantr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : { 0 , 1 } ⟶ { 𝑆 , 𝑇 } ) → { 𝑆 , 𝑇 } ⊆ 𝑉 )
16 13 15 fssd ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : { 0 , 1 } ⟶ { 𝑆 , 𝑇 } ) → { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : ( 0 ..^ 2 ) ⟶ 𝑉 )
17 16 ex ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : { 0 , 1 } ⟶ { 𝑆 , 𝑇 } → { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : ( 0 ..^ 2 ) ⟶ 𝑉 ) )
18 17 adantr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) → ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : { 0 , 1 } ⟶ { 𝑆 , 𝑇 } → { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : ( 0 ..^ 2 ) ⟶ 𝑉 ) )
19 18 impcom ⊢ ( ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : { 0 , 1 } ⟶ { 𝑆 , 𝑇 } ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) ) → { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : ( 0 ..^ 2 ) ⟶ 𝑉 )
20 feq1 ⊢ ( 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } → ( 𝑊 : ( 0 ..^ 2 ) ⟶ 𝑉 ↔ { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : ( 0 ..^ 2 ) ⟶ 𝑉 ) )
21 20 adantl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) → ( 𝑊 : ( 0 ..^ 2 ) ⟶ 𝑉 ↔ { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : ( 0 ..^ 2 ) ⟶ 𝑉 ) )
22 21 adantl ⊢ ( ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : { 0 , 1 } ⟶ { 𝑆 , 𝑇 } ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) ) → ( 𝑊 : ( 0 ..^ 2 ) ⟶ 𝑉 ↔ { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : ( 0 ..^ 2 ) ⟶ 𝑉 ) )
23 19 22 mpbird ⊢ ( ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } : { 0 , 1 } ⟶ { 𝑆 , 𝑇 } ∧ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) ) → 𝑊 : ( 0 ..^ 2 ) ⟶ 𝑉 )
24 8 23 mpancom ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) → 𝑊 : ( 0 ..^ 2 ) ⟶ 𝑉 )
25 iswrdi ⊢ ( 𝑊 : ( 0 ..^ 2 ) ⟶ 𝑉 → 𝑊 ∈ Word 𝑉 )
26 24 25 syl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) → 𝑊 ∈ Word 𝑉 )
27 fveq2 ⊢ ( 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } → ( ♯ ‘ 𝑊 ) = ( ♯ ‘ { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) )
28 5 neii ⊢ ¬ 0 = 1
29 simpl ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → 𝑆 ∈ 𝑉 )
30 opth1g ⊢ ( ( 0 ∈ V ∧ 𝑆 ∈ 𝑉 ) → ( ⟨ 0 , 𝑆 ⟩ = ⟨ 1 , 𝑇 ⟩ → 0 = 1 ) )
31 1 29 30 sylancr ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → ( ⟨ 0 , 𝑆 ⟩ = ⟨ 1 , 𝑇 ⟩ → 0 = 1 ) )
32 28 31 mtoi ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → ¬ ⟨ 0 , 𝑆 ⟩ = ⟨ 1 , 𝑇 ⟩ )
33 32 neqned ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → ⟨ 0 , 𝑆 ⟩ ≠ ⟨ 1 , 𝑇 ⟩ )
34 opex ⊢ ⟨ 0 , 𝑆 ⟩ ∈ V
35 opex ⊢ ⟨ 1 , 𝑇 ⟩ ∈ V
36 34 35 pm3.2i ⊢ ( ⟨ 0 , 𝑆 ⟩ ∈ V ∧ ⟨ 1 , 𝑇 ⟩ ∈ V )
37 hashprg ⊢ ( ( ⟨ 0 , 𝑆 ⟩ ∈ V ∧ ⟨ 1 , 𝑇 ⟩ ∈ V ) → ( ⟨ 0 , 𝑆 ⟩ ≠ ⟨ 1 , 𝑇 ⟩ ↔ ( ♯ ‘ { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) = 2 ) )
38 36 37 mp1i ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → ( ⟨ 0 , 𝑆 ⟩ ≠ ⟨ 1 , 𝑇 ⟩ ↔ ( ♯ ‘ { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) = 2 ) )
39 33 38 mpbid ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → ( ♯ ‘ { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) = 2 )
40 27 39 sylan9eqr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) → ( ♯ ‘ 𝑊 ) = 2 )
41 5 a1i ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → 0 ≠ 1 )
42 fvpr1g ⊢ ( ( 0 ∈ V ∧ 𝑆 ∈ 𝑉 ∧ 0 ≠ 1 ) → ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ‘ 0 ) = 𝑆 )
43 1 29 41 42 mp3an2i ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ‘ 0 ) = 𝑆 )
44 simpr ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → 𝑇 ∈ 𝑉 )
45 fvpr2g ⊢ ( ( 1 ∈ V ∧ 𝑇 ∈ 𝑉 ∧ 0 ≠ 1 ) → ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ‘ 1 ) = 𝑇 )
46 2 44 41 45 mp3an2i ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ‘ 1 ) = 𝑇 )
47 43 46 jca ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → ( ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ‘ 0 ) = 𝑆 ∧ ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ‘ 1 ) = 𝑇 ) )
48 47 adantr ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) → ( ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ‘ 0 ) = 𝑆 ∧ ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ‘ 1 ) = 𝑇 ) )
49 fveq1 ⊢ ( 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } → ( 𝑊 ‘ 0 ) = ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ‘ 0 ) )
50 49 eqeq1d ⊢ ( 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } → ( ( 𝑊 ‘ 0 ) = 𝑆 ↔ ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ‘ 0 ) = 𝑆 ) )
51 fveq1 ⊢ ( 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } → ( 𝑊 ‘ 1 ) = ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ‘ 1 ) )
52 51 eqeq1d ⊢ ( 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } → ( ( 𝑊 ‘ 1 ) = 𝑇 ↔ ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ‘ 1 ) = 𝑇 ) )
53 50 52 anbi12d ⊢ ( 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } → ( ( ( 𝑊 ‘ 0 ) = 𝑆 ∧ ( 𝑊 ‘ 1 ) = 𝑇 ) ↔ ( ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ‘ 0 ) = 𝑆 ∧ ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ‘ 1 ) = 𝑇 ) ) )
54 53 adantl ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) → ( ( ( 𝑊 ‘ 0 ) = 𝑆 ∧ ( 𝑊 ‘ 1 ) = 𝑇 ) ↔ ( ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ‘ 0 ) = 𝑆 ∧ ( { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ‘ 1 ) = 𝑇 ) ) )
55 48 54 mpbird ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) → ( ( 𝑊 ‘ 0 ) = 𝑆 ∧ ( 𝑊 ‘ 1 ) = 𝑇 ) )
56 26 40 55 jca31 ⊢ ( ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) ∧ 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } ) → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 2 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑆 ∧ ( 𝑊 ‘ 1 ) = 𝑇 ) ) )
57 56 ex ⊢ ( ( 𝑆 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → ( 𝑊 = { ⟨ 0 , 𝑆 ⟩ , ⟨ 1 , 𝑇 ⟩ } → ( ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 2 ) ∧ ( ( 𝑊 ‘ 0 ) = 𝑆 ∧ ( 𝑊 ‘ 1 ) = 𝑇 ) ) ) )