Step | Hyp | Ref
| Expression |
1 | | vdn0conngrv2.v |
. . . 4
⊢ 𝑉 = (Vtx‘𝐺) |
2 | | eqid 2740 |
. . . 4
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
3 | | eqid 2740 |
. . . 4
⊢ dom
(iEdg‘𝐺) = dom
(iEdg‘𝐺) |
4 | | eqid 2740 |
. . . 4
⊢
(VtxDeg‘𝐺) =
(VtxDeg‘𝐺) |
5 | 1, 2, 3, 4 | vtxdumgrval 27851 |
. . 3
⊢ ((𝐺 ∈ UMGraph ∧ 𝑁 ∈ 𝑉) → ((VtxDeg‘𝐺)‘𝑁) = (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)})) |
6 | 5 | ad2ant2lr 745 |
. 2
⊢ (((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) ∧ (𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉))) → ((VtxDeg‘𝐺)‘𝑁) = (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)})) |
7 | | umgruhgr 27472 |
. . . . . . . 8
⊢ (𝐺 ∈ UMGraph → 𝐺 ∈
UHGraph) |
8 | 2 | uhgrfun 27434 |
. . . . . . . 8
⊢ (𝐺 ∈ UHGraph → Fun
(iEdg‘𝐺)) |
9 | | funfn 6462 |
. . . . . . . . 9
⊢ (Fun
(iEdg‘𝐺) ↔
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
10 | 9 | biimpi 215 |
. . . . . . . 8
⊢ (Fun
(iEdg‘𝐺) →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
11 | 7, 8, 10 | 3syl 18 |
. . . . . . 7
⊢ (𝐺 ∈ UMGraph →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
12 | 11 | adantl 482 |
. . . . . 6
⊢ ((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) →
(iEdg‘𝐺) Fn dom
(iEdg‘𝐺)) |
13 | 12 | adantr 481 |
. . . . 5
⊢ (((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) ∧ (𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉))) → (iEdg‘𝐺) Fn dom (iEdg‘𝐺)) |
14 | | simpl 483 |
. . . . . . 7
⊢ ((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) → 𝐺 ∈
ConnGraph) |
15 | 14 | adantr 481 |
. . . . . 6
⊢ (((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) ∧ (𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉))) → 𝐺 ∈ ConnGraph) |
16 | | simpl 483 |
. . . . . . 7
⊢ ((𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉)) → 𝑁 ∈ 𝑉) |
17 | 16 | adantl 482 |
. . . . . 6
⊢ (((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) ∧ (𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉))) → 𝑁 ∈ 𝑉) |
18 | | simprr 770 |
. . . . . 6
⊢ (((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) ∧ (𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉))) → 1 <
(♯‘𝑉)) |
19 | 1, 2 | conngrv2edg 28555 |
. . . . . 6
⊢ ((𝐺 ∈ ConnGraph ∧ 𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉)) → ∃𝑒 ∈ ran (iEdg‘𝐺)𝑁 ∈ 𝑒) |
20 | 15, 17, 18, 19 | syl3anc 1370 |
. . . . 5
⊢ (((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) ∧ (𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉))) → ∃𝑒 ∈ ran (iEdg‘𝐺)𝑁 ∈ 𝑒) |
21 | | eleq2 2829 |
. . . . . . 7
⊢ (𝑒 = ((iEdg‘𝐺)‘𝑥) → (𝑁 ∈ 𝑒 ↔ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥))) |
22 | 21 | rexrn 6960 |
. . . . . 6
⊢
((iEdg‘𝐺) Fn
dom (iEdg‘𝐺) →
(∃𝑒 ∈ ran
(iEdg‘𝐺)𝑁 ∈ 𝑒 ↔ ∃𝑥 ∈ dom (iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥))) |
23 | 22 | biimpd 228 |
. . . . 5
⊢
((iEdg‘𝐺) Fn
dom (iEdg‘𝐺) →
(∃𝑒 ∈ ran
(iEdg‘𝐺)𝑁 ∈ 𝑒 → ∃𝑥 ∈ dom (iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥))) |
24 | 13, 20, 23 | sylc 65 |
. . . 4
⊢ (((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) ∧ (𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉))) → ∃𝑥 ∈ dom (iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥)) |
25 | | dfrex2 3169 |
. . . 4
⊢
(∃𝑥 ∈ dom
(iEdg‘𝐺)𝑁 ∈ ((iEdg‘𝐺)‘𝑥) ↔ ¬ ∀𝑥 ∈ dom (iEdg‘𝐺) ¬ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)) |
26 | 24, 25 | sylib 217 |
. . 3
⊢ (((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) ∧ (𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉))) → ¬ ∀𝑥 ∈ dom (iEdg‘𝐺) ¬ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)) |
27 | | fvex 6784 |
. . . . . . . 8
⊢
(iEdg‘𝐺)
∈ V |
28 | 27 | dmex 7752 |
. . . . . . 7
⊢ dom
(iEdg‘𝐺) ∈
V |
29 | 28 | a1i 11 |
. . . . . 6
⊢ (((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) ∧ (𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉))) → dom (iEdg‘𝐺) ∈ V) |
30 | | rabexg 5259 |
. . . . . 6
⊢ (dom
(iEdg‘𝐺) ∈ V
→ {𝑥 ∈ dom
(iEdg‘𝐺) ∣
𝑁 ∈ ((iEdg‘𝐺)‘𝑥)} ∈ V) |
31 | | hasheq0 14076 |
. . . . . 6
⊢ ({𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)} ∈ V → ((♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)}) = 0 ↔ {𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)} = ∅)) |
32 | 29, 30, 31 | 3syl 18 |
. . . . 5
⊢ (((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) ∧ (𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉))) →
((♯‘{𝑥 ∈
dom (iEdg‘𝐺) ∣
𝑁 ∈ ((iEdg‘𝐺)‘𝑥)}) = 0 ↔ {𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)} = ∅)) |
33 | | rabeq0 4324 |
. . . . 5
⊢ ({𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)} = ∅ ↔ ∀𝑥 ∈ dom (iEdg‘𝐺) ¬ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)) |
34 | 32, 33 | bitrdi 287 |
. . . 4
⊢ (((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) ∧ (𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉))) →
((♯‘{𝑥 ∈
dom (iEdg‘𝐺) ∣
𝑁 ∈ ((iEdg‘𝐺)‘𝑥)}) = 0 ↔ ∀𝑥 ∈ dom (iEdg‘𝐺) ¬ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥))) |
35 | 34 | necon3abid 2982 |
. . 3
⊢ (((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) ∧ (𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉))) →
((♯‘{𝑥 ∈
dom (iEdg‘𝐺) ∣
𝑁 ∈ ((iEdg‘𝐺)‘𝑥)}) ≠ 0 ↔ ¬ ∀𝑥 ∈ dom (iEdg‘𝐺) ¬ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥))) |
36 | 26, 35 | mpbird 256 |
. 2
⊢ (((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) ∧ (𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉))) → (♯‘{𝑥 ∈ dom (iEdg‘𝐺) ∣ 𝑁 ∈ ((iEdg‘𝐺)‘𝑥)}) ≠ 0) |
37 | 6, 36 | eqnetrd 3013 |
1
⊢ (((𝐺 ∈ ConnGraph ∧ 𝐺 ∈ UMGraph) ∧ (𝑁 ∈ 𝑉 ∧ 1 < (♯‘𝑉))) → ((VtxDeg‘𝐺)‘𝑁) ≠ 0) |