Step | Hyp | Ref
| Expression |
1 | | releupa 26491 |
. . . . 5
⊢ Rel
(𝑉 EulPaths 𝐸) |
2 | | reldm0 5264 |
. . . . 5
⊢ (Rel
(𝑉 EulPaths 𝐸) → ((𝑉 EulPaths 𝐸) = ∅ ↔ dom (𝑉 EulPaths 𝐸) = ∅)) |
3 | 1, 2 | ax-mp 5 |
. . . 4
⊢ ((𝑉 EulPaths 𝐸) = ∅ ↔ dom (𝑉 EulPaths 𝐸) = ∅) |
4 | 3 | necon3bii 2834 |
. . 3
⊢ ((𝑉 EulPaths 𝐸) ≠ ∅ ↔ dom (𝑉 EulPaths 𝐸) ≠ ∅) |
5 | | n0 3890 |
. . 3
⊢ (dom
(𝑉 EulPaths 𝐸) ≠ ∅ ↔
∃𝑓 𝑓 ∈ dom (𝑉 EulPaths 𝐸)) |
6 | 4, 5 | bitri 263 |
. 2
⊢ ((𝑉 EulPaths 𝐸) ≠ ∅ ↔ ∃𝑓 𝑓 ∈ dom (𝑉 EulPaths 𝐸)) |
7 | | vex 3176 |
. . . . 5
⊢ 𝑓 ∈ V |
8 | 7 | eldm 5243 |
. . . 4
⊢ (𝑓 ∈ dom (𝑉 EulPaths 𝐸) ↔ ∃𝑝 𝑓(𝑉 EulPaths 𝐸)𝑝) |
9 | | eupagra 26493 |
. . . . . . . . 9
⊢ (𝑓(𝑉 EulPaths 𝐸)𝑝 → 𝑉 UMGrph 𝐸) |
10 | | umgraf2 25846 |
. . . . . . . . 9
⊢ (𝑉 UMGrph 𝐸 → 𝐸:dom 𝐸⟶{𝑦 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑦) ≤ 2}) |
11 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐸:dom 𝐸⟶{𝑦 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑦) ≤ 2} → 𝐸 Fn dom 𝐸) |
12 | 9, 10, 11 | 3syl 18 |
. . . . . . . 8
⊢ (𝑓(𝑉 EulPaths 𝐸)𝑝 → 𝐸 Fn dom 𝐸) |
13 | | id 22 |
. . . . . . . 8
⊢ (𝑓(𝑉 EulPaths 𝐸)𝑝 → 𝑓(𝑉 EulPaths 𝐸)𝑝) |
14 | 12, 13 | eupath2 26507 |
. . . . . . 7
⊢ (𝑓(𝑉 EulPaths 𝐸)𝑝 → {𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)} = if((𝑝‘0) = (𝑝‘(#‘𝑓)), ∅, {(𝑝‘0), (𝑝‘(#‘𝑓))})) |
15 | 14 | fveq2d 6107 |
. . . . . 6
⊢ (𝑓(𝑉 EulPaths 𝐸)𝑝 → (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) = (#‘if((𝑝‘0) = (𝑝‘(#‘𝑓)), ∅, {(𝑝‘0), (𝑝‘(#‘𝑓))}))) |
16 | | fveq2 6103 |
. . . . . . . 8
⊢ (∅
= if((𝑝‘0) = (𝑝‘(#‘𝑓)), ∅, {(𝑝‘0), (𝑝‘(#‘𝑓))}) → (#‘∅) =
(#‘if((𝑝‘0) =
(𝑝‘(#‘𝑓)), ∅, {(𝑝‘0), (𝑝‘(#‘𝑓))}))) |
17 | 16 | eleq1d 2672 |
. . . . . . 7
⊢ (∅
= if((𝑝‘0) = (𝑝‘(#‘𝑓)), ∅, {(𝑝‘0), (𝑝‘(#‘𝑓))}) → ((#‘∅) ∈ {0, 2}
↔ (#‘if((𝑝‘0) = (𝑝‘(#‘𝑓)), ∅, {(𝑝‘0), (𝑝‘(#‘𝑓))})) ∈ {0, 2})) |
18 | | fveq2 6103 |
. . . . . . . 8
⊢ ({(𝑝‘0), (𝑝‘(#‘𝑓))} = if((𝑝‘0) = (𝑝‘(#‘𝑓)), ∅, {(𝑝‘0), (𝑝‘(#‘𝑓))}) → (#‘{(𝑝‘0), (𝑝‘(#‘𝑓))}) = (#‘if((𝑝‘0) = (𝑝‘(#‘𝑓)), ∅, {(𝑝‘0), (𝑝‘(#‘𝑓))}))) |
19 | 18 | eleq1d 2672 |
. . . . . . 7
⊢ ({(𝑝‘0), (𝑝‘(#‘𝑓))} = if((𝑝‘0) = (𝑝‘(#‘𝑓)), ∅, {(𝑝‘0), (𝑝‘(#‘𝑓))}) → ((#‘{(𝑝‘0), (𝑝‘(#‘𝑓))}) ∈ {0, 2} ↔ (#‘if((𝑝‘0) = (𝑝‘(#‘𝑓)), ∅, {(𝑝‘0), (𝑝‘(#‘𝑓))})) ∈ {0, 2})) |
20 | | hash0 13019 |
. . . . . . . . 9
⊢
(#‘∅) = 0 |
21 | | c0ex 9913 |
. . . . . . . . . 10
⊢ 0 ∈
V |
22 | 21 | prid1 4241 |
. . . . . . . . 9
⊢ 0 ∈
{0, 2} |
23 | 20, 22 | eqeltri 2684 |
. . . . . . . 8
⊢
(#‘∅) ∈ {0, 2} |
24 | 23 | a1i 11 |
. . . . . . 7
⊢ ((𝑓(𝑉 EulPaths 𝐸)𝑝 ∧ (𝑝‘0) = (𝑝‘(#‘𝑓))) → (#‘∅) ∈ {0,
2}) |
25 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑓(𝑉 EulPaths 𝐸)𝑝 ∧ ¬ (𝑝‘0) = (𝑝‘(#‘𝑓))) → ¬ (𝑝‘0) = (𝑝‘(#‘𝑓))) |
26 | 25 | neqned 2789 |
. . . . . . . . 9
⊢ ((𝑓(𝑉 EulPaths 𝐸)𝑝 ∧ ¬ (𝑝‘0) = (𝑝‘(#‘𝑓))) → (𝑝‘0) ≠ (𝑝‘(#‘𝑓))) |
27 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝑝‘0) ∈
V |
28 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝑝‘(#‘𝑓)) ∈ V |
29 | | hashprgOLD 13044 |
. . . . . . . . . 10
⊢ (((𝑝‘0) ∈ V ∧ (𝑝‘(#‘𝑓)) ∈ V) → ((𝑝‘0) ≠ (𝑝‘(#‘𝑓)) ↔ (#‘{(𝑝‘0), (𝑝‘(#‘𝑓))}) = 2)) |
30 | 27, 28, 29 | mp2an 704 |
. . . . . . . . 9
⊢ ((𝑝‘0) ≠ (𝑝‘(#‘𝑓)) ↔ (#‘{(𝑝‘0), (𝑝‘(#‘𝑓))}) = 2) |
31 | 26, 30 | sylib 207 |
. . . . . . . 8
⊢ ((𝑓(𝑉 EulPaths 𝐸)𝑝 ∧ ¬ (𝑝‘0) = (𝑝‘(#‘𝑓))) → (#‘{(𝑝‘0), (𝑝‘(#‘𝑓))}) = 2) |
32 | | 2ex 10969 |
. . . . . . . . 9
⊢ 2 ∈
V |
33 | 32 | prid2 4242 |
. . . . . . . 8
⊢ 2 ∈
{0, 2} |
34 | 31, 33 | syl6eqel 2696 |
. . . . . . 7
⊢ ((𝑓(𝑉 EulPaths 𝐸)𝑝 ∧ ¬ (𝑝‘0) = (𝑝‘(#‘𝑓))) → (#‘{(𝑝‘0), (𝑝‘(#‘𝑓))}) ∈ {0, 2}) |
35 | 17, 19, 24, 34 | ifbothda 4073 |
. . . . . 6
⊢ (𝑓(𝑉 EulPaths 𝐸)𝑝 → (#‘if((𝑝‘0) = (𝑝‘(#‘𝑓)), ∅, {(𝑝‘0), (𝑝‘(#‘𝑓))})) ∈ {0, 2}) |
36 | 15, 35 | eqeltrd 2688 |
. . . . 5
⊢ (𝑓(𝑉 EulPaths 𝐸)𝑝 → (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) ∈ {0, 2}) |
37 | 36 | exlimiv 1845 |
. . . 4
⊢
(∃𝑝 𝑓(𝑉 EulPaths 𝐸)𝑝 → (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) ∈ {0, 2}) |
38 | 8, 37 | sylbi 206 |
. . 3
⊢ (𝑓 ∈ dom (𝑉 EulPaths 𝐸) → (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) ∈ {0, 2}) |
39 | 38 | exlimiv 1845 |
. 2
⊢
(∃𝑓 𝑓 ∈ dom (𝑉 EulPaths 𝐸) → (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) ∈ {0, 2}) |
40 | 6, 39 | sylbi 206 |
1
⊢ ((𝑉 EulPaths 𝐸) ≠ ∅ → (#‘{𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ((𝑉 VDeg 𝐸)‘𝑥)}) ∈ {0, 2}) |