Proof of Theorem vtxd0nedgb
Step | Hyp | Ref
| Expression |
1 | | vtxd0nedgb.d |
. . . . 5
⊢ 𝐷 = (VtxDeg‘𝐺) |
2 | 1 | fveq1i 6665 |
. . . 4
⊢ (𝐷‘𝑈) = ((VtxDeg‘𝐺)‘𝑈) |
3 | | vtxd0nedgb.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
4 | | vtxd0nedgb.i |
. . . . 5
⊢ 𝐼 = (iEdg‘𝐺) |
5 | | eqid 2821 |
. . . . 5
⊢ dom 𝐼 = dom 𝐼 |
6 | 3, 4, 5 | vtxdgval 27244 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → ((VtxDeg‘𝐺)‘𝑈) = ((♯‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) +𝑒
(♯‘{𝑖 ∈
dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}))) |
7 | 2, 6 | syl5eq 2868 |
. . 3
⊢ (𝑈 ∈ 𝑉 → (𝐷‘𝑈) = ((♯‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) +𝑒
(♯‘{𝑖 ∈
dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}))) |
8 | 7 | eqeq1d 2823 |
. 2
⊢ (𝑈 ∈ 𝑉 → ((𝐷‘𝑈) = 0 ↔ ((♯‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) +𝑒
(♯‘{𝑖 ∈
dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}})) = 0)) |
9 | 4 | fvexi 6678 |
. . . . . . 7
⊢ 𝐼 ∈ V |
10 | 9 | dmex 7610 |
. . . . . 6
⊢ dom 𝐼 ∈ V |
11 | 10 | rabex 5227 |
. . . . 5
⊢ {𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)} ∈ V |
12 | | hashxnn0 13693 |
. . . . 5
⊢ ({𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)} ∈ V → (♯‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) ∈
ℕ0*) |
13 | 11, 12 | ax-mp 5 |
. . . 4
⊢
(♯‘{𝑖
∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) ∈
ℕ0* |
14 | 10 | rabex 5227 |
. . . . 5
⊢ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}} ∈ V |
15 | | hashxnn0 13693 |
. . . . 5
⊢ ({𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}} ∈ V → (♯‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) ∈
ℕ0*) |
16 | 14, 15 | ax-mp 5 |
. . . 4
⊢
(♯‘{𝑖
∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) ∈
ℕ0* |
17 | 13, 16 | pm3.2i 473 |
. . 3
⊢
((♯‘{𝑖
∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) ∈ ℕ0*
∧ (♯‘{𝑖
∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) ∈
ℕ0*) |
18 | | xnn0xadd0 12634 |
. . 3
⊢
(((♯‘{𝑖
∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) ∈ ℕ0*
∧ (♯‘{𝑖
∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) ∈ ℕ0*)
→ (((♯‘{𝑖
∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) +𝑒
(♯‘{𝑖 ∈
dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}})) = 0 ↔ ((♯‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) = 0 ∧ (♯‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) = 0))) |
19 | 17, 18 | mp1i 13 |
. 2
⊢ (𝑈 ∈ 𝑉 → (((♯‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) +𝑒
(♯‘{𝑖 ∈
dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}})) = 0 ↔ ((♯‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) = 0 ∧ (♯‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) = 0))) |
20 | | hasheq0 13718 |
. . . . . 6
⊢ ({𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)} ∈ V → ((♯‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) = 0 ↔ {𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)} = ∅)) |
21 | 11, 20 | ax-mp 5 |
. . . . 5
⊢
((♯‘{𝑖
∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) = 0 ↔ {𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)} = ∅) |
22 | | hasheq0 13718 |
. . . . . 6
⊢ ({𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}} ∈ V → ((♯‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) = 0 ↔ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}} = ∅)) |
23 | 14, 22 | ax-mp 5 |
. . . . 5
⊢
((♯‘{𝑖
∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) = 0 ↔ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}} = ∅) |
24 | 21, 23 | anbi12i 628 |
. . . 4
⊢
(((♯‘{𝑖
∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) = 0 ∧ (♯‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) = 0) ↔ ({𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)} = ∅ ∧ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}} = ∅)) |
25 | | rabeq0 4337 |
. . . . 5
⊢ ({𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)} = ∅ ↔ ∀𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ (𝐼‘𝑖)) |
26 | | rabeq0 4337 |
. . . . 5
⊢ ({𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}} = ∅ ↔ ∀𝑖 ∈ dom 𝐼 ¬ (𝐼‘𝑖) = {𝑈}) |
27 | 25, 26 | anbi12i 628 |
. . . 4
⊢ (({𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)} = ∅ ∧ {𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}} = ∅) ↔ (∀𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ (𝐼‘𝑖) ∧ ∀𝑖 ∈ dom 𝐼 ¬ (𝐼‘𝑖) = {𝑈})) |
28 | | ralnex 3236 |
. . . . . . 7
⊢
(∀𝑖 ∈
dom 𝐼 ¬ (𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ ¬ ∃𝑖 ∈ dom 𝐼(𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈})) |
29 | 28 | bicomi 226 |
. . . . . 6
⊢ (¬
∃𝑖 ∈ dom 𝐼(𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ ∀𝑖 ∈ dom 𝐼 ¬ (𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈})) |
30 | | ioran 980 |
. . . . . . 7
⊢ (¬
(𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ (¬ 𝑈 ∈ (𝐼‘𝑖) ∧ ¬ (𝐼‘𝑖) = {𝑈})) |
31 | 30 | ralbii 3165 |
. . . . . 6
⊢
(∀𝑖 ∈
dom 𝐼 ¬ (𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ ∀𝑖 ∈ dom 𝐼(¬ 𝑈 ∈ (𝐼‘𝑖) ∧ ¬ (𝐼‘𝑖) = {𝑈})) |
32 | | r19.26 3170 |
. . . . . 6
⊢
(∀𝑖 ∈
dom 𝐼(¬ 𝑈 ∈ (𝐼‘𝑖) ∧ ¬ (𝐼‘𝑖) = {𝑈}) ↔ (∀𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ (𝐼‘𝑖) ∧ ∀𝑖 ∈ dom 𝐼 ¬ (𝐼‘𝑖) = {𝑈})) |
33 | 29, 31, 32 | 3bitri 299 |
. . . . 5
⊢ (¬
∃𝑖 ∈ dom 𝐼(𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ (∀𝑖 ∈ dom 𝐼 ¬ 𝑈 ∈ (𝐼‘𝑖) ∧ ∀𝑖 ∈ dom 𝐼 ¬ (𝐼‘𝑖) = {𝑈})) |
34 | 33 | bicomi 226 |
. . . 4
⊢
((∀𝑖 ∈
dom 𝐼 ¬ 𝑈 ∈ (𝐼‘𝑖) ∧ ∀𝑖 ∈ dom 𝐼 ¬ (𝐼‘𝑖) = {𝑈}) ↔ ¬ ∃𝑖 ∈ dom 𝐼(𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈})) |
35 | 24, 27, 34 | 3bitri 299 |
. . 3
⊢
(((♯‘{𝑖
∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) = 0 ∧ (♯‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) = 0) ↔ ¬ ∃𝑖 ∈ dom 𝐼(𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈})) |
36 | | snidg 4592 |
. . . . . . . 8
⊢ (𝑈 ∈ 𝑉 → 𝑈 ∈ {𝑈}) |
37 | | eleq2 2901 |
. . . . . . . 8
⊢ ((𝐼‘𝑖) = {𝑈} → (𝑈 ∈ (𝐼‘𝑖) ↔ 𝑈 ∈ {𝑈})) |
38 | 36, 37 | syl5ibrcom 249 |
. . . . . . 7
⊢ (𝑈 ∈ 𝑉 → ((𝐼‘𝑖) = {𝑈} → 𝑈 ∈ (𝐼‘𝑖))) |
39 | | pm4.72 946 |
. . . . . . 7
⊢ (((𝐼‘𝑖) = {𝑈} → 𝑈 ∈ (𝐼‘𝑖)) ↔ (𝑈 ∈ (𝐼‘𝑖) ↔ ((𝐼‘𝑖) = {𝑈} ∨ 𝑈 ∈ (𝐼‘𝑖)))) |
40 | 38, 39 | sylib 220 |
. . . . . 6
⊢ (𝑈 ∈ 𝑉 → (𝑈 ∈ (𝐼‘𝑖) ↔ ((𝐼‘𝑖) = {𝑈} ∨ 𝑈 ∈ (𝐼‘𝑖)))) |
41 | | orcom 866 |
. . . . . 6
⊢ ((𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ ((𝐼‘𝑖) = {𝑈} ∨ 𝑈 ∈ (𝐼‘𝑖))) |
42 | 40, 41 | syl6rbbr 292 |
. . . . 5
⊢ (𝑈 ∈ 𝑉 → ((𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ 𝑈 ∈ (𝐼‘𝑖))) |
43 | 42 | rexbidv 3297 |
. . . 4
⊢ (𝑈 ∈ 𝑉 → (∃𝑖 ∈ dom 𝐼(𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ ∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖))) |
44 | 43 | notbid 320 |
. . 3
⊢ (𝑈 ∈ 𝑉 → (¬ ∃𝑖 ∈ dom 𝐼(𝑈 ∈ (𝐼‘𝑖) ∨ (𝐼‘𝑖) = {𝑈}) ↔ ¬ ∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖))) |
45 | 35, 44 | syl5bb 285 |
. 2
⊢ (𝑈 ∈ 𝑉 → (((♯‘{𝑖 ∈ dom 𝐼 ∣ 𝑈 ∈ (𝐼‘𝑖)}) = 0 ∧ (♯‘{𝑖 ∈ dom 𝐼 ∣ (𝐼‘𝑖) = {𝑈}}) = 0) ↔ ¬ ∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖))) |
46 | 8, 19, 45 | 3bitrd 307 |
1
⊢ (𝑈 ∈ 𝑉 → ((𝐷‘𝑈) = 0 ↔ ¬ ∃𝑖 ∈ dom 𝐼 𝑈 ∈ (𝐼‘𝑖))) |