Step | Hyp | Ref
| Expression |
1 | | fndm 5904 |
. . . . 5
⊢ (𝐸 Fn 𝐴 → dom 𝐸 = 𝐴) |
2 | | iseupa 26492 |
. . . . 5
⊢ (dom
𝐸 = 𝐴 → (𝐹(𝑉 EulPaths 𝐸)𝑃 ↔ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})))) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝐸 Fn 𝐴 → (𝐹(𝑉 EulPaths 𝐸)𝑃 ↔ (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})))) |
4 | 3 | biimpac 502 |
. . 3
⊢ ((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) → (𝑉 UMGrph 𝐸 ∧ ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}))) |
5 | 4 | simprd 478 |
. 2
⊢ ((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) → ∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})) |
6 | | f1ofn 6051 |
. . . . . . . . . . . . . 14
⊢ (𝐹:(1...𝑛)–1-1-onto→𝐴 → 𝐹 Fn (1...𝑛)) |
7 | 6 | ad2antll 761 |
. . . . . . . . . . . . 13
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → 𝐹 Fn (1...𝑛)) |
8 | | fzfid 12634 |
. . . . . . . . . . . . 13
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → (1...𝑛) ∈ Fin) |
9 | | fndmeng 7919 |
. . . . . . . . . . . . 13
⊢ ((𝐹 Fn (1...𝑛) ∧ (1...𝑛) ∈ Fin) → (1...𝑛) ≈ 𝐹) |
10 | 7, 8, 9 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → (1...𝑛) ≈ 𝐹) |
11 | | enfi 8061 |
. . . . . . . . . . . . . . 15
⊢
((1...𝑛) ≈
𝐹 → ((1...𝑛) ∈ Fin ↔ 𝐹 ∈ Fin)) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → ((1...𝑛) ∈ Fin ↔ 𝐹 ∈ Fin)) |
13 | 8, 12 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → 𝐹 ∈ Fin) |
14 | | hashen 12997 |
. . . . . . . . . . . . 13
⊢
(((1...𝑛) ∈ Fin
∧ 𝐹 ∈ Fin) →
((#‘(1...𝑛)) =
(#‘𝐹) ↔
(1...𝑛) ≈ 𝐹)) |
15 | 8, 13, 14 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → ((#‘(1...𝑛)) = (#‘𝐹) ↔ (1...𝑛) ≈ 𝐹)) |
16 | 10, 15 | mpbird 246 |
. . . . . . . . . . 11
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → (#‘(1...𝑛)) = (#‘𝐹)) |
17 | | hashfz1 12996 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ (#‘(1...𝑛)) =
𝑛) |
18 | 17 | ad2antrl 760 |
. . . . . . . . . . 11
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → (#‘(1...𝑛)) = 𝑛) |
19 | 16, 18 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → (#‘𝐹) = 𝑛) |
20 | | simprl 790 |
. . . . . . . . . 10
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → 𝑛 ∈ ℕ0) |
21 | 19, 20 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → (#‘𝐹) ∈
ℕ0) |
22 | 21 | a1d 25 |
. . . . . . . 8
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → (𝑃:(0...𝑛)⟶𝑉 → (#‘𝐹) ∈
ℕ0)) |
23 | | simprr 792 |
. . . . . . . . . 10
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → 𝐹:(1...𝑛)–1-1-onto→𝐴) |
24 | 19 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → (1...(#‘𝐹)) = (1...𝑛)) |
25 | | f1oeq2 6041 |
. . . . . . . . . . 11
⊢
((1...(#‘𝐹)) =
(1...𝑛) → (𝐹:(1...(#‘𝐹))–1-1-onto→𝐴 ↔ 𝐹:(1...𝑛)–1-1-onto→𝐴)) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → (𝐹:(1...(#‘𝐹))–1-1-onto→𝐴 ↔ 𝐹:(1...𝑛)–1-1-onto→𝐴)) |
27 | 23, 26 | mpbird 246 |
. . . . . . . . 9
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → 𝐹:(1...(#‘𝐹))–1-1-onto→𝐴) |
28 | 27 | a1d 25 |
. . . . . . . 8
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → (𝑃:(0...𝑛)⟶𝑉 → 𝐹:(1...(#‘𝐹))–1-1-onto→𝐴)) |
29 | 19 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → (0...(#‘𝐹)) = (0...𝑛)) |
30 | 29 | feq2d 5944 |
. . . . . . . . 9
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → (𝑃:(0...(#‘𝐹))⟶𝑉 ↔ 𝑃:(0...𝑛)⟶𝑉)) |
31 | 30 | biimprd 237 |
. . . . . . . 8
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → (𝑃:(0...𝑛)⟶𝑉 → 𝑃:(0...(#‘𝐹))⟶𝑉)) |
32 | 22, 28, 31 | 3jcad 1236 |
. . . . . . 7
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → (𝑃:(0...𝑛)⟶𝑉 → ((#‘𝐹) ∈ ℕ0 ∧ 𝐹:(1...(#‘𝐹))–1-1-onto→𝐴 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉))) |
33 | 24 | raleqdv 3121 |
. . . . . . . 8
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → (∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} ↔ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})) |
34 | 33 | biimprd 237 |
. . . . . . 7
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → (∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → ∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})) |
35 | 32, 34 | anim12d 584 |
. . . . . 6
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → ((𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) → (((#‘𝐹) ∈ ℕ0 ∧ 𝐹:(1...(#‘𝐹))–1-1-onto→𝐴 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ ∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}))) |
36 | 35 | expd 451 |
. . . . 5
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ (𝑛 ∈ ℕ0 ∧ 𝐹:(1...𝑛)–1-1-onto→𝐴)) → (𝑃:(0...𝑛)⟶𝑉 → (∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → (((#‘𝐹) ∈ ℕ0 ∧ 𝐹:(1...(#‘𝐹))–1-1-onto→𝐴 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ ∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})))) |
37 | 36 | expr 641 |
. . . 4
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ 𝑛 ∈ ℕ0) → (𝐹:(1...𝑛)–1-1-onto→𝐴 → (𝑃:(0...𝑛)⟶𝑉 → (∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)} → (((#‘𝐹) ∈ ℕ0 ∧ 𝐹:(1...(#‘𝐹))–1-1-onto→𝐴 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ ∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}))))) |
38 | 37 | 3impd 1273 |
. . 3
⊢ (((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) ∧ 𝑛 ∈ ℕ0) → ((𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) → (((#‘𝐹) ∈ ℕ0 ∧ 𝐹:(1...(#‘𝐹))–1-1-onto→𝐴 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ ∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}))) |
39 | 38 | rexlimdva 3013 |
. 2
⊢ ((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) → (∃𝑛 ∈ ℕ0 (𝐹:(1...𝑛)–1-1-onto→𝐴 ∧ 𝑃:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) → (((#‘𝐹) ∈ ℕ0 ∧ 𝐹:(1...(#‘𝐹))–1-1-onto→𝐴 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ ∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}))) |
40 | 5, 39 | mpd 15 |
1
⊢ ((𝐹(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn 𝐴) → (((#‘𝐹) ∈ ℕ0 ∧ 𝐹:(1...(#‘𝐹))–1-1-onto→𝐴 ∧ 𝑃:(0...(#‘𝐹))⟶𝑉) ∧ ∀𝑘 ∈ (1...(#‘𝐹))(𝐸‘(𝐹‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)})) |