Step | Hyp | Ref
| Expression |
1 | | nbgraf1o 25976 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑈)–1-1-onto→{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) |
2 | | hasheqf1o 12999 |
. . . 4
⊢
(((〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin ∧ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin) → ((#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) ↔ ∃𝑓 𝑓:(〈𝑉, 𝐸〉 Neighbors 𝑈)–1-1-onto→{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})) |
3 | 1, 2 | syl5ibr 235 |
. . 3
⊢
(((〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin ∧ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin) → ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}))) |
4 | | edgusgranbfin 25979 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ((〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin ↔ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin)) |
5 | | pm2.24 120 |
. . . . . 6
⊢ ({𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin → (¬ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}))) |
6 | 4, 5 | syl6bi 242 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ((〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin → (¬ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})))) |
7 | 6 | com3l 87 |
. . . 4
⊢
((〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin → (¬
{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin → ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})))) |
8 | 7 | imp 444 |
. . 3
⊢
(((〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin ∧ ¬ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin) → ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}))) |
9 | | pm2.24 120 |
. . . . . 6
⊢
((〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin → (¬
(〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}))) |
10 | 4, 9 | syl6bir 243 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ({𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin → (¬ (〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})))) |
11 | 10 | com13 86 |
. . . 4
⊢ (¬
(〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin → ({𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin → ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})))) |
12 | 11 | imp 444 |
. . 3
⊢ ((¬
(〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin ∧ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin) → ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}))) |
13 | | ovex 6577 |
. . . . . . 7
⊢
(〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ V |
14 | 13 | a1i 11 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ V) |
15 | | simpl 472 |
. . . . . 6
⊢ ((¬
(〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin ∧ ¬ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin) → ¬ (〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin) |
16 | | hashinf 12984 |
. . . . . 6
⊢
(((〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ V ∧ ¬
(〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = +∞) |
17 | 14, 15, 16 | syl2anr 494 |
. . . . 5
⊢ (((¬
(〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin ∧ ¬ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin) ∧ (𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉)) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = +∞) |
18 | | usgrav 25867 |
. . . . . . . . 9
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
19 | 18 | simprd 478 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → 𝐸 ∈ V) |
20 | | dmexg 6989 |
. . . . . . . 8
⊢ (𝐸 ∈ V → dom 𝐸 ∈ V) |
21 | | rabexg 4739 |
. . . . . . . 8
⊢ (dom
𝐸 ∈ V → {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ V) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ V) |
23 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ V) |
24 | | simpr 476 |
. . . . . 6
⊢ ((¬
(〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin ∧ ¬ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin) → ¬ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin) |
25 | | hashinf 12984 |
. . . . . 6
⊢ (({𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ V ∧ ¬ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin) → (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) = +∞) |
26 | 23, 24, 25 | syl2anr 494 |
. . . . 5
⊢ (((¬
(〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin ∧ ¬ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin) ∧ (𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉)) → (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) = +∞) |
27 | 17, 26 | eqtr4d 2647 |
. . . 4
⊢ (((¬
(〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin ∧ ¬ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin) ∧ (𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉)) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})) |
28 | 27 | ex 449 |
. . 3
⊢ ((¬
(〈𝑉, 𝐸〉 Neighbors 𝑈) ∈ Fin ∧ ¬ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin) → ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}))) |
29 | 3, 8, 12, 28 | 4cases 987 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})) |
30 | | vdusgraval 26434 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ((𝑉 VDeg 𝐸)‘𝑈) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})) |
31 | 29, 30 | eqtr4d 2647 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (#‘(〈𝑉, 𝐸〉 Neighbors 𝑈)) = ((𝑉 VDeg 𝐸)‘𝑈)) |