Step |
Hyp |
Ref |
Expression |
1 |
|
eulerpathpr.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
3 |
|
simpl |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ) → 𝐺 ∈ UPGraph ) |
4 |
|
upgruhgr |
⊢ ( 𝐺 ∈ UPGraph → 𝐺 ∈ UHGraph ) |
5 |
2
|
uhgrfun |
⊢ ( 𝐺 ∈ UHGraph → Fun ( iEdg ‘ 𝐺 ) ) |
6 |
4 5
|
syl |
⊢ ( 𝐺 ∈ UPGraph → Fun ( iEdg ‘ 𝐺 ) ) |
7 |
6
|
adantr |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ) → Fun ( iEdg ‘ 𝐺 ) ) |
8 |
|
simpr |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ) → 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ) |
9 |
1 2 3 7 8
|
eupth2 |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) ) |
10 |
9
|
3adant3 |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ∧ 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) ) |
11 |
|
crctprop |
⊢ ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ∧ ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) ) |
12 |
11
|
simprd |
⊢ ( 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) |
13 |
12
|
3ad2ant3 |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ∧ 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) ) |
14 |
13
|
iftrued |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ∧ 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) = ∅ ) |
15 |
14
|
eqeq2d |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ∧ 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → ( { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) ↔ { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } = ∅ ) ) |
16 |
|
rabeq0 |
⊢ ( { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } = ∅ ↔ ∀ 𝑥 ∈ 𝑉 ¬ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) |
17 |
|
notnotr |
⊢ ( ¬ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) → 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) |
18 |
17
|
ralimi |
⊢ ( ∀ 𝑥 ∈ 𝑉 ¬ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝑉 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) |
19 |
16 18
|
sylbi |
⊢ ( { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } = ∅ → ∀ 𝑥 ∈ 𝑉 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) |
20 |
15 19
|
syl6bi |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ∧ 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → ( { 𝑥 ∈ 𝑉 ∣ ¬ 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) } = if ( ( 𝑃 ‘ 0 ) = ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) , ∅ , { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ ( ♯ ‘ 𝐹 ) ) } ) → ∀ 𝑥 ∈ 𝑉 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) ) |
21 |
10 20
|
mpd |
⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐹 ( EulerPaths ‘ 𝐺 ) 𝑃 ∧ 𝐹 ( Circuits ‘ 𝐺 ) 𝑃 ) → ∀ 𝑥 ∈ 𝑉 2 ∥ ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) |