Step | Hyp | Ref
| Expression |
1 | | vdusgraval 26434 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ((𝑉 VDeg 𝐸)‘𝑈) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})) |
2 | 1 | 3adant3 1074 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → ((𝑉 VDeg 𝐸)‘𝑈) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})) |
3 | 2 | eqeq1d 2612 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → (((𝑉 VDeg 𝐸)‘𝑈) = 0 ↔ (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) = 0)) |
4 | | dmfi 8129 |
. . . . . 6
⊢ (𝐸 ∈ Fin → dom 𝐸 ∈ Fin) |
5 | | rabfi 8070 |
. . . . . 6
⊢ (dom
𝐸 ∈ Fin → {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin) |
6 | 4, 5 | syl 17 |
. . . . 5
⊢ (𝐸 ∈ Fin → {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin) |
7 | 6 | 3ad2ant3 1077 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin) |
8 | | hasheq0 13015 |
. . . 4
⊢ ({𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ Fin → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) = 0 ↔ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} = ∅)) |
9 | 7, 8 | syl 17 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) = 0 ↔ {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} = ∅)) |
10 | | rabeq0 3911 |
. . . 4
⊢ ({𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} = ∅ ↔ ∀𝑥 ∈ dom 𝐸 ¬ 𝑈 ∈ (𝐸‘𝑥)) |
11 | | ralnex 2975 |
. . . . 5
⊢
(∀𝑥 ∈
dom 𝐸 ¬ 𝑈 ∈ (𝐸‘𝑥) ↔ ¬ ∃𝑥 ∈ dom 𝐸 𝑈 ∈ (𝐸‘𝑥)) |
12 | | usgrafun 25878 |
. . . . . . . . . . 11
⊢ (𝑉 USGrph 𝐸 → Fun 𝐸) |
13 | 12 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → Fun 𝐸) |
14 | 13 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) ∧ 𝑣 ∈ 𝑉) → Fun 𝐸) |
15 | | elrnrexdm 6271 |
. . . . . . . . 9
⊢ (Fun
𝐸 → ({𝑈, 𝑣} ∈ ran 𝐸 → ∃𝑥 ∈ dom 𝐸{𝑈, 𝑣} = (𝐸‘𝑥))) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) ∧ 𝑣 ∈ 𝑉) → ({𝑈, 𝑣} ∈ ran 𝐸 → ∃𝑥 ∈ dom 𝐸{𝑈, 𝑣} = (𝐸‘𝑥))) |
17 | | prid1g 4239 |
. . . . . . . . . . . 12
⊢ (𝑈 ∈ 𝑉 → 𝑈 ∈ {𝑈, 𝑣}) |
18 | | eleq2 2677 |
. . . . . . . . . . . . 13
⊢ ((𝐸‘𝑥) = {𝑈, 𝑣} → (𝑈 ∈ (𝐸‘𝑥) ↔ 𝑈 ∈ {𝑈, 𝑣})) |
19 | 18 | eqcoms 2618 |
. . . . . . . . . . . 12
⊢ ({𝑈, 𝑣} = (𝐸‘𝑥) → (𝑈 ∈ (𝐸‘𝑥) ↔ 𝑈 ∈ {𝑈, 𝑣})) |
20 | 17, 19 | syl5ibrcom 236 |
. . . . . . . . . . 11
⊢ (𝑈 ∈ 𝑉 → ({𝑈, 𝑣} = (𝐸‘𝑥) → 𝑈 ∈ (𝐸‘𝑥))) |
21 | 20 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → ({𝑈, 𝑣} = (𝐸‘𝑥) → 𝑈 ∈ (𝐸‘𝑥))) |
22 | 21 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) ∧ 𝑣 ∈ 𝑉) → ({𝑈, 𝑣} = (𝐸‘𝑥) → 𝑈 ∈ (𝐸‘𝑥))) |
23 | 22 | reximdv 2999 |
. . . . . . . 8
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) ∧ 𝑣 ∈ 𝑉) → (∃𝑥 ∈ dom 𝐸{𝑈, 𝑣} = (𝐸‘𝑥) → ∃𝑥 ∈ dom 𝐸 𝑈 ∈ (𝐸‘𝑥))) |
24 | 16, 23 | syld 46 |
. . . . . . 7
⊢ (((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) ∧ 𝑣 ∈ 𝑉) → ({𝑈, 𝑣} ∈ ran 𝐸 → ∃𝑥 ∈ dom 𝐸 𝑈 ∈ (𝐸‘𝑥))) |
25 | 24 | rexlimdva 3013 |
. . . . . 6
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → (∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ ran 𝐸 → ∃𝑥 ∈ dom 𝐸 𝑈 ∈ (𝐸‘𝑥))) |
26 | 25 | con3d 147 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → (¬ ∃𝑥 ∈ dom 𝐸 𝑈 ∈ (𝐸‘𝑥) → ¬ ∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ ran 𝐸)) |
27 | 11, 26 | syl5bi 231 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → (∀𝑥 ∈ dom 𝐸 ¬ 𝑈 ∈ (𝐸‘𝑥) → ¬ ∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ ran 𝐸)) |
28 | 10, 27 | syl5bi 231 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → ({𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} = ∅ → ¬ ∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ ran 𝐸)) |
29 | 9, 28 | sylbid 229 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) = 0 → ¬ ∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ ran 𝐸)) |
30 | 3, 29 | sylbid 229 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉 ∧ 𝐸 ∈ Fin) → (((𝑉 VDeg 𝐸)‘𝑈) = 0 → ¬ ∃𝑣 ∈ 𝑉 {𝑈, 𝑣} ∈ ran 𝐸)) |