Step | Hyp | Ref
| Expression |
1 | | df-eupa 26490 |
. . . 4
⊢ EulPaths
= (𝑣 ∈ V, 𝑒 ∈ V ↦ {〈𝑓, 𝑝〉 ∣ (𝑣 UMGrph 𝑒 ∧ ∃𝑛 ∈ ℕ0 (𝑓:(1...𝑛)–1-1-onto→dom
𝑒 ∧ 𝑝:(0...𝑛)⟶𝑣 ∧ ∀𝑘 ∈ (1...𝑛)(𝑒‘(𝑓‘𝑘)) = {(𝑝‘(𝑘 − 1)), (𝑝‘𝑘)}))}) |
2 | 1 | brovmpt2ex 7236 |
. . 3
⊢ (𝐹(𝑉 EulPaths 𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V))) |
3 | | eupatrl.f |
. . . . . . 7
⊢ 𝐺 = (𝑥 ∈ (0..^(#‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) |
4 | | ovex 6577 |
. . . . . . . 8
⊢
(0..^(#‘𝐹))
∈ V |
5 | 4 | mptex 6390 |
. . . . . . 7
⊢ (𝑥 ∈ (0..^(#‘𝐹)) ↦ (𝐹‘(𝑥 + 1))) ∈ V |
6 | 3, 5 | eqeltri 2684 |
. . . . . 6
⊢ 𝐺 ∈ V |
7 | 6 | a1i 11 |
. . . . 5
⊢ (𝐹 ∈ V → 𝐺 ∈ V) |
8 | 7 | anim1i 590 |
. . . 4
⊢ ((𝐹 ∈ V ∧ 𝑃 ∈ V) → (𝐺 ∈ V ∧ 𝑃 ∈ V)) |
9 | 8 | anim2i 591 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐺 ∈ V ∧ 𝑃 ∈ V))) |
10 | 2, 9 | syl 17 |
. 2
⊢ (𝐹(𝑉 EulPaths 𝐸)𝑃 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐺 ∈ V ∧ 𝑃 ∈ V))) |
11 | | f1ofn 6051 |
. . . . . . . . . . . . 13
⊢ (𝐹:(1...𝑛)–1-1-onto→dom
𝐸 → 𝐹 Fn (1...𝑛)) |
12 | | fseq1hash 13026 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℕ0
∧ 𝐹 Fn (1...𝑛)) → (#‘𝐹) = 𝑛) |
13 | 11, 12 | sylan2 490 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℕ0
∧ 𝐹:(1...𝑛)–1-1-onto→dom
𝐸) → (#‘𝐹) = 𝑛) |
14 | 13 | ancoms 468 |
. . . . . . . . . . 11
⊢ ((𝐹:(1...𝑛)–1-1-onto→dom
𝐸 ∧ 𝑛 ∈ ℕ0) →
(#‘𝐹) = 𝑛) |
15 | | f1of1 6049 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 → 𝐹:(1...(#‘𝐹))–1-1→dom 𝐸) |
16 | 3 | fargshiftf1 26165 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝐹:(1...(#‘𝐹))–1-1→dom 𝐸) → 𝐺:(0..^(#‘𝐹))–1-1→dom 𝐸) |
17 | 16 | expcom 450 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:(1...(#‘𝐹))–1-1→dom 𝐸 → ((#‘𝐹) ∈ ℕ0 → 𝐺:(0..^(#‘𝐹))–1-1→dom 𝐸)) |
18 | 15, 17 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 → ((#‘𝐹) ∈ ℕ0
→ 𝐺:(0..^(#‘𝐹))–1-1→dom 𝐸)) |
19 | 18 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0)
→ 𝐺:(0..^(#‘𝐹))–1-1→dom 𝐸) |
20 | | f1ofo 6057 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 → 𝐹:(1...(#‘𝐹))–onto→dom 𝐸) |
21 | 3 | fargshiftfo 26166 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝐹:(1...(#‘𝐹))–onto→dom 𝐸) → 𝐺:(0..^(#‘𝐹))–onto→dom 𝐸) |
22 | 21 | expcom 450 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹:(1...(#‘𝐹))–onto→dom 𝐸 → ((#‘𝐹) ∈ ℕ0 → 𝐺:(0..^(#‘𝐹))–onto→dom 𝐸)) |
23 | 20, 22 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 → ((#‘𝐹) ∈ ℕ0
→ 𝐺:(0..^(#‘𝐹))–onto→dom 𝐸)) |
24 | 23 | imp 444 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0)
→ 𝐺:(0..^(#‘𝐹))–onto→dom 𝐸) |
25 | | df-f1o 5811 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ↔ (𝐺:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝐺:(0..^(#‘𝐹))–onto→dom 𝐸)) |
26 | 19, 24, 25 | sylanbrc 695 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0)
→ 𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸) |
27 | | f1ofn 6051 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 → 𝐺 Fn (0..^(#‘𝐹))) |
28 | | hashfn 13025 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐺 Fn (0..^(#‘𝐹)) → (#‘𝐺) = (#‘(0..^(#‘𝐹)))) |
29 | 28 | anim2i 591 |
. . . . . . . . . . . . . . . . . 18
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝐺
Fn (0..^(#‘𝐹)))
→ ((#‘𝐹) ∈
ℕ0 ∧ (#‘𝐺) = (#‘(0..^(#‘𝐹))))) |
30 | 29 | ancoms 468 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺 Fn (0..^(#‘𝐹)) ∧ (#‘𝐹) ∈ ℕ0)
→ ((#‘𝐹) ∈
ℕ0 ∧ (#‘𝐺) = (#‘(0..^(#‘𝐹))))) |
31 | 27, 30 | sylan 487 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0)
→ ((#‘𝐹) ∈
ℕ0 ∧ (#‘𝐺) = (#‘(0..^(#‘𝐹))))) |
32 | | hashfzo0 13077 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝐹) ∈
ℕ0 → (#‘(0..^(#‘𝐹))) = (#‘𝐹)) |
33 | 32 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢
((#‘𝐹) ∈
ℕ0 → ((#‘𝐺) = (#‘(0..^(#‘𝐹))) ↔ (#‘𝐺) = (#‘𝐹))) |
34 | 33 | biimpa 500 |
. . . . . . . . . . . . . . . . 17
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (#‘𝐺) = (#‘(0..^(#‘𝐹)))) → (#‘𝐺) = (#‘𝐹)) |
35 | | pm3.2 462 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 → ((#‘𝐺) = (#‘𝐹) → (𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐺) = (#‘𝐹)))) |
36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0)
→ ((#‘𝐺) =
(#‘𝐹) → (𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐺) = (#‘𝐹)))) |
37 | 34, 36 | syl5com 31 |
. . . . . . . . . . . . . . . 16
⊢
(((#‘𝐹) ∈
ℕ0 ∧ (#‘𝐺) = (#‘(0..^(#‘𝐹)))) → ((𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0)
→ (𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐺) = (#‘𝐹)))) |
38 | 31, 37 | mpcom 37 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0)
→ (𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐺) = (#‘𝐹))) |
39 | 26, 38 | sylancom 698 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0)
→ (𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐺) = (#‘𝐹))) |
40 | | df-f1 5809 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐺:(0..^(#‘𝐹))–1-1→dom 𝐸 ↔ (𝐺:(0..^(#‘𝐹))⟶dom 𝐸 ∧ Fun ◡𝐺)) |
41 | | iswrdi 13164 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐺:(0..^(#‘𝐹))⟶dom 𝐸 → 𝐺 ∈ Word dom 𝐸) |
42 | 41 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐺:(0..^(#‘𝐹))⟶dom 𝐸 ∧ Fun ◡𝐺) → 𝐺 ∈ Word dom 𝐸) |
43 | 40, 42 | sylbi 206 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺:(0..^(#‘𝐹))–1-1→dom 𝐸 → 𝐺 ∈ Word dom 𝐸) |
44 | 43 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝐺:(0..^(#‘𝐹))–onto→dom 𝐸) → 𝐺 ∈ Word dom 𝐸) |
45 | 25, 44 | sylbi 206 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 → 𝐺 ∈ Word dom 𝐸) |
46 | 45 | ad4antr 764 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐺) = (#‘𝐹)) ∧ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0))
∧ ∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → 𝐺 ∈ Word dom 𝐸) |
47 | 40 | simprbi 479 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺:(0..^(#‘𝐹))–1-1→dom 𝐸 → Fun ◡𝐺) |
48 | 47 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐺:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ 𝐺:(0..^(#‘𝐹))–onto→dom 𝐸) → Fun ◡𝐺) |
49 | 25, 48 | sylbi 206 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 → Fun ◡𝐺) |
50 | 49 | ad4antr 764 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐺) = (#‘𝐹)) ∧ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0))
∧ ∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → Fun ◡𝐺) |
51 | 46, 50 | jca 553 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐺) = (#‘𝐹)) ∧ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0))
∧ ∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → (𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺)) |
52 | | eqcom 2617 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝐺) =
(#‘𝐹) ↔
(#‘𝐹) =
(#‘𝐺)) |
53 | 52 | biimpi 205 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐺) =
(#‘𝐹) →
(#‘𝐹) =
(#‘𝐺)) |
54 | 53 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐺) = (#‘𝐹)) ∧ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0))
∧ ∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) → (#‘𝐹) = (#‘𝐺)) |
55 | 54 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐺) = (#‘𝐹)) ∧ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0))
∧ ∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) → (0...(#‘𝐹)) = (0...(#‘𝐺))) |
56 | 55 | feq2d 5944 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐺) = (#‘𝐹)) ∧ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0))
∧ ∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) → (𝑃:(0...(#‘𝐹))⟶𝑉 ↔ 𝑃:(0...(#‘𝐺))⟶𝑉)) |
57 | 56 | biimpa 500 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐺) = (#‘𝐹)) ∧ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0))
∧ ∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → 𝑃:(0...(#‘𝐺))⟶𝑉) |
58 | | f1of 6050 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 → 𝐹:(1...(#‘𝐹))⟶dom 𝐸) |
59 | | fargshiftlem 26162 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑙
∈ (0..^(#‘𝐹)))
→ (𝑙 + 1) ∈
(1...(#‘𝐹))) |
60 | | simpll 786 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝑙 + 1) ∈ (1...(#‘𝐹)) ∧ ((#‘𝐹) ∈ ℕ0
∧ 𝑙 ∈
(0..^(#‘𝐹)))) ∧
𝐹:(1...(#‘𝐹))⟶dom 𝐸) → (𝑙 + 1) ∈ (1...(#‘𝐹))) |
61 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑘 = (𝑙 + 1) → (𝐹‘𝑘) = (𝐹‘(𝑙 + 1))) |
62 | 61 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝑘 = (𝑙 + 1) → (𝐸‘(𝐹‘𝑘)) = (𝐸‘(𝐹‘(𝑙 + 1)))) |
63 | 62 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝑙 ∈ (0..^(#‘𝐹))) ∧ 𝑘 = (𝑙 + 1)) → (𝐸‘(𝐹‘𝑘)) = (𝐸‘(𝐹‘(𝑙 + 1)))) |
64 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑘 = (𝑙 + 1) → (𝑘 − 1) = ((𝑙 + 1) − 1)) |
65 | | elfzoelz 12339 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (𝑙 ∈ (0..^(#‘𝐹)) → 𝑙 ∈ ℤ) |
66 | 65 | zcnd 11359 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (𝑙 ∈ (0..^(#‘𝐹)) → 𝑙 ∈ ℂ) |
67 | 66 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑙
∈ (0..^(#‘𝐹)))
→ 𝑙 ∈
ℂ) |
68 | | 1cnd 9935 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑙
∈ (0..^(#‘𝐹)))
→ 1 ∈ ℂ) |
69 | 67, 68 | pncand 10272 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑙
∈ (0..^(#‘𝐹)))
→ ((𝑙 + 1) − 1)
= 𝑙) |
70 | 64, 69 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝑙 ∈ (0..^(#‘𝐹))) ∧ 𝑘 = (𝑙 + 1)) → (𝑘 − 1) = 𝑙) |
71 | 70 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝑙 ∈ (0..^(#‘𝐹))) ∧ 𝑘 = (𝑙 + 1)) → (𝑃‘(𝑘 − 1)) = (𝑃‘𝑙)) |
72 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑘 = (𝑙 + 1) → (𝑃‘𝑘) = (𝑃‘(𝑙 + 1))) |
73 | 72 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝑙 ∈ (0..^(#‘𝐹))) ∧ 𝑘 = (𝑙 + 1)) → (𝑃‘𝑘) = (𝑃‘(𝑙 + 1))) |
74 | 71, 73 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝑙 ∈ (0..^(#‘𝐹))) ∧ 𝑘 = (𝑙 + 1)) → {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}) |
75 | 63, 74 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝑙 ∈ (0..^(#‘𝐹))) ∧ 𝑘 = (𝑙 + 1)) → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} ↔ (𝐸‘(𝐹‘(𝑙 + 1))) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})) |
76 | 75 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑙
∈ (0..^(#‘𝐹)))
→ (𝑘 = (𝑙 + 1) → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} ↔ (𝐸‘(𝐹‘(𝑙 + 1))) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))) |
77 | 76 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑙 + 1) ∈ (1...(#‘𝐹)) ∧ ((#‘𝐹) ∈ ℕ0
∧ 𝑙 ∈
(0..^(#‘𝐹)))) →
(𝑘 = (𝑙 + 1) → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} ↔ (𝐸‘(𝐹‘(𝑙 + 1))) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))) |
78 | 77 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((((𝑙 + 1) ∈ (1...(#‘𝐹)) ∧ ((#‘𝐹) ∈ ℕ0
∧ 𝑙 ∈
(0..^(#‘𝐹)))) ∧
𝐹:(1...(#‘𝐹))⟶dom 𝐸) → (𝑘 = (𝑙 + 1) → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} ↔ (𝐸‘(𝐹‘(𝑙 + 1))) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))) |
79 | 78 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝑙 + 1) ∈
(1...(#‘𝐹)) ∧
((#‘𝐹) ∈
ℕ0 ∧ 𝑙
∈ (0..^(#‘𝐹))))
∧ 𝐹:(1...(#‘𝐹))⟶dom 𝐸) ∧ 𝑘 = (𝑙 + 1)) → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} ↔ (𝐸‘(𝐹‘(𝑙 + 1))) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})) |
80 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (((𝑙 + 1) ∈ (1...(#‘𝐹)) ∧ ((#‘𝐹) ∈ ℕ0
∧ 𝑙 ∈
(0..^(#‘𝐹)))) →
(#‘𝐹) ∈
ℕ0) |
81 | 80 | anim1i 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((((𝑙 + 1) ∈ (1...(#‘𝐹)) ∧ ((#‘𝐹) ∈ ℕ0
∧ 𝑙 ∈
(0..^(#‘𝐹)))) ∧
𝐹:(1...(#‘𝐹))⟶dom 𝐸) → ((#‘𝐹) ∈ ℕ0 ∧ 𝐹:(1...(#‘𝐹))⟶dom 𝐸)) |
82 | 81 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((((𝑙 + 1) ∈
(1...(#‘𝐹)) ∧
((#‘𝐹) ∈
ℕ0 ∧ 𝑙
∈ (0..^(#‘𝐹))))
∧ 𝐹:(1...(#‘𝐹))⟶dom 𝐸) ∧ 𝑘 = (𝑙 + 1)) → ((#‘𝐹) ∈ ℕ0 ∧ 𝐹:(1...(#‘𝐹))⟶dom 𝐸)) |
83 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑙
∈ (0..^(#‘𝐹)))
→ 𝑙 ∈
(0..^(#‘𝐹))) |
84 | 83 | ad3antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
(((((𝑙 + 1) ∈
(1...(#‘𝐹)) ∧
((#‘𝐹) ∈
ℕ0 ∧ 𝑙
∈ (0..^(#‘𝐹))))
∧ 𝐹:(1...(#‘𝐹))⟶dom 𝐸) ∧ 𝑘 = (𝑙 + 1)) → 𝑙 ∈ (0..^(#‘𝐹))) |
85 | 3 | fargshiftfv 26163 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝐹:(1...(#‘𝐹))⟶dom 𝐸) → (𝑙 ∈ (0..^(#‘𝐹)) → (𝐺‘𝑙) = (𝐹‘(𝑙 + 1)))) |
86 | 85 | imp 444 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝐹:(1...(#‘𝐹))⟶dom 𝐸) ∧ 𝑙 ∈ (0..^(#‘𝐹))) → (𝐺‘𝑙) = (𝐹‘(𝑙 + 1))) |
87 | 86 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝐹:(1...(#‘𝐹))⟶dom 𝐸) ∧ 𝑙 ∈ (0..^(#‘𝐹))) → (𝐹‘(𝑙 + 1)) = (𝐺‘𝑙)) |
88 | 82, 84, 87 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢
(((((𝑙 + 1) ∈
(1...(#‘𝐹)) ∧
((#‘𝐹) ∈
ℕ0 ∧ 𝑙
∈ (0..^(#‘𝐹))))
∧ 𝐹:(1...(#‘𝐹))⟶dom 𝐸) ∧ 𝑘 = (𝑙 + 1)) → (𝐹‘(𝑙 + 1)) = (𝐺‘𝑙)) |
89 | 88 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢
(((((𝑙 + 1) ∈
(1...(#‘𝐹)) ∧
((#‘𝐹) ∈
ℕ0 ∧ 𝑙
∈ (0..^(#‘𝐹))))
∧ 𝐹:(1...(#‘𝐹))⟶dom 𝐸) ∧ 𝑘 = (𝑙 + 1)) → (𝐸‘(𝐹‘(𝑙 + 1))) = (𝐸‘(𝐺‘𝑙))) |
90 | 89 | eqeq1d 2612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢
(((((𝑙 + 1) ∈
(1...(#‘𝐹)) ∧
((#‘𝐹) ∈
ℕ0 ∧ 𝑙
∈ (0..^(#‘𝐹))))
∧ 𝐹:(1...(#‘𝐹))⟶dom 𝐸) ∧ 𝑘 = (𝑙 + 1)) → ((𝐸‘(𝐹‘(𝑙 + 1))) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))} ↔ (𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})) |
91 | 79, 90 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢
(((((𝑙 + 1) ∈
(1...(#‘𝐹)) ∧
((#‘𝐹) ∈
ℕ0 ∧ 𝑙
∈ (0..^(#‘𝐹))))
∧ 𝐹:(1...(#‘𝐹))⟶dom 𝐸) ∧ 𝑘 = (𝑙 + 1)) → ((𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} ↔ (𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})) |
92 | 60, 91 | rspcdv 3285 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑙 + 1) ∈ (1...(#‘𝐹)) ∧ ((#‘𝐹) ∈ ℕ0
∧ 𝑙 ∈
(0..^(#‘𝐹)))) ∧
𝐹:(1...(#‘𝐹))⟶dom 𝐸) → (∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → (𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})) |
93 | 92 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑙 + 1) ∈ (1...(#‘𝐹)) ∧ ((#‘𝐹) ∈ ℕ0
∧ 𝑙 ∈
(0..^(#‘𝐹)))) →
(𝐹:(1...(#‘𝐹))⟶dom 𝐸 → (∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → (𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))) |
94 | 93 | com23 84 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑙 + 1) ∈ (1...(#‘𝐹)) ∧ ((#‘𝐹) ∈ ℕ0
∧ 𝑙 ∈
(0..^(#‘𝐹)))) →
(∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → (𝐹:(1...(#‘𝐹))⟶dom 𝐸 → (𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))) |
95 | 59, 94 | mpancom 700 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝑙
∈ (0..^(#‘𝐹)))
→ (∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → (𝐹:(1...(#‘𝐹))⟶dom 𝐸 → (𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))) |
96 | 95 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢
((#‘𝐹) ∈
ℕ0 → (𝑙 ∈ (0..^(#‘𝐹)) → (∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → (𝐹:(1...(#‘𝐹))⟶dom 𝐸 → (𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})))) |
97 | 96 | com24 93 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((#‘𝐹) ∈
ℕ0 → (𝐹:(1...(#‘𝐹))⟶dom 𝐸 → (∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → (𝑙 ∈ (0..^(#‘𝐹)) → (𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})))) |
98 | 97 | imp31 447 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝐹:(1...(#‘𝐹))⟶dom 𝐸) ∧ ∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) → (𝑙 ∈ (0..^(#‘𝐹)) → (𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})) |
99 | 98 | ralrimiv 2948 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((((#‘𝐹)
∈ ℕ0 ∧ 𝐹:(1...(#‘𝐹))⟶dom 𝐸) ∧ ∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) → ∀𝑙 ∈ (0..^(#‘𝐹))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}) |
100 | 99 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((#‘𝐹) ∈
ℕ0 ∧ 𝐹:(1...(#‘𝐹))⟶dom 𝐸) → (∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → ∀𝑙 ∈ (0..^(#‘𝐹))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})) |
101 | 100 | expcom 450 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐹:(1...(#‘𝐹))⟶dom 𝐸 → ((#‘𝐹) ∈ ℕ0 →
(∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → ∀𝑙 ∈ (0..^(#‘𝐹))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))) |
102 | 58, 101 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 → ((#‘𝐹) ∈ ℕ0
→ (∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → ∀𝑙 ∈ (0..^(#‘𝐹))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))) |
103 | 102 | imp 444 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0)
→ (∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → ∀𝑙 ∈ (0..^(#‘𝐹))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})) |
104 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((#‘𝐺) =
(#‘𝐹) →
(0..^(#‘𝐺)) =
(0..^(#‘𝐹))) |
105 | 104 | raleqdv 3121 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((#‘𝐺) =
(#‘𝐹) →
(∀𝑙 ∈
(0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))} ↔ ∀𝑙 ∈ (0..^(#‘𝐹))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})) |
106 | 105 | imbi2d 329 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((#‘𝐺) =
(#‘𝐹) →
((∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}) ↔ (∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → ∀𝑙 ∈ (0..^(#‘𝐹))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))) |
107 | 103, 106 | syl5ibr 235 |
. . . . . . . . . . . . . . . . . . 19
⊢
((#‘𝐺) =
(#‘𝐹) → ((𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0)
→ (∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))) |
108 | 107 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐺) = (#‘𝐹)) → ((𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0)
→ (∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))) |
109 | 108 | imp31 447 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐺) = (#‘𝐹)) ∧ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0))
∧ ∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) → ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}) |
110 | 109 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐺) = (#‘𝐹)) ∧ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0))
∧ ∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}) |
111 | 51, 57, 110 | 3jca 1235 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐺) = (#‘𝐹)) ∧ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0))
∧ ∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) → ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})) |
112 | 111 | exp31 628 |
. . . . . . . . . . . . . 14
⊢ (((𝐺:(0..^(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐺) = (#‘𝐹)) ∧ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0))
→ (∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})))) |
113 | 39, 112 | mpancom 700 |
. . . . . . . . . . . . 13
⊢ ((𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0)
→ (∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})))) |
114 | 113 | a1i 11 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 𝑛 → ((𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈ ℕ0)
→ (∀𝑘 ∈
(1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))))) |
115 | | oveq2 6557 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = (#‘𝐹) → (1...𝑛) = (1...(#‘𝐹))) |
116 | 115 | eqcoms 2618 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 𝑛 → (1...𝑛) = (1...(#‘𝐹))) |
117 | | f1oeq2 6041 |
. . . . . . . . . . . . . 14
⊢
((1...𝑛) =
(1...(#‘𝐹)) →
(𝐹:(1...𝑛)–1-1-onto→dom
𝐸 ↔ 𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸)) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 𝑛 → (𝐹:(1...𝑛)–1-1-onto→dom
𝐸 ↔ 𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸)) |
119 | | eleq1 2676 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = (#‘𝐹) → (𝑛 ∈ ℕ0 ↔
(#‘𝐹) ∈
ℕ0)) |
120 | 119 | eqcoms 2618 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 𝑛 → (𝑛 ∈ ℕ0 ↔
(#‘𝐹) ∈
ℕ0)) |
121 | 118, 120 | anbi12d 743 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 𝑛 → ((𝐹:(1...𝑛)–1-1-onto→dom
𝐸 ∧ 𝑛 ∈ ℕ0) ↔ (𝐹:(1...(#‘𝐹))–1-1-onto→dom
𝐸 ∧ (#‘𝐹) ∈
ℕ0))) |
122 | 116 | raleqdv 3121 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 𝑛 → (∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} ↔ ∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})) |
123 | | oveq2 6557 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = (#‘𝐹) → (0...𝑛) = (0...(#‘𝐹))) |
124 | 123 | eqcoms 2618 |
. . . . . . . . . . . . . . 15
⊢
((#‘𝐹) = 𝑛 → (0...𝑛) = (0...(#‘𝐹))) |
125 | 124 | feq2d 5944 |
. . . . . . . . . . . . . 14
⊢
((#‘𝐹) = 𝑛 → (𝑃:(0...𝑛)⟶𝑉 ↔ 𝑃:(0...(#‘𝐹))⟶𝑉)) |
126 | 125 | imbi1d 330 |
. . . . . . . . . . . . 13
⊢
((#‘𝐹) = 𝑛 → ((𝑃:(0...𝑛)⟶𝑉 → ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})) ↔ (𝑃:(0...(#‘𝐹))⟶𝑉 → ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})))) |
127 | 122, 126 | imbi12d 333 |
. . . . . . . . . . . 12
⊢
((#‘𝐹) = 𝑛 → ((∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → (𝑃:(0...𝑛)⟶𝑉 → ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))) ↔ (∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → (𝑃:(0...(#‘𝐹))⟶𝑉 → ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))))) |
128 | 114, 121,
127 | 3imtr4d 282 |
. . . . . . . . . . 11
⊢
((#‘𝐹) = 𝑛 → ((𝐹:(1...𝑛)–1-1-onto→dom
𝐸 ∧ 𝑛 ∈ ℕ0) →
(∀𝑘 ∈
(1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → (𝑃:(0...𝑛)⟶𝑉 → ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))))) |
129 | 14, 128 | mpcom 37 |
. . . . . . . . . 10
⊢ ((𝐹:(1...𝑛)–1-1-onto→dom
𝐸 ∧ 𝑛 ∈ ℕ0) →
(∀𝑘 ∈
(1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → (𝑃:(0...𝑛)⟶𝑉 → ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})))) |
130 | 129 | ex 449 |
. . . . . . . . 9
⊢ (𝐹:(1...𝑛)–1-1-onto→dom
𝐸 → (𝑛 ∈ ℕ0
→ (∀𝑘 ∈
(1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → (𝑃:(0...𝑛)⟶𝑉 → ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))))) |
131 | 130 | com24 93 |
. . . . . . . 8
⊢ (𝐹:(1...𝑛)–1-1-onto→dom
𝐸 → (𝑃:(0...𝑛)⟶𝑉 → (∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → (𝑛 ∈ ℕ0 → ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))))) |
132 | 131 | 3imp 1249 |
. . . . . . 7
⊢ ((𝐹:(1...𝑛)–1-1-onto→dom
𝐸 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) → (𝑛 ∈ ℕ0 → ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))) |
133 | 132 | com12 32 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
→ ((𝐹:(1...𝑛)–1-1-onto→dom
𝐸 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) → ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))) |
134 | 133 | rexlimiv 3009 |
. . . . 5
⊢
(∃𝑛 ∈
ℕ0 (𝐹:(1...𝑛)–1-1-onto→dom
𝐸 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) → ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})) |
135 | 134 | adantl 481 |
. . . 4
⊢ ((𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto→dom
𝐸 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})) → ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))})) |
136 | 135 | a1i 11 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐺 ∈ V ∧ 𝑃 ∈ V)) → ((𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto→dom
𝐸 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})) → ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))) |
137 | | eqid 2610 |
. . . 4
⊢ dom 𝐸 = dom 𝐸 |
138 | | iseupa 26492 |
. . . 4
⊢ (dom
𝐸 = dom 𝐸 → (𝐹(𝑉 EulPaths 𝐸)𝑃 ↔ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto→dom
𝐸 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})))) |
139 | 137, 138 | mp1i 13 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐺 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 EulPaths 𝐸)𝑃 ↔ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto→dom
𝐸 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})))) |
140 | | istrl 26067 |
. . 3
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐺 ∈ V ∧ 𝑃 ∈ V)) → (𝐺(𝑉 Trails 𝐸)𝑃 ↔ ((𝐺 ∈ Word dom 𝐸 ∧ Fun ◡𝐺) ∧ 𝑃:(0...(#‘𝐺))⟶𝑉 ∧ ∀𝑙 ∈ (0..^(#‘𝐺))(𝐸‘(𝐺‘𝑙)) = {(𝑃‘𝑙), (𝑃‘(𝑙 + 1))}))) |
141 | 136, 139,
140 | 3imtr4d 282 |
. 2
⊢ (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐺 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 EulPaths 𝐸)𝑃 → 𝐺(𝑉 Trails 𝐸)𝑃)) |
142 | 10, 141 | mpcom 37 |
1
⊢ (𝐹(𝑉 EulPaths 𝐸)𝑃 → 𝐺(𝑉 Trails 𝐸)𝑃) |