Step |
Hyp |
Ref |
Expression |
1 |
|
vtxd0nedgb.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
vtxd0nedgb.i |
⊢ 𝐼 = ( iEdg ‘ 𝐺 ) |
3 |
|
vtxd0nedgb.d |
⊢ 𝐷 = ( VtxDeg ‘ 𝐺 ) |
4 |
3
|
fveq1i |
⊢ ( 𝐷 ‘ 𝑈 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) |
5 |
|
eqid |
⊢ dom 𝐼 = dom 𝐼 |
6 |
1 2 5
|
vtxdgval |
⊢ ( 𝑈 ∈ 𝑉 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ) +𝑒 ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ) ) ) |
7 |
4 6
|
syl5eq |
⊢ ( 𝑈 ∈ 𝑉 → ( 𝐷 ‘ 𝑈 ) = ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ) +𝑒 ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ) ) ) |
8 |
7
|
eqeq1d |
⊢ ( 𝑈 ∈ 𝑉 → ( ( 𝐷 ‘ 𝑈 ) = 0 ↔ ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ) +𝑒 ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ) ) = 0 ) ) |
9 |
2
|
fvexi |
⊢ 𝐼 ∈ V |
10 |
9
|
dmex |
⊢ dom 𝐼 ∈ V |
11 |
10
|
rabex |
⊢ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ∈ V |
12 |
|
hashxnn0 |
⊢ ( { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ∈ V → ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ) ∈ ℕ0* ) |
13 |
11 12
|
ax-mp |
⊢ ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ) ∈ ℕ0* |
14 |
10
|
rabex |
⊢ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ∈ V |
15 |
|
hashxnn0 |
⊢ ( { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ∈ V → ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ) ∈ ℕ0* ) |
16 |
14 15
|
ax-mp |
⊢ ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ) ∈ ℕ0* |
17 |
13 16
|
pm3.2i |
⊢ ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ) ∈ ℕ0* ∧ ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ) ∈ ℕ0* ) |
18 |
|
xnn0xadd0 |
⊢ ( ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ) ∈ ℕ0* ∧ ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ) ∈ ℕ0* ) → ( ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ) +𝑒 ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ) ) = 0 ↔ ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ) = 0 ∧ ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ) = 0 ) ) ) |
19 |
17 18
|
mp1i |
⊢ ( 𝑈 ∈ 𝑉 → ( ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ) +𝑒 ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ) ) = 0 ↔ ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ) = 0 ∧ ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ) = 0 ) ) ) |
20 |
|
hasheq0 |
⊢ ( { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ∈ V → ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ) = 0 ↔ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } = ∅ ) ) |
21 |
11 20
|
ax-mp |
⊢ ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ) = 0 ↔ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } = ∅ ) |
22 |
|
hasheq0 |
⊢ ( { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ∈ V → ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ) = 0 ↔ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } = ∅ ) ) |
23 |
14 22
|
ax-mp |
⊢ ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ) = 0 ↔ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } = ∅ ) |
24 |
21 23
|
anbi12i |
⊢ ( ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ) = 0 ∧ ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ) = 0 ) ↔ ( { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } = ∅ ∧ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } = ∅ ) ) |
25 |
|
rabeq0 |
⊢ ( { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } = ∅ ↔ ∀ 𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ) |
26 |
|
rabeq0 |
⊢ ( { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } = ∅ ↔ ∀ 𝑖 ∈ dom 𝐼 ¬ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) |
27 |
25 26
|
anbi12i |
⊢ ( ( { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } = ∅ ∧ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } = ∅ ) ↔ ( ∀ 𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∧ ∀ 𝑖 ∈ dom 𝐼 ¬ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ) |
28 |
|
ralnex |
⊢ ( ∀ 𝑖 ∈ dom 𝐼 ¬ ( 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∨ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ↔ ¬ ∃ 𝑖 ∈ dom 𝐼 ( 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∨ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ) |
29 |
28
|
bicomi |
⊢ ( ¬ ∃ 𝑖 ∈ dom 𝐼 ( 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∨ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ↔ ∀ 𝑖 ∈ dom 𝐼 ¬ ( 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∨ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ) |
30 |
|
ioran |
⊢ ( ¬ ( 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∨ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ↔ ( ¬ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∧ ¬ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ) |
31 |
30
|
ralbii |
⊢ ( ∀ 𝑖 ∈ dom 𝐼 ¬ ( 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∨ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ↔ ∀ 𝑖 ∈ dom 𝐼 ( ¬ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∧ ¬ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ) |
32 |
|
r19.26 |
⊢ ( ∀ 𝑖 ∈ dom 𝐼 ( ¬ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∧ ¬ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ↔ ( ∀ 𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∧ ∀ 𝑖 ∈ dom 𝐼 ¬ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ) |
33 |
29 31 32
|
3bitri |
⊢ ( ¬ ∃ 𝑖 ∈ dom 𝐼 ( 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∨ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ↔ ( ∀ 𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∧ ∀ 𝑖 ∈ dom 𝐼 ¬ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ) |
34 |
33
|
bicomi |
⊢ ( ( ∀ 𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∧ ∀ 𝑖 ∈ dom 𝐼 ¬ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ↔ ¬ ∃ 𝑖 ∈ dom 𝐼 ( 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∨ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ) |
35 |
24 27 34
|
3bitri |
⊢ ( ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ) = 0 ∧ ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ) = 0 ) ↔ ¬ ∃ 𝑖 ∈ dom 𝐼 ( 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∨ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ) |
36 |
|
orcom |
⊢ ( ( 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∨ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ↔ ( ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ∨ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ) ) |
37 |
|
snidg |
⊢ ( 𝑈 ∈ 𝑉 → 𝑈 ∈ { 𝑈 } ) |
38 |
|
eleq2 |
⊢ ( ( 𝐼 ‘ 𝑖 ) = { 𝑈 } → ( 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ↔ 𝑈 ∈ { 𝑈 } ) ) |
39 |
37 38
|
syl5ibrcom |
⊢ ( 𝑈 ∈ 𝑉 → ( ( 𝐼 ‘ 𝑖 ) = { 𝑈 } → 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ) ) |
40 |
|
pm4.72 |
⊢ ( ( ( 𝐼 ‘ 𝑖 ) = { 𝑈 } → 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ) ↔ ( 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ↔ ( ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ∨ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ) ) ) |
41 |
39 40
|
sylib |
⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ↔ ( ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ∨ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ) ) ) |
42 |
36 41
|
bitr4id |
⊢ ( 𝑈 ∈ 𝑉 → ( ( 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∨ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ↔ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ) ) |
43 |
42
|
rexbidv |
⊢ ( 𝑈 ∈ 𝑉 → ( ∃ 𝑖 ∈ dom 𝐼 ( 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∨ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ↔ ∃ 𝑖 ∈ dom 𝐼 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ) ) |
44 |
43
|
notbid |
⊢ ( 𝑈 ∈ 𝑉 → ( ¬ ∃ 𝑖 ∈ dom 𝐼 ( 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ∨ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } ) ↔ ¬ ∃ 𝑖 ∈ dom 𝐼 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ) ) |
45 |
35 44
|
syl5bb |
⊢ ( 𝑈 ∈ 𝑉 → ( ( ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) } ) = 0 ∧ ( ♯ ‘ { 𝑖 ∈ dom 𝐼 ∣ ( 𝐼 ‘ 𝑖 ) = { 𝑈 } } ) = 0 ) ↔ ¬ ∃ 𝑖 ∈ dom 𝐼 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ) ) |
46 |
8 19 45
|
3bitrd |
⊢ ( 𝑈 ∈ 𝑉 → ( ( 𝐷 ‘ 𝑈 ) = 0 ↔ ¬ ∃ 𝑖 ∈ dom 𝐼 𝑈 ∈ ( 𝐼 ‘ 𝑖 ) ) ) |