Step |
Hyp |
Ref |
Expression |
1 |
|
1hevtxdg0.i |
⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { 〈 𝐴 , 𝐸 〉 } ) |
2 |
|
1hevtxdg0.v |
⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 ) |
3 |
|
1hevtxdg0.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑋 ) |
4 |
|
1hevtxdg0.d |
⊢ ( 𝜑 → 𝐷 ∈ 𝑉 ) |
5 |
|
1hevtxdg0.e |
⊢ ( 𝜑 → 𝐸 ∈ 𝑌 ) |
6 |
|
1hevtxdg0.n |
⊢ ( 𝜑 → 𝐷 ∉ 𝐸 ) |
7 |
|
df-nel |
⊢ ( 𝐷 ∉ 𝐸 ↔ ¬ 𝐷 ∈ 𝐸 ) |
8 |
6 7
|
sylib |
⊢ ( 𝜑 → ¬ 𝐷 ∈ 𝐸 ) |
9 |
1
|
fveq1d |
⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) = ( { 〈 𝐴 , 𝐸 〉 } ‘ 𝐴 ) ) |
10 |
|
fvsng |
⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ) → ( { 〈 𝐴 , 𝐸 〉 } ‘ 𝐴 ) = 𝐸 ) |
11 |
3 5 10
|
syl2anc |
⊢ ( 𝜑 → ( { 〈 𝐴 , 𝐸 〉 } ‘ 𝐴 ) = 𝐸 ) |
12 |
9 11
|
eqtrd |
⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) = 𝐸 ) |
13 |
8 12
|
neleqtrrd |
⊢ ( 𝜑 → ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) ) |
14 |
|
fveq2 |
⊢ ( 𝑥 = 𝐴 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) ) |
15 |
14
|
eleq2d |
⊢ ( 𝑥 = 𝐴 → ( 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) ) ) |
16 |
15
|
notbid |
⊢ ( 𝑥 = 𝐴 → ( ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) ) ) |
17 |
16
|
ralsng |
⊢ ( 𝐴 ∈ 𝑋 → ( ∀ 𝑥 ∈ { 𝐴 } ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) ) ) |
18 |
3 17
|
syl |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ { 𝐴 } ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝐴 ) ) ) |
19 |
13 18
|
mpbird |
⊢ ( 𝜑 → ∀ 𝑥 ∈ { 𝐴 } ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) |
20 |
1
|
dmeqd |
⊢ ( 𝜑 → dom ( iEdg ‘ 𝐺 ) = dom { 〈 𝐴 , 𝐸 〉 } ) |
21 |
|
dmsnopg |
⊢ ( 𝐸 ∈ 𝑌 → dom { 〈 𝐴 , 𝐸 〉 } = { 𝐴 } ) |
22 |
5 21
|
syl |
⊢ ( 𝜑 → dom { 〈 𝐴 , 𝐸 〉 } = { 𝐴 } ) |
23 |
20 22
|
eqtrd |
⊢ ( 𝜑 → dom ( iEdg ‘ 𝐺 ) = { 𝐴 } ) |
24 |
23
|
raleqdv |
⊢ ( 𝜑 → ( ∀ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ { 𝐴 } ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) |
25 |
19 24
|
mpbird |
⊢ ( 𝜑 → ∀ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) |
26 |
|
ralnex |
⊢ ( ∀ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ¬ 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ¬ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) |
27 |
25 26
|
sylib |
⊢ ( 𝜑 → ¬ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) |
28 |
2
|
eleq2d |
⊢ ( 𝜑 → ( 𝐷 ∈ ( Vtx ‘ 𝐺 ) ↔ 𝐷 ∈ 𝑉 ) ) |
29 |
4 28
|
mpbird |
⊢ ( 𝜑 → 𝐷 ∈ ( Vtx ‘ 𝐺 ) ) |
30 |
|
eqid |
⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 ) |
31 |
|
eqid |
⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 ) |
32 |
|
eqid |
⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 ) |
33 |
30 31 32
|
vtxd0nedgb |
⊢ ( 𝐷 ∈ ( Vtx ‘ 𝐺 ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐷 ) = 0 ↔ ¬ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) |
34 |
29 33
|
syl |
⊢ ( 𝜑 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐷 ) = 0 ↔ ¬ ∃ 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝐷 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) |
35 |
27 34
|
mpbird |
⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐷 ) = 0 ) |