Step | Hyp | Ref
| Expression |
1 | | eupares.g |
. . . . 5
⊢ (𝜑 → 𝐺(𝑉 EulPaths 𝐸)𝑃) |
2 | | eupagra 26493 |
. . . . 5
⊢ (𝐺(𝑉 EulPaths 𝐸)𝑃 → 𝑉 UMGrph 𝐸) |
3 | 1, 2 | syl 17 |
. . . 4
⊢ (𝜑 → 𝑉 UMGrph 𝐸) |
4 | | umgrares 25853 |
. . . 4
⊢ (𝑉 UMGrph 𝐸 → 𝑉 UMGrph (𝐸 ↾ (𝐺 “ (1...𝑁)))) |
5 | 3, 4 | syl 17 |
. . 3
⊢ (𝜑 → 𝑉 UMGrph (𝐸 ↾ (𝐺 “ (1...𝑁)))) |
6 | | eupares.f |
. . 3
⊢ 𝐹 = (𝐸 ↾ (𝐺 “ (1...𝑁))) |
7 | 5, 6 | syl6breqr 4625 |
. 2
⊢ (𝜑 → 𝑉 UMGrph 𝐹) |
8 | | eupares.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈ (0...(#‘𝐺))) |
9 | | elfznn0 12302 |
. . . 4
⊢ (𝑁 ∈ (0...(#‘𝐺)) → 𝑁 ∈
ℕ0) |
10 | 8, 9 | syl 17 |
. . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
11 | | umgraf2 25846 |
. . . . . . . . 9
⊢ (𝑉 UMGrph 𝐸 → 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) |
12 | 3, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}) |
13 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} → 𝐸 Fn dom 𝐸) |
14 | 12, 13 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐸 Fn dom 𝐸) |
15 | | eupaf1o 26497 |
. . . . . . 7
⊢ ((𝐺(𝑉 EulPaths 𝐸)𝑃 ∧ 𝐸 Fn dom 𝐸) → 𝐺:(1...(#‘𝐺))–1-1-onto→dom
𝐸) |
16 | 1, 14, 15 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → 𝐺:(1...(#‘𝐺))–1-1-onto→dom
𝐸) |
17 | | f1of1 6049 |
. . . . . 6
⊢ (𝐺:(1...(#‘𝐺))–1-1-onto→dom
𝐸 → 𝐺:(1...(#‘𝐺))–1-1→dom 𝐸) |
18 | 16, 17 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐺:(1...(#‘𝐺))–1-1→dom 𝐸) |
19 | | elfzuz3 12210 |
. . . . . . 7
⊢ (𝑁 ∈ (0...(#‘𝐺)) → (#‘𝐺) ∈
(ℤ≥‘𝑁)) |
20 | 8, 19 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘𝐺) ∈ (ℤ≥‘𝑁)) |
21 | | fzss2 12252 |
. . . . . 6
⊢
((#‘𝐺) ∈
(ℤ≥‘𝑁) → (1...𝑁) ⊆ (1...(#‘𝐺))) |
22 | 20, 21 | syl 17 |
. . . . 5
⊢ (𝜑 → (1...𝑁) ⊆ (1...(#‘𝐺))) |
23 | | f1ores 6064 |
. . . . 5
⊢ ((𝐺:(1...(#‘𝐺))–1-1→dom 𝐸 ∧ (1...𝑁) ⊆ (1...(#‘𝐺))) → (𝐺 ↾ (1...𝑁)):(1...𝑁)–1-1-onto→(𝐺 “ (1...𝑁))) |
24 | 18, 22, 23 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝐺 ↾ (1...𝑁)):(1...𝑁)–1-1-onto→(𝐺 “ (1...𝑁))) |
25 | | eupares.h |
. . . . 5
⊢ 𝐻 = (𝐺 ↾ (1...𝑁)) |
26 | | f1oeq1 6040 |
. . . . 5
⊢ (𝐻 = (𝐺 ↾ (1...𝑁)) → (𝐻:(1...𝑁)–1-1-onto→(𝐺 “ (1...𝑁)) ↔ (𝐺 ↾ (1...𝑁)):(1...𝑁)–1-1-onto→(𝐺 “ (1...𝑁)))) |
27 | 25, 26 | ax-mp 5 |
. . . 4
⊢ (𝐻:(1...𝑁)–1-1-onto→(𝐺 “ (1...𝑁)) ↔ (𝐺 ↾ (1...𝑁)):(1...𝑁)–1-1-onto→(𝐺 “ (1...𝑁))) |
28 | 24, 27 | sylibr 223 |
. . 3
⊢ (𝜑 → 𝐻:(1...𝑁)–1-1-onto→(𝐺 “ (1...𝑁))) |
29 | | eupapf 26499 |
. . . . . 6
⊢ (𝐺(𝑉 EulPaths 𝐸)𝑃 → 𝑃:(0...(#‘𝐺))⟶𝑉) |
30 | 1, 29 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑃:(0...(#‘𝐺))⟶𝑉) |
31 | | fzss2 12252 |
. . . . . 6
⊢
((#‘𝐺) ∈
(ℤ≥‘𝑁) → (0...𝑁) ⊆ (0...(#‘𝐺))) |
32 | 20, 31 | syl 17 |
. . . . 5
⊢ (𝜑 → (0...𝑁) ⊆ (0...(#‘𝐺))) |
33 | 30, 32 | fssresd 5984 |
. . . 4
⊢ (𝜑 → (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶𝑉) |
34 | | eupares.q |
. . . . 5
⊢ 𝑄 = (𝑃 ↾ (0...𝑁)) |
35 | 34 | feq1i 5949 |
. . . 4
⊢ (𝑄:(0...𝑁)⟶𝑉 ↔ (𝑃 ↾ (0...𝑁)):(0...𝑁)⟶𝑉) |
36 | 33, 35 | sylibr 223 |
. . 3
⊢ (𝜑 → 𝑄:(0...𝑁)⟶𝑉) |
37 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → 𝐺(𝑉 EulPaths 𝐸)𝑃) |
38 | 22 | sselda 3568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ (1...(#‘𝐺))) |
39 | | eupaseg 26500 |
. . . . . 6
⊢ ((𝐺(𝑉 EulPaths 𝐸)𝑃 ∧ 𝑘 ∈ (1...(#‘𝐺))) → (𝐸‘(𝐺‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) |
40 | 37, 38, 39 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝐸‘(𝐺‘𝑘)) = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) |
41 | 25 | fveq1i 6104 |
. . . . . . . 8
⊢ (𝐻‘𝑘) = ((𝐺 ↾ (1...𝑁))‘𝑘) |
42 | | fvres 6117 |
. . . . . . . . 9
⊢ (𝑘 ∈ (1...𝑁) → ((𝐺 ↾ (1...𝑁))‘𝑘) = (𝐺‘𝑘)) |
43 | 42 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → ((𝐺 ↾ (1...𝑁))‘𝑘) = (𝐺‘𝑘)) |
44 | 41, 43 | syl5eq 2656 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝐻‘𝑘) = (𝐺‘𝑘)) |
45 | 44 | fveq2d 6107 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝐹‘(𝐻‘𝑘)) = (𝐹‘(𝐺‘𝑘))) |
46 | 6 | fveq1i 6104 |
. . . . . . 7
⊢ (𝐹‘(𝐺‘𝑘)) = ((𝐸 ↾ (𝐺 “ (1...𝑁)))‘(𝐺‘𝑘)) |
47 | | f1ofun 6052 |
. . . . . . . . . . 11
⊢ (𝐺:(1...(#‘𝐺))–1-1-onto→dom
𝐸 → Fun 𝐺) |
48 | 16, 47 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → Fun 𝐺) |
49 | | f1of 6050 |
. . . . . . . . . . . 12
⊢ (𝐺:(1...(#‘𝐺))–1-1-onto→dom
𝐸 → 𝐺:(1...(#‘𝐺))⟶dom 𝐸) |
50 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝐺:(1...(#‘𝐺))⟶dom 𝐸 → dom 𝐺 = (1...(#‘𝐺))) |
51 | 16, 49, 50 | 3syl 18 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐺 = (1...(#‘𝐺))) |
52 | 22, 51 | sseqtr4d 3605 |
. . . . . . . . . 10
⊢ (𝜑 → (1...𝑁) ⊆ dom 𝐺) |
53 | | funfvima2 6397 |
. . . . . . . . . 10
⊢ ((Fun
𝐺 ∧ (1...𝑁) ⊆ dom 𝐺) → (𝑘 ∈ (1...𝑁) → (𝐺‘𝑘) ∈ (𝐺 “ (1...𝑁)))) |
54 | 48, 52, 53 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝑘 ∈ (1...𝑁) → (𝐺‘𝑘) ∈ (𝐺 “ (1...𝑁)))) |
55 | 54 | imp 444 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝐺‘𝑘) ∈ (𝐺 “ (1...𝑁))) |
56 | | fvres 6117 |
. . . . . . . 8
⊢ ((𝐺‘𝑘) ∈ (𝐺 “ (1...𝑁)) → ((𝐸 ↾ (𝐺 “ (1...𝑁)))‘(𝐺‘𝑘)) = (𝐸‘(𝐺‘𝑘))) |
57 | 55, 56 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → ((𝐸 ↾ (𝐺 “ (1...𝑁)))‘(𝐺‘𝑘)) = (𝐸‘(𝐺‘𝑘))) |
58 | 46, 57 | syl5eq 2656 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝐹‘(𝐺‘𝑘)) = (𝐸‘(𝐺‘𝑘))) |
59 | 45, 58 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝐹‘(𝐻‘𝑘)) = (𝐸‘(𝐺‘𝑘))) |
60 | | elfznn 12241 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ) |
61 | 60 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℕ) |
62 | | nnm1nn0 11211 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈
ℕ0) |
63 | 61, 62 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 − 1) ∈
ℕ0) |
64 | | nn0uz 11598 |
. . . . . . . . 9
⊢
ℕ0 = (ℤ≥‘0) |
65 | 63, 64 | syl6eleq 2698 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 − 1) ∈
(ℤ≥‘0)) |
66 | 61 | nncnd 10913 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ ℂ) |
67 | | ax-1cn 9873 |
. . . . . . . . . 10
⊢ 1 ∈
ℂ |
68 | | npcan 10169 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝑘 −
1) + 1) = 𝑘) |
69 | 66, 67, 68 | sylancl 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → ((𝑘 − 1) + 1) = 𝑘) |
70 | | 1e0p1 11428 |
. . . . . . . . . . . 12
⊢ 1 = (0 +
1) |
71 | 70 | oveq1i 6559 |
. . . . . . . . . . 11
⊢
(1...𝑁) = ((0 +
1)...𝑁) |
72 | | 0z 11265 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℤ |
73 | | fzp1ss 12262 |
. . . . . . . . . . . 12
⊢ (0 ∈
ℤ → ((0 + 1)...𝑁) ⊆ (0...𝑁)) |
74 | 72, 73 | mp1i 13 |
. . . . . . . . . . 11
⊢ (𝜑 → ((0 + 1)...𝑁) ⊆ (0...𝑁)) |
75 | 71, 74 | syl5eqss 3612 |
. . . . . . . . . 10
⊢ (𝜑 → (1...𝑁) ⊆ (0...𝑁)) |
76 | 75 | sselda 3568 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 ∈ (0...𝑁)) |
77 | 69, 76 | eqeltrd 2688 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → ((𝑘 − 1) + 1) ∈ (0...𝑁)) |
78 | | peano2fzr 12225 |
. . . . . . . 8
⊢ (((𝑘 − 1) ∈
(ℤ≥‘0) ∧ ((𝑘 − 1) + 1) ∈ (0...𝑁)) → (𝑘 − 1) ∈ (0...𝑁)) |
79 | 65, 77, 78 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 − 1) ∈ (0...𝑁)) |
80 | 34 | fveq1i 6104 |
. . . . . . . 8
⊢ (𝑄‘(𝑘 − 1)) = ((𝑃 ↾ (0...𝑁))‘(𝑘 − 1)) |
81 | | fvres 6117 |
. . . . . . . 8
⊢ ((𝑘 − 1) ∈ (0...𝑁) → ((𝑃 ↾ (0...𝑁))‘(𝑘 − 1)) = (𝑃‘(𝑘 − 1))) |
82 | 80, 81 | syl5eq 2656 |
. . . . . . 7
⊢ ((𝑘 − 1) ∈ (0...𝑁) → (𝑄‘(𝑘 − 1)) = (𝑃‘(𝑘 − 1))) |
83 | 79, 82 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝑄‘(𝑘 − 1)) = (𝑃‘(𝑘 − 1))) |
84 | 34 | fveq1i 6104 |
. . . . . . . 8
⊢ (𝑄‘𝑘) = ((𝑃 ↾ (0...𝑁))‘𝑘) |
85 | | fvres 6117 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → ((𝑃 ↾ (0...𝑁))‘𝑘) = (𝑃‘𝑘)) |
86 | 84, 85 | syl5eq 2656 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑁) → (𝑄‘𝑘) = (𝑃‘𝑘)) |
87 | 76, 86 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝑄‘𝑘) = (𝑃‘𝑘)) |
88 | 83, 87 | preq12d 4220 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)} = {(𝑃‘(𝑘 − 1)), (𝑃‘𝑘)}) |
89 | 40, 59, 88 | 3eqtr4d 2654 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (1...𝑁)) → (𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)}) |
90 | 89 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑘 ∈ (1...𝑁)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)}) |
91 | | oveq2 6557 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (1...𝑛) = (1...𝑁)) |
92 | | f1oeq2 6041 |
. . . . . 6
⊢
((1...𝑛) =
(1...𝑁) → (𝐻:(1...𝑛)–1-1-onto→(𝐺 “ (1...𝑁)) ↔ 𝐻:(1...𝑁)–1-1-onto→(𝐺 “ (1...𝑁)))) |
93 | 91, 92 | syl 17 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝐻:(1...𝑛)–1-1-onto→(𝐺 “ (1...𝑁)) ↔ 𝐻:(1...𝑁)–1-1-onto→(𝐺 “ (1...𝑁)))) |
94 | | oveq2 6557 |
. . . . . 6
⊢ (𝑛 = 𝑁 → (0...𝑛) = (0...𝑁)) |
95 | 94 | feq2d 5944 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑄:(0...𝑛)⟶𝑉 ↔ 𝑄:(0...𝑁)⟶𝑉)) |
96 | 91 | raleqdv 3121 |
. . . . 5
⊢ (𝑛 = 𝑁 → (∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)} ↔ ∀𝑘 ∈ (1...𝑁)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)})) |
97 | 93, 95, 96 | 3anbi123d 1391 |
. . . 4
⊢ (𝑛 = 𝑁 → ((𝐻:(1...𝑛)–1-1-onto→(𝐺 “ (1...𝑁)) ∧ 𝑄:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)}) ↔ (𝐻:(1...𝑁)–1-1-onto→(𝐺 “ (1...𝑁)) ∧ 𝑄:(0...𝑁)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑁)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)}))) |
98 | 97 | rspcev 3282 |
. . 3
⊢ ((𝑁 ∈ ℕ0
∧ (𝐻:(1...𝑁)–1-1-onto→(𝐺 “ (1...𝑁)) ∧ 𝑄:(0...𝑁)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑁)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)})) → ∃𝑛 ∈ ℕ0 (𝐻:(1...𝑛)–1-1-onto→(𝐺 “ (1...𝑁)) ∧ 𝑄:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)})) |
99 | 10, 28, 36, 90, 98 | syl13anc 1320 |
. 2
⊢ (𝜑 → ∃𝑛 ∈ ℕ0 (𝐻:(1...𝑛)–1-1-onto→(𝐺 “ (1...𝑁)) ∧ 𝑄:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)})) |
100 | 6 | dmeqi 5247 |
. . . . 5
⊢ dom 𝐹 = dom (𝐸 ↾ (𝐺 “ (1...𝑁))) |
101 | | dmres 5339 |
. . . . 5
⊢ dom
(𝐸 ↾ (𝐺 “ (1...𝑁))) = ((𝐺 “ (1...𝑁)) ∩ dom 𝐸) |
102 | 100, 101 | eqtri 2632 |
. . . 4
⊢ dom 𝐹 = ((𝐺 “ (1...𝑁)) ∩ dom 𝐸) |
103 | | imassrn 5396 |
. . . . . 6
⊢ (𝐺 “ (1...𝑁)) ⊆ ran 𝐺 |
104 | | f1ofo 6057 |
. . . . . . 7
⊢ (𝐺:(1...(#‘𝐺))–1-1-onto→dom
𝐸 → 𝐺:(1...(#‘𝐺))–onto→dom 𝐸) |
105 | | forn 6031 |
. . . . . . 7
⊢ (𝐺:(1...(#‘𝐺))–onto→dom 𝐸 → ran 𝐺 = dom 𝐸) |
106 | 16, 104, 105 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → ran 𝐺 = dom 𝐸) |
107 | 103, 106 | syl5sseq 3616 |
. . . . 5
⊢ (𝜑 → (𝐺 “ (1...𝑁)) ⊆ dom 𝐸) |
108 | | df-ss 3554 |
. . . . 5
⊢ ((𝐺 “ (1...𝑁)) ⊆ dom 𝐸 ↔ ((𝐺 “ (1...𝑁)) ∩ dom 𝐸) = (𝐺 “ (1...𝑁))) |
109 | 107, 108 | sylib 207 |
. . . 4
⊢ (𝜑 → ((𝐺 “ (1...𝑁)) ∩ dom 𝐸) = (𝐺 “ (1...𝑁))) |
110 | 102, 109 | syl5eq 2656 |
. . 3
⊢ (𝜑 → dom 𝐹 = (𝐺 “ (1...𝑁))) |
111 | | iseupa 26492 |
. . 3
⊢ (dom
𝐹 = (𝐺 “ (1...𝑁)) → (𝐻(𝑉 EulPaths 𝐹)𝑄 ↔ (𝑉 UMGrph 𝐹 ∧ ∃𝑛 ∈ ℕ0 (𝐻:(1...𝑛)–1-1-onto→(𝐺 “ (1...𝑁)) ∧ 𝑄:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)})))) |
112 | 110, 111 | syl 17 |
. 2
⊢ (𝜑 → (𝐻(𝑉 EulPaths 𝐹)𝑄 ↔ (𝑉 UMGrph 𝐹 ∧ ∃𝑛 ∈ ℕ0 (𝐻:(1...𝑛)–1-1-onto→(𝐺 “ (1...𝑁)) ∧ 𝑄:(0...𝑛)⟶𝑉 ∧ ∀𝑘 ∈ (1...𝑛)(𝐹‘(𝐻‘𝑘)) = {(𝑄‘(𝑘 − 1)), (𝑄‘𝑘)})))) |
113 | 7, 99, 112 | mpbir2and 959 |
1
⊢ (𝜑 → 𝐻(𝑉 EulPaths 𝐹)𝑄) |