Proof of Theorem vtxd0nedgb
Step | Hyp | Ref
| Expression |
1 | | vtxd0nedgb.d |
. . . . 5
⊢ 𝐷 = (VtxDeg‘𝐺) |
2 | 1 | fveq1i 6192 |
. . . 4
⊢ (𝐷‘𝑈) = ((VtxDeg‘𝐺)‘𝑈) |
3 | | vtxd0nedgb.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
4 | | vtxd0nedgb.i |
. . . . 5
⊢ 𝐼 = (iEdg‘𝐺) |
5 | | eqid 2622 |
. . . . 5
⊢ dom 𝐼 = dom 𝐼 |
6 | 3, 4, 5 | vtxdgval 26364 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑈) = ((#‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) +𝑒 (#‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}))) |
7 | 2, 6 | syl5eq 2668 |
. . 3
⊢ (𝑈 ∈ 𝑉 → (𝐷‘𝑈) = ((#‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) +𝑒 (#‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}))) |
8 | 7 | eqeq1d 2624 |
. 2
⊢ (𝑈 ∈ 𝑉 → ((𝐷‘𝑈) = 0 ↔ ((#‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) +𝑒 (#‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}})) = 0)) |
9 | | fvex 6201 |
. . . . . . . 8
⊢
(iEdg‘𝐺)
∈ V |
10 | 4, 9 | eqeltri 2697 |
. . . . . . 7
⊢ 𝐼 ∈ V |
11 | 10 | dmex 7099 |
. . . . . 6
⊢ dom 𝐼 ∈ V |
12 | 11 | rabex 4813 |
. . . . 5
⊢ {𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)} ∈ V |
13 | | hashxnn0 13127 |
. . . . 5
⊢ ({𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)} ∈ V → (#‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) ∈
ℕ0*) |
14 | 12, 13 | ax-mp 5 |
. . . 4
⊢
(#‘{𝑖 ∈
dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) ∈
ℕ0* |
15 | 11 | rabex 4813 |
. . . . 5
⊢ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}} ∈ V |
16 | | hashxnn0 13127 |
. . . . 5
⊢ ({𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}} ∈ V → (#‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) ∈
ℕ0*) |
17 | 15, 16 | ax-mp 5 |
. . . 4
⊢
(#‘{𝑖 ∈
dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) ∈
ℕ0* |
18 | 14, 17 | pm3.2i 471 |
. . 3
⊢
((#‘{𝑖 ∈
dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) ∈ ℕ0*
∧ (#‘{𝑖 ∈
dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) ∈
ℕ0*) |
19 | | xnn0xadd0 12077 |
. . 3
⊢
(((#‘{𝑖 ∈
dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) ∈ ℕ0*
∧ (#‘{𝑖 ∈
dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) ∈ ℕ0*)
→ (((#‘{𝑖 ∈
dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) +𝑒 (#‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}})) = 0 ↔ ((#‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) = 0 ∧ (#‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) = 0))) |
20 | 18, 19 | mp1i 13 |
. 2
⊢ (𝑈 ∈ 𝑉 → (((#‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) +𝑒 (#‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}})) = 0 ↔ ((#‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) = 0 ∧ (#‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) = 0))) |
21 | | hasheq0 13154 |
. . . . . 6
⊢ ({𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)} ∈ V → ((#‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) = 0 ↔ {𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)} = ∅)) |
22 | 12, 21 | ax-mp 5 |
. . . . 5
⊢
((#‘{𝑖 ∈
dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) = 0 ↔ {𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)} = ∅) |
23 | | hasheq0 13154 |
. . . . . 6
⊢ ({𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}} ∈ V → ((#‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) = 0 ↔ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}} = ∅)) |
24 | 15, 23 | ax-mp 5 |
. . . . 5
⊢
((#‘{𝑖 ∈
dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) = 0 ↔ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}} = ∅) |
25 | 22, 24 | anbi12i 733 |
. . . 4
⊢
(((#‘{𝑖 ∈
dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) = 0 ∧ (#‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) = 0) ↔ ({𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)} = ∅ ∧ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}} = ∅)) |
26 | | rabeq0 3957 |
. . . . 5
⊢ ({𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)} = ∅ ↔ ∀𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ (𝐼‘𝑖)) |
27 | | rabeq0 3957 |
. . . . 5
⊢ ({𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}} = ∅ ↔ ∀𝑖 ∈ dom 𝐼 ¬ (𝐼‘𝑖) = {𝑈}) |
28 | 26, 27 | anbi12i 733 |
. . . 4
⊢ (({𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)} = ∅ ∧ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}} = ∅) ↔ (∀𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ (𝐼‘𝑖) ∧ ∀𝑖 ∈ dom 𝐼 ¬ (𝐼‘𝑖) = {𝑈})) |
29 | | ralnex 2992 |
. . . . . . 7
⊢
(∀𝑖 ∈
dom 𝐼 ¬ (𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ ¬ ∃𝑖 ∈ dom 𝐼(𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈})) |
30 | 29 | bicomi 214 |
. . . . . 6
⊢ (¬
∃𝑖 ∈ dom 𝐼(𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ ∀𝑖 ∈ dom 𝐼 ¬ (𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈})) |
31 | | ioran 511 |
. . . . . . 7
⊢ (¬
(𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ (¬ 𝑈 ∈ (𝐼‘𝑖) ∧ ¬ (𝐼‘𝑖) = {𝑈})) |
32 | 31 | ralbii 2980 |
. . . . . 6
⊢
(∀𝑖 ∈
dom 𝐼 ¬ (𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ ∀𝑖 ∈ dom 𝐼(¬ 𝑈 ∈ (𝐼‘𝑖) ∧ ¬ (𝐼‘𝑖) = {𝑈})) |
33 | | r19.26 3064 |
. . . . . 6
⊢
(∀𝑖 ∈
dom 𝐼(¬ 𝑈 ∈ (𝐼‘𝑖) ∧ ¬ (𝐼‘𝑖) = {𝑈}) ↔ (∀𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ (𝐼‘𝑖) ∧ ∀𝑖 ∈ dom 𝐼 ¬ (𝐼‘𝑖) = {𝑈})) |
34 | 30, 32, 33 | 3bitri 286 |
. . . . 5
⊢ (¬
∃𝑖 ∈ dom 𝐼(𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ (∀𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ (𝐼‘𝑖) ∧ ∀𝑖 ∈ dom 𝐼 ¬ (𝐼‘𝑖) = {𝑈})) |
35 | 34 | bicomi 214 |
. . . 4
⊢
((∀𝑖 ∈
dom 𝐼 ¬ 𝑈 ∈ (𝐼‘𝑖) ∧ ∀𝑖 ∈ dom 𝐼 ¬ (𝐼‘𝑖) = {𝑈}) ↔ ¬ ∃𝑖 ∈ dom 𝐼(𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈})) |
36 | 25, 28, 35 | 3bitri 286 |
. . 3
⊢
(((#‘{𝑖 ∈
dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) = 0 ∧ (#‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) = 0) ↔ ¬ ∃𝑖 ∈ dom 𝐼(𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈})) |
37 | | snidg 4206 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝑉 → 𝑈 ∈ {𝑈}) |
38 | | eleq2 2690 |
. . . . . . . 8
⊢ ((𝐼‘𝑖) = {𝑈} → (𝑈 ∈ (𝐼‘𝑖) ↔ 𝑈 ∈ {𝑈})) |
39 | 37, 38 | syl5ibrcom 237 |
. . . . . . 7
⊢ (𝑈 ∈ 𝑉 → ((𝐼‘𝑖) = {𝑈} → 𝑈 ∈ (𝐼‘𝑖))) |
40 | | pm4.72 920 |
. . . . . . 7
⊢ (((𝐼‘𝑖) = {𝑈} → 𝑈 ∈ (𝐼‘𝑖)) ↔ (𝑈 ∈ (𝐼‘𝑖) ↔ ((𝐼‘𝑖) = {𝑈} ∨ 𝑈 ∈ (𝐼‘𝑖)))) |
41 | 39, 40 | sylib 208 |
. . . . . 6
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ (𝐼‘𝑖) ↔ ((𝐼‘𝑖) = {𝑈} ∨ 𝑈 ∈ (𝐼‘𝑖)))) |
42 | | orcom 402 |
. . . . . 6
⊢ ((𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ ((𝐼‘𝑖) = {𝑈} ∨ 𝑈 ∈ (𝐼‘𝑖))) |
43 | 41, 42 | syl6rbbr 279 |
. . . . 5
⊢ (𝑈 ∈ 𝑉 → ((𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ 𝑈 ∈ (𝐼‘𝑖))) |
44 | 43 | rexbidv 3052 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → (∃𝑖 ∈ dom 𝐼(𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ ∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖))) |
45 | 44 | notbid 308 |
. . 3
⊢ (𝑈 ∈ 𝑉 → (¬ ∃𝑖 ∈ dom 𝐼(𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ ¬ ∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖))) |
46 | 36, 45 | syl5bb 272 |
. 2
⊢ (𝑈 ∈ 𝑉 → (((#‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) = 0 ∧ (#‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) = 0) ↔ ¬ ∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖))) |
47 | 8, 20, 46 | 3bitrd 294 |
1
⊢ (𝑈 ∈ 𝑉 → ((𝐷‘𝑈) = 0 ↔ ¬ ∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖))) |