Proof of Theorem vdusgraval
Step | Hyp | Ref
| Expression |
1 | | usgranloop0 25909 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → {𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅) |
2 | | usgrafun 25878 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → Fun 𝐸) |
3 | | usgrav 25867 |
. . . . . . 7
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
4 | | funfn 5833 |
. . . . . . . 8
⊢ (Fun
𝐸 ↔ 𝐸 Fn dom 𝐸) |
5 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → 𝑉 ∈ V) |
6 | 5 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐸 Fn dom 𝐸 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V)) → 𝑉 ∈ V) |
7 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝐸 Fn dom 𝐸 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V)) → 𝐸 Fn dom 𝐸) |
8 | | dmexg 6989 |
. . . . . . . . . . . 12
⊢ (𝐸 ∈ V → dom 𝐸 ∈ V) |
9 | 8 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → dom 𝐸 ∈ V) |
10 | 9 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐸 Fn dom 𝐸 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V)) → dom 𝐸 ∈ V) |
11 | 6, 7, 10 | 3jca 1235 |
. . . . . . . . 9
⊢ ((𝐸 Fn dom 𝐸 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V)) → (𝑉 ∈ V ∧ 𝐸 Fn dom 𝐸 ∧ dom 𝐸 ∈ V)) |
12 | 11 | ex 449 |
. . . . . . . 8
⊢ (𝐸 Fn dom 𝐸 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ∈ V ∧ 𝐸 Fn dom 𝐸 ∧ dom 𝐸 ∈ V))) |
13 | 4, 12 | sylbi 206 |
. . . . . . 7
⊢ (Fun
𝐸 → ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 ∈ V ∧ 𝐸 Fn dom 𝐸 ∧ dom 𝐸 ∈ V))) |
14 | 2, 3, 13 | sylc 63 |
. . . . . 6
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 Fn dom 𝐸 ∧ dom 𝐸 ∈ V)) |
15 | 14 | anim1i 590 |
. . . . 5
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ((𝑉 ∈ V ∧ 𝐸 Fn dom 𝐸 ∧ dom 𝐸 ∈ V) ∧ 𝑈 ∈ 𝑉)) |
16 | | vdgrval 26423 |
. . . . 5
⊢ (((𝑉 ∈ V ∧ 𝐸 Fn dom 𝐸 ∧ dom 𝐸 ∈ V) ∧ 𝑈 ∈ 𝑉) → ((𝑉 VDeg 𝐸)‘𝑈) = ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}}))) |
17 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ ({𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅ → (#‘{𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}}) = (#‘∅)) |
18 | | hash0 13019 |
. . . . . . . . . . 11
⊢
(#‘∅) = 0 |
19 | 17, 18 | syl6eq 2660 |
. . . . . . . . . 10
⊢ ({𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅ → (#‘{𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}}) = 0) |
20 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢
((#‘{𝑥 ∈
dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}}) = 0 → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}})) = ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒
0)) |
21 | 20 | adantr 480 |
. . . . . . . . . . . 12
⊢
(((#‘{𝑥 ∈
dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}}) = 0 ∧ 𝑉 USGrph 𝐸) → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}})) = ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒
0)) |
22 | 3 | simprd 478 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 USGrph 𝐸 → 𝐸 ∈ V) |
23 | | rabexg 4739 |
. . . . . . . . . . . . . . 15
⊢ (dom
𝐸 ∈ V → {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ V) |
24 | 22, 8, 23 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝑉 USGrph 𝐸 → {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ V) |
25 | 24 | adantl 481 |
. . . . . . . . . . . . 13
⊢
(((#‘{𝑥 ∈
dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}}) = 0 ∧ 𝑉 USGrph 𝐸) → {𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ V) |
26 | | hashxrcl 13010 |
. . . . . . . . . . . . 13
⊢ ({𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)} ∈ V → (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) ∈
ℝ*) |
27 | | xaddid1 11946 |
. . . . . . . . . . . . 13
⊢
((#‘{𝑥 ∈
dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) ∈ ℝ* →
((#‘{𝑥 ∈ dom
𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 0) =
(#‘{𝑥 ∈ dom
𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})) |
28 | 25, 26, 27 | 3syl 18 |
. . . . . . . . . . . 12
⊢
(((#‘{𝑥 ∈
dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}}) = 0 ∧ 𝑉 USGrph 𝐸) → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 0) =
(#‘{𝑥 ∈ dom
𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})) |
29 | 21, 28 | eqtrd 2644 |
. . . . . . . . . . 11
⊢
(((#‘{𝑥 ∈
dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}}) = 0 ∧ 𝑉 USGrph 𝐸) → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}})) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})) |
30 | 29 | ex 449 |
. . . . . . . . . 10
⊢
((#‘{𝑥 ∈
dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}}) = 0 → (𝑉 USGrph 𝐸 → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}})) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}))) |
31 | 19, 30 | syl 17 |
. . . . . . . . 9
⊢ ({𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅ → (𝑉 USGrph 𝐸 → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}})) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}))) |
32 | 31 | com12 32 |
. . . . . . . 8
⊢ (𝑉 USGrph 𝐸 → ({𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅ → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}})) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}))) |
33 | 32 | adantl 481 |
. . . . . . 7
⊢ ((((𝑉 VDeg 𝐸)‘𝑈) = ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}})) ∧ 𝑉 USGrph 𝐸) → ({𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅ → ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}})) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}))) |
34 | | eqeq1 2614 |
. . . . . . . 8
⊢ (((𝑉 VDeg 𝐸)‘𝑈) = ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}})) → (((𝑉 VDeg 𝐸)‘𝑈) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) ↔ ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}})) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}))) |
35 | 34 | adantr 480 |
. . . . . . 7
⊢ ((((𝑉 VDeg 𝐸)‘𝑈) = ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}})) ∧ 𝑉 USGrph 𝐸) → (((𝑉 VDeg 𝐸)‘𝑈) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) ↔ ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}})) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}))) |
36 | 33, 35 | sylibrd 248 |
. . . . . 6
⊢ ((((𝑉 VDeg 𝐸)‘𝑈) = ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}})) ∧ 𝑉 USGrph 𝐸) → ({𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅ → ((𝑉 VDeg 𝐸)‘𝑈) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}))) |
37 | 36 | ex 449 |
. . . . 5
⊢ (((𝑉 VDeg 𝐸)‘𝑈) = ((#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}) +𝑒 (#‘{𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}})) → (𝑉 USGrph 𝐸 → ({𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅ → ((𝑉 VDeg 𝐸)‘𝑈) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})))) |
38 | 15, 16, 37 | 3syl 18 |
. . . 4
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → (𝑉 USGrph 𝐸 → ({𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅ → ((𝑉 VDeg 𝐸)‘𝑈) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})))) |
39 | 38 | com12 32 |
. . 3
⊢ (𝑉 USGrph 𝐸 → ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ({𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅ → ((𝑉 VDeg 𝐸)‘𝑈) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})))) |
40 | 39 | anabsi5 854 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ({𝑥 ∈ dom 𝐸 ∣ (𝐸‘𝑥) = {𝑈}} = ∅ → ((𝑉 VDeg 𝐸)‘𝑈) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)}))) |
41 | 1, 40 | mpd 15 |
1
⊢ ((𝑉 USGrph 𝐸 ∧ 𝑈 ∈ 𝑉) → ((𝑉 VDeg 𝐸)‘𝑈) = (#‘{𝑥 ∈ dom 𝐸 ∣ 𝑈 ∈ (𝐸‘𝑥)})) |