Proof of Theorem repsdf2
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | repsconst 14810 | . . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑆 repeatS 𝑁) = ((0..^𝑁) × {𝑆})) | 
| 2 | 1 | eqeq2d 2748 | . 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊 = (𝑆 repeatS 𝑁) ↔ 𝑊 = ((0..^𝑁) × {𝑆}))) | 
| 3 |  | fconst2g 7223 | . . 3
⊢ (𝑆 ∈ 𝑉 → (𝑊:(0..^𝑁)⟶{𝑆} ↔ 𝑊 = ((0..^𝑁) × {𝑆}))) | 
| 4 | 3 | adantr 480 | . 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊:(0..^𝑁)⟶{𝑆} ↔ 𝑊 = ((0..^𝑁) × {𝑆}))) | 
| 5 |  | fconstfv 7232 | . . . . . . . . 9
⊢ (𝑊:(0..^𝑁)⟶{𝑆} ↔ (𝑊 Fn (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆)) | 
| 6 |  | snssi 4808 | . . . . . . . . . . . . . 14
⊢ (𝑆 ∈ 𝑉 → {𝑆} ⊆ 𝑉) | 
| 7 | 6 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → {𝑆} ⊆ 𝑉) | 
| 8 | 7 | anim1ci 616 | . . . . . . . . . . . 12
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑊:(0..^𝑁)⟶{𝑆}) → (𝑊:(0..^𝑁)⟶{𝑆} ∧ {𝑆} ⊆ 𝑉)) | 
| 9 |  | fss 6752 | . . . . . . . . . . . 12
⊢ ((𝑊:(0..^𝑁)⟶{𝑆} ∧ {𝑆} ⊆ 𝑉) → 𝑊:(0..^𝑁)⟶𝑉) | 
| 10 |  | iswrdi 14556 | . . . . . . . . . . . 12
⊢ (𝑊:(0..^𝑁)⟶𝑉 → 𝑊 ∈ Word 𝑉) | 
| 11 | 8, 9, 10 | 3syl 18 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑊:(0..^𝑁)⟶{𝑆}) → 𝑊 ∈ Word 𝑉) | 
| 12 |  | ffzo0hash 14488 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℕ0
∧ 𝑊 Fn (0..^𝑁)) → (♯‘𝑊) = 𝑁) | 
| 13 | 12 | expcom 413 | . . . . . . . . . . . . . 14
⊢ (𝑊 Fn (0..^𝑁) → (𝑁 ∈ ℕ0 →
(♯‘𝑊) = 𝑁)) | 
| 14 |  | ffn 6736 | . . . . . . . . . . . . . 14
⊢ (𝑊:(0..^𝑁)⟶{𝑆} → 𝑊 Fn (0..^𝑁)) | 
| 15 | 13, 14 | syl11 33 | . . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℕ0
→ (𝑊:(0..^𝑁)⟶{𝑆} → (♯‘𝑊) = 𝑁)) | 
| 16 | 15 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊:(0..^𝑁)⟶{𝑆} → (♯‘𝑊) = 𝑁)) | 
| 17 | 16 | imp 406 | . . . . . . . . . . 11
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑊:(0..^𝑁)⟶{𝑆}) → (♯‘𝑊) = 𝑁) | 
| 18 | 11, 17 | jca 511 | . . . . . . . . . 10
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧ 𝑊:(0..^𝑁)⟶{𝑆}) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁)) | 
| 19 | 18 | ex 412 | . . . . . . . . 9
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊:(0..^𝑁)⟶{𝑆} → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁))) | 
| 20 | 5, 19 | biimtrrid 243 | . . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑊 Fn (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁))) | 
| 21 | 20 | expcomd 416 | . . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(∀𝑖 ∈
(0..^𝑁)(𝑊‘𝑖) = 𝑆 → (𝑊 Fn (0..^𝑁) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁)))) | 
| 22 | 21 | imp 406 | . . . . . 6
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆) → (𝑊 Fn (0..^𝑁) → (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁))) | 
| 23 |  | wrdf 14557 | . . . . . . . . . 10
⊢ (𝑊 ∈ Word 𝑉 → 𝑊:(0..^(♯‘𝑊))⟶𝑉) | 
| 24 |  | ffn 6736 | . . . . . . . . . 10
⊢ (𝑊:(0..^(♯‘𝑊))⟶𝑉 → 𝑊 Fn (0..^(♯‘𝑊))) | 
| 25 |  | oveq2 7439 | . . . . . . . . . . . . . 14
⊢
((♯‘𝑊) =
𝑁 →
(0..^(♯‘𝑊)) =
(0..^𝑁)) | 
| 26 | 25 | fneq2d 6662 | . . . . . . . . . . . . 13
⊢
((♯‘𝑊) =
𝑁 → (𝑊 Fn (0..^(♯‘𝑊)) ↔ 𝑊 Fn (0..^𝑁))) | 
| 27 | 26 | biimpd 229 | . . . . . . . . . . . 12
⊢
((♯‘𝑊) =
𝑁 → (𝑊 Fn (0..^(♯‘𝑊)) → 𝑊 Fn (0..^𝑁))) | 
| 28 | 27 | a1d 25 | . . . . . . . . . . 11
⊢
((♯‘𝑊) =
𝑁 → ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊 Fn (0..^(♯‘𝑊)) → 𝑊 Fn (0..^𝑁)))) | 
| 29 | 28 | com13 88 | . . . . . . . . . 10
⊢ (𝑊 Fn (0..^(♯‘𝑊)) → ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
((♯‘𝑊) = 𝑁 → 𝑊 Fn (0..^𝑁)))) | 
| 30 | 23, 24, 29 | 3syl 18 | . . . . . . . . 9
⊢ (𝑊 ∈ Word 𝑉 → ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
((♯‘𝑊) = 𝑁 → 𝑊 Fn (0..^𝑁)))) | 
| 31 | 30 | com12 32 | . . . . . . . 8
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊 ∈ Word 𝑉 → ((♯‘𝑊) = 𝑁 → 𝑊 Fn (0..^𝑁)))) | 
| 32 | 31 | impd 410 | . . . . . . 7
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) → 𝑊 Fn (0..^𝑁))) | 
| 33 | 32 | adantr 480 | . . . . . 6
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆) → ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) → 𝑊 Fn (0..^𝑁))) | 
| 34 | 22, 33 | impbid 212 | . . . . 5
⊢ (((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) ∧
∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆) → (𝑊 Fn (0..^𝑁) ↔ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁))) | 
| 35 | 34 | ex 412 | . . . 4
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) →
(∀𝑖 ∈
(0..^𝑁)(𝑊‘𝑖) = 𝑆 → (𝑊 Fn (0..^𝑁) ↔ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁)))) | 
| 36 | 35 | pm5.32rd 578 | . . 3
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → ((𝑊 Fn (0..^𝑁) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆) ↔ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆))) | 
| 37 |  | df-3an 1089 | . . 3
⊢ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆) ↔ ((𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆)) | 
| 38 | 36, 5, 37 | 3bitr4g 314 | . 2
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊:(0..^𝑁)⟶{𝑆} ↔ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆))) | 
| 39 | 2, 4, 38 | 3bitr2d 307 | 1
⊢ ((𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0) → (𝑊 = (𝑆 repeatS 𝑁) ↔ (𝑊 ∈ Word 𝑉 ∧ (♯‘𝑊) = 𝑁 ∧ ∀𝑖 ∈ (0..^𝑁)(𝑊‘𝑖) = 𝑆))) |