Step |
Hyp |
Ref |
Expression |
1 |
|
eulerpathpr.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
releupth |
⊢ Rel ( EulerPaths ‘ 𝐺 ) |
3 |
|
reldm0 |
⊢ ( Rel ( EulerPaths ‘ 𝐺 ) → ( ( EulerPaths ‘ 𝐺 ) = ∅ ↔ dom ( EulerPaths ‘ 𝐺 ) = ∅ ) ) |
4 |
2 3
|
ax-mp |
⊢ ( ( EulerPaths ‘ 𝐺 ) = ∅ ↔ dom ( EulerPaths ‘ 𝐺 ) = ∅ ) |
5 |
4
|
necon3bii |
⊢ ( ( EulerPaths ‘ 𝐺 ) ≠ ∅ ↔ dom ( EulerPaths ‘ 𝐺 ) ≠ ∅ ) |
6 |
|
n0 |
⊢ ( dom ( EulerPaths ‘ 𝐺 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ dom ( EulerPaths ‘ 𝐺 ) ) |
7 |
5 6
|
bitri |
⊢ ( ( EulerPaths ‘ 𝐺 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ dom ( EulerPaths ‘ 𝐺 ) ) |
8 |
|
vex |
⊢ 𝑓 ∈ V |
9 |
8
|
eldm |
⊢ ( 𝑓 ∈ dom ( EulerPaths ‘ 𝐺 ) ↔ ∃ 𝑝 𝑓 ( EulerPaths ‘ 𝐺 ) 𝑝 ) |
10 |
1
|
eulerpathpr |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝑓 ( EulerPaths ‘ 𝐺 ) 𝑝 ) → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } ) |
11 |
10
|
expcom |
⊢ ( 𝑓 ( EulerPaths ‘ 𝐺 ) 𝑝 → ( 𝐺 ∈ UPGraph → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } ) ) |
12 |
11
|
exlimiv |
⊢ ( ∃ 𝑝 𝑓 ( EulerPaths ‘ 𝐺 ) 𝑝 → ( 𝐺 ∈ UPGraph → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } ) ) |
13 |
9 12
|
sylbi |
⊢ ( 𝑓 ∈ dom ( EulerPaths ‘ 𝐺 ) → ( 𝐺 ∈ UPGraph → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } ) ) |
14 |
13
|
exlimiv |
⊢ ( ∃ 𝑓 𝑓 ∈ dom ( EulerPaths ‘ 𝐺 ) → ( 𝐺 ∈ UPGraph → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } ) ) |
15 |
7 14
|
sylbi |
⊢ ( ( EulerPaths ‘ 𝐺 ) ≠ ∅ → ( 𝐺 ∈ UPGraph → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } ) ) |
16 |
15
|
impcom |
⊢ ( ( 𝐺 ∈ UPGraph ∧ ( EulerPaths ‘ 𝐺 ) ≠ ∅ ) → ( ♯ ‘ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } ) ∈ { 0 , 2 } ) |