Step |
Hyp |
Ref |
Expression |
1 |
|
vtxdginducedm1.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
vtxdginducedm1.e |
⊢ 𝐸 = ( iEdg ‘ 𝐺 ) |
3 |
|
vtxdginducedm1.k |
⊢ 𝐾 = ( 𝑉 ∖ { 𝑁 } ) |
4 |
|
vtxdginducedm1.i |
⊢ 𝐼 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∉ ( 𝐸 ‘ 𝑖 ) } |
5 |
|
vtxdginducedm1.p |
⊢ 𝑃 = ( 𝐸 ↾ 𝐼 ) |
6 |
|
vtxdginducedm1.s |
⊢ 𝑆 = 〈 𝐾 , 𝑃 〉 |
7 |
|
vtxdginducedm1.j |
⊢ 𝐽 = { 𝑖 ∈ dom 𝐸 ∣ 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) } |
8 |
|
fveq2 |
⊢ ( 𝑖 = 𝑘 → ( 𝐸 ‘ 𝑖 ) = ( 𝐸 ‘ 𝑘 ) ) |
9 |
8
|
eleq2d |
⊢ ( 𝑖 = 𝑘 → ( 𝑁 ∈ ( 𝐸 ‘ 𝑖 ) ↔ 𝑁 ∈ ( 𝐸 ‘ 𝑘 ) ) ) |
10 |
9 7
|
elrab2 |
⊢ ( 𝑘 ∈ 𝐽 ↔ ( 𝑘 ∈ dom 𝐸 ∧ 𝑁 ∈ ( 𝐸 ‘ 𝑘 ) ) ) |
11 |
|
eldifsn |
⊢ ( 𝑊 ∈ ( 𝑉 ∖ { 𝑁 } ) ↔ ( 𝑊 ∈ 𝑉 ∧ 𝑊 ≠ 𝑁 ) ) |
12 |
|
df-ne |
⊢ ( 𝑊 ≠ 𝑁 ↔ ¬ 𝑊 = 𝑁 ) |
13 |
|
eleq2 |
⊢ ( ( 𝐸 ‘ 𝑘 ) = { 𝑊 } → ( 𝑁 ∈ ( 𝐸 ‘ 𝑘 ) ↔ 𝑁 ∈ { 𝑊 } ) ) |
14 |
|
elsni |
⊢ ( 𝑁 ∈ { 𝑊 } → 𝑁 = 𝑊 ) |
15 |
14
|
eqcomd |
⊢ ( 𝑁 ∈ { 𝑊 } → 𝑊 = 𝑁 ) |
16 |
13 15
|
syl6bi |
⊢ ( ( 𝐸 ‘ 𝑘 ) = { 𝑊 } → ( 𝑁 ∈ ( 𝐸 ‘ 𝑘 ) → 𝑊 = 𝑁 ) ) |
17 |
16
|
com12 |
⊢ ( 𝑁 ∈ ( 𝐸 ‘ 𝑘 ) → ( ( 𝐸 ‘ 𝑘 ) = { 𝑊 } → 𝑊 = 𝑁 ) ) |
18 |
17
|
con3rr3 |
⊢ ( ¬ 𝑊 = 𝑁 → ( 𝑁 ∈ ( 𝐸 ‘ 𝑘 ) → ¬ ( 𝐸 ‘ 𝑘 ) = { 𝑊 } ) ) |
19 |
12 18
|
sylbi |
⊢ ( 𝑊 ≠ 𝑁 → ( 𝑁 ∈ ( 𝐸 ‘ 𝑘 ) → ¬ ( 𝐸 ‘ 𝑘 ) = { 𝑊 } ) ) |
20 |
11 19
|
simplbiim |
⊢ ( 𝑊 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( 𝑁 ∈ ( 𝐸 ‘ 𝑘 ) → ¬ ( 𝐸 ‘ 𝑘 ) = { 𝑊 } ) ) |
21 |
20
|
com12 |
⊢ ( 𝑁 ∈ ( 𝐸 ‘ 𝑘 ) → ( 𝑊 ∈ ( 𝑉 ∖ { 𝑁 } ) → ¬ ( 𝐸 ‘ 𝑘 ) = { 𝑊 } ) ) |
22 |
10 21
|
simplbiim |
⊢ ( 𝑘 ∈ 𝐽 → ( 𝑊 ∈ ( 𝑉 ∖ { 𝑁 } ) → ¬ ( 𝐸 ‘ 𝑘 ) = { 𝑊 } ) ) |
23 |
22
|
impcom |
⊢ ( ( 𝑊 ∈ ( 𝑉 ∖ { 𝑁 } ) ∧ 𝑘 ∈ 𝐽 ) → ¬ ( 𝐸 ‘ 𝑘 ) = { 𝑊 } ) |
24 |
23
|
ralrimiva |
⊢ ( 𝑊 ∈ ( 𝑉 ∖ { 𝑁 } ) → ∀ 𝑘 ∈ 𝐽 ¬ ( 𝐸 ‘ 𝑘 ) = { 𝑊 } ) |
25 |
|
rabeq0 |
⊢ ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑊 } } = ∅ ↔ ∀ 𝑘 ∈ 𝐽 ¬ ( 𝐸 ‘ 𝑘 ) = { 𝑊 } ) |
26 |
24 25
|
sylibr |
⊢ ( 𝑊 ∈ ( 𝑉 ∖ { 𝑁 } ) → { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑊 } } = ∅ ) |
27 |
2
|
fvexi |
⊢ 𝐸 ∈ V |
28 |
27
|
dmex |
⊢ dom 𝐸 ∈ V |
29 |
7 28
|
rab2ex |
⊢ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑊 } } ∈ V |
30 |
|
hasheq0 |
⊢ ( { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑊 } } ∈ V → ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑊 } } ) = 0 ↔ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑊 } } = ∅ ) ) |
31 |
29 30
|
ax-mp |
⊢ ( ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑊 } } ) = 0 ↔ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑊 } } = ∅ ) |
32 |
26 31
|
sylibr |
⊢ ( 𝑊 ∈ ( 𝑉 ∖ { 𝑁 } ) → ( ♯ ‘ { 𝑘 ∈ 𝐽 ∣ ( 𝐸 ‘ 𝑘 ) = { 𝑊 } } ) = 0 ) |