Proof of Theorem nvnencycllem
Step | Hyp | Ref
| Expression |
1 | | simpl 472 |
. . . 4
⊢ ((Fun
𝐸 ∧ 𝐹 ∈ Word dom 𝐸) → Fun 𝐸) |
2 | 1 | adantr 480 |
. . 3
⊢ (((Fun
𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (𝑋 ∈ ℕ0 ∧ 𝑋 < (#‘𝐹))) → Fun 𝐸) |
3 | | wrdf 13165 |
. . . . . 6
⊢ (𝐹 ∈ Word dom 𝐸 → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
4 | 3 | adantl 481 |
. . . . 5
⊢ ((Fun
𝐸 ∧ 𝐹 ∈ Word dom 𝐸) → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
5 | 4 | adantr 480 |
. . . 4
⊢ (((Fun
𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (𝑋 ∈ ℕ0 ∧ 𝑋 < (#‘𝐹))) → 𝐹:(0..^(#‘𝐹))⟶dom 𝐸) |
6 | | lencl 13179 |
. . . . . . 7
⊢ (𝐹 ∈ Word dom 𝐸 → (#‘𝐹) ∈
ℕ0) |
7 | | simpl 472 |
. . . . . . . . . 10
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑋 ∈ ℕ0 ∧ 𝑋 < (#‘𝐹))) → (#‘𝐹) ∈
ℕ0) |
8 | | nn0ge0 11195 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ ℕ0
→ 0 ≤ 𝑋) |
9 | | 0red 9920 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑋
∈ ℕ0) → 0 ∈ ℝ) |
10 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑋 ∈ ℕ0
→ 𝑋 ∈
ℝ) |
11 | 10 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑋
∈ ℕ0) → 𝑋 ∈ ℝ) |
12 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ∈ ℝ) |
13 | 12 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑋
∈ ℕ0) → (#‘𝐹) ∈ ℝ) |
14 | | lelttr 10007 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0
∈ ℝ ∧ 𝑋
∈ ℝ ∧ (#‘𝐹) ∈ ℝ) → ((0 ≤ 𝑋 ∧ 𝑋 < (#‘𝐹)) → 0 < (#‘𝐹))) |
15 | 9, 11, 13, 14 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑋
∈ ℕ0) → ((0 ≤ 𝑋 ∧ 𝑋 < (#‘𝐹)) → 0 < (#‘𝐹))) |
16 | | ltne 10013 |
. . . . . . . . . . . . . . . . . 18
⊢ ((0
∈ ℝ ∧ 0 < (#‘𝐹)) → (#‘𝐹) ≠ 0) |
17 | 9, 15, 16 | syl6an 566 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑋
∈ ℕ0) → ((0 ≤ 𝑋 ∧ 𝑋 < (#‘𝐹)) → (#‘𝐹) ≠ 0)) |
18 | 17 | ex 449 |
. . . . . . . . . . . . . . . 16
⊢
((#‘𝐹) ∈
ℕ0 → (𝑋 ∈ ℕ0 → ((0 ≤
𝑋 ∧ 𝑋 < (#‘𝐹)) → (#‘𝐹) ≠ 0))) |
19 | 18 | com13 86 |
. . . . . . . . . . . . . . 15
⊢ ((0 ≤
𝑋 ∧ 𝑋 < (#‘𝐹)) → (𝑋 ∈ ℕ0 →
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ≠ 0))) |
20 | 19 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (0 ≤
𝑋 → (𝑋 < (#‘𝐹) → (𝑋 ∈ ℕ0 →
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ≠ 0)))) |
21 | 20 | com23 84 |
. . . . . . . . . . . . 13
⊢ (0 ≤
𝑋 → (𝑋 ∈ ℕ0 → (𝑋 < (#‘𝐹) → ((#‘𝐹) ∈ ℕ0 →
(#‘𝐹) ≠
0)))) |
22 | 8, 21 | mpcom 37 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℕ0
→ (𝑋 <
(#‘𝐹) →
((#‘𝐹) ∈
ℕ0 → (#‘𝐹) ≠ 0))) |
23 | 22 | imp 444 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℕ0
∧ 𝑋 < (#‘𝐹)) → ((#‘𝐹) ∈ ℕ0
→ (#‘𝐹) ≠
0)) |
24 | 23 | impcom 445 |
. . . . . . . . . 10
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑋 ∈ ℕ0 ∧ 𝑋 < (#‘𝐹))) → (#‘𝐹) ≠ 0) |
25 | | elnnne0 11183 |
. . . . . . . . . 10
⊢
((#‘𝐹) ∈
ℕ ↔ ((#‘𝐹)
∈ ℕ0 ∧ (#‘𝐹) ≠ 0)) |
26 | 7, 24, 25 | sylanbrc 695 |
. . . . . . . . 9
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑋 ∈ ℕ0 ∧ 𝑋 < (#‘𝐹))) → (#‘𝐹) ∈ ℕ) |
27 | | elfzo0 12376 |
. . . . . . . . . . . . . 14
⊢ (𝑋 ∈ (0..^(#‘𝐹)) ↔ (𝑋 ∈ ℕ0 ∧
(#‘𝐹) ∈ ℕ
∧ 𝑋 < (#‘𝐹))) |
28 | 27 | biimpri 217 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ ℕ0
∧ (#‘𝐹) ∈
ℕ ∧ 𝑋 <
(#‘𝐹)) → 𝑋 ∈ (0..^(#‘𝐹))) |
29 | 28 | 3exp 1256 |
. . . . . . . . . . . 12
⊢ (𝑋 ∈ ℕ0
→ ((#‘𝐹) ∈
ℕ → (𝑋 <
(#‘𝐹) → 𝑋 ∈ (0..^(#‘𝐹))))) |
30 | 29 | com12 32 |
. . . . . . . . . . 11
⊢
((#‘𝐹) ∈
ℕ → (𝑋 ∈
ℕ0 → (𝑋 < (#‘𝐹) → 𝑋 ∈ (0..^(#‘𝐹))))) |
31 | 30 | impd 446 |
. . . . . . . . . 10
⊢
((#‘𝐹) ∈
ℕ → ((𝑋 ∈
ℕ0 ∧ 𝑋
< (#‘𝐹)) →
𝑋 ∈
(0..^(#‘𝐹)))) |
32 | 31 | adantld 482 |
. . . . . . . . 9
⊢
((#‘𝐹) ∈
ℕ → (((#‘𝐹) ∈ ℕ0 ∧ (𝑋 ∈ ℕ0
∧ 𝑋 < (#‘𝐹))) → 𝑋 ∈ (0..^(#‘𝐹)))) |
33 | 26, 32 | mpcom 37 |
. . . . . . . 8
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (𝑋 ∈ ℕ0 ∧ 𝑋 < (#‘𝐹))) → 𝑋 ∈ (0..^(#‘𝐹))) |
34 | 33 | ex 449 |
. . . . . . 7
⊢
((#‘𝐹) ∈
ℕ0 → ((𝑋 ∈ ℕ0 ∧ 𝑋 < (#‘𝐹)) → 𝑋 ∈ (0..^(#‘𝐹)))) |
35 | 6, 34 | syl 17 |
. . . . . 6
⊢ (𝐹 ∈ Word dom 𝐸 → ((𝑋 ∈ ℕ0 ∧ 𝑋 < (#‘𝐹)) → 𝑋 ∈ (0..^(#‘𝐹)))) |
36 | 35 | adantl 481 |
. . . . 5
⊢ ((Fun
𝐸 ∧ 𝐹 ∈ Word dom 𝐸) → ((𝑋 ∈ ℕ0 ∧ 𝑋 < (#‘𝐹)) → 𝑋 ∈ (0..^(#‘𝐹)))) |
37 | 36 | imp 444 |
. . . 4
⊢ (((Fun
𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (𝑋 ∈ ℕ0 ∧ 𝑋 < (#‘𝐹))) → 𝑋 ∈ (0..^(#‘𝐹))) |
38 | 5, 37 | ffvelrnd 6268 |
. . 3
⊢ (((Fun
𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (𝑋 ∈ ℕ0 ∧ 𝑋 < (#‘𝐹))) → (𝐹‘𝑋) ∈ dom 𝐸) |
39 | | fvelrn 6260 |
. . 3
⊢ ((Fun
𝐸 ∧ (𝐹‘𝑋) ∈ dom 𝐸) → (𝐸‘(𝐹‘𝑋)) ∈ ran 𝐸) |
40 | 2, 38, 39 | syl2anc 691 |
. 2
⊢ (((Fun
𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (𝑋 ∈ ℕ0 ∧ 𝑋 < (#‘𝐹))) → (𝐸‘(𝐹‘𝑋)) ∈ ran 𝐸) |
41 | | eleq1 2676 |
. 2
⊢ ((𝐸‘(𝐹‘𝑋)) = {𝐴, 𝐵} → ((𝐸‘(𝐹‘𝑋)) ∈ ran 𝐸 ↔ {𝐴, 𝐵} ∈ ran 𝐸)) |
42 | 40, 41 | syl5ibcom 234 |
1
⊢ (((Fun
𝐸 ∧ 𝐹 ∈ Word dom 𝐸) ∧ (𝑋 ∈ ℕ0 ∧ 𝑋 < (#‘𝐹))) → ((𝐸‘(𝐹‘𝑋)) = {𝐴, 𝐵} → {𝐴, 𝐵} ∈ ran 𝐸)) |