Step | Hyp | Ref
| Expression |
1 | | rusgraprop3 26470 |
. . 3
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → (𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑘 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸}) = 𝐾)) |
2 | | usgrav 25867 |
. . . . 5
⊢ (𝑉 USGrph 𝐸 → (𝑉 ∈ V ∧ 𝐸 ∈ V)) |
3 | | hash1snb 13068 |
. . . . . . . 8
⊢ (𝑉 ∈ V → ((#‘𝑉) = 1 ↔ ∃𝑣 𝑉 = {𝑣})) |
4 | | raleq 3115 |
. . . . . . . . . . . . 13
⊢ (𝑉 = {𝑣} → (∀𝑘 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸}) = 𝐾 ↔ ∀𝑘 ∈ {𝑣} (#‘{𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸}) = 𝐾)) |
5 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑣 ∈ V |
6 | | preq1 4212 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑣 → {𝑘, 𝑛} = {𝑣, 𝑛}) |
7 | 6 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑣 → ({𝑘, 𝑛} ∈ ran 𝐸 ↔ {𝑣, 𝑛} ∈ ran 𝐸)) |
8 | 7 | rabbidv 3164 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑣 → {𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸} = {𝑛 ∈ 𝑉 ∣ {𝑣, 𝑛} ∈ ran 𝐸}) |
9 | 8 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑣 → (#‘{𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸}) = (#‘{𝑛 ∈ 𝑉 ∣ {𝑣, 𝑛} ∈ ran 𝐸})) |
10 | 9 | eqeq1d 2612 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑣 → ((#‘{𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸}) = 𝐾 ↔ (#‘{𝑛 ∈ 𝑉 ∣ {𝑣, 𝑛} ∈ ran 𝐸}) = 𝐾)) |
11 | 10 | ralsng 4165 |
. . . . . . . . . . . . . 14
⊢ (𝑣 ∈ V → (∀𝑘 ∈ {𝑣} (#‘{𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸}) = 𝐾 ↔ (#‘{𝑛 ∈ 𝑉 ∣ {𝑣, 𝑛} ∈ ran 𝐸}) = 𝐾)) |
12 | 5, 11 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ (𝑉 = {𝑣} → (∀𝑘 ∈ {𝑣} (#‘{𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸}) = 𝐾 ↔ (#‘{𝑛 ∈ 𝑉 ∣ {𝑣, 𝑛} ∈ ran 𝐸}) = 𝐾)) |
13 | | rabeq 3166 |
. . . . . . . . . . . . . . 15
⊢ (𝑉 = {𝑣} → {𝑛 ∈ 𝑉 ∣ {𝑣, 𝑛} ∈ ran 𝐸} = {𝑛 ∈ {𝑣} ∣ {𝑣, 𝑛} ∈ ran 𝐸}) |
14 | 13 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑉 = {𝑣} → (#‘{𝑛 ∈ 𝑉 ∣ {𝑣, 𝑛} ∈ ran 𝐸}) = (#‘{𝑛 ∈ {𝑣} ∣ {𝑣, 𝑛} ∈ ran 𝐸})) |
15 | 14 | eqeq1d 2612 |
. . . . . . . . . . . . 13
⊢ (𝑉 = {𝑣} → ((#‘{𝑛 ∈ 𝑉 ∣ {𝑣, 𝑛} ∈ ran 𝐸}) = 𝐾 ↔ (#‘{𝑛 ∈ {𝑣} ∣ {𝑣, 𝑛} ∈ ran 𝐸}) = 𝐾)) |
16 | 4, 12, 15 | 3bitrd 293 |
. . . . . . . . . . . 12
⊢ (𝑉 = {𝑣} → (∀𝑘 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸}) = 𝐾 ↔ (#‘{𝑛 ∈ {𝑣} ∣ {𝑣, 𝑛} ∈ ran 𝐸}) = 𝐾)) |
17 | | hashrabsn01 13023 |
. . . . . . . . . . . . . 14
⊢
((#‘{𝑛 ∈
{𝑣} ∣ {𝑣, 𝑛} ∈ ran 𝐸}) = 𝐾 → (𝐾 = 0 ∨ 𝐾 = 1)) |
18 | | ax-1 6 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 = 0 → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0)) |
19 | 18 | 2a1d 26 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 = 0 → (𝐾 ∈ ℕ0 → (𝑉 ∈ V → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0)))) |
20 | 19 | 2a1d 26 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 = 0 → ((#‘{𝑛 ∈ {𝑣} ∣ {𝑣, 𝑛} ∈ ran 𝐸}) = 𝐾 → (𝑉 = {𝑣} → (𝐾 ∈ ℕ0 → (𝑉 ∈ V → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0)))))) |
21 | | eqeq2 2621 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 = 1 → ((#‘{𝑛 ∈ {𝑣} ∣ {𝑣, 𝑛} ∈ ran 𝐸}) = 𝐾 ↔ (#‘{𝑛 ∈ {𝑣} ∣ {𝑣, 𝑛} ∈ ran 𝐸}) = 1)) |
22 | | hashrabsn1 13024 |
. . . . . . . . . . . . . . . . 17
⊢
((#‘{𝑛 ∈
{𝑣} ∣ {𝑣, 𝑛} ∈ ran 𝐸}) = 1 → [𝑣 / 𝑛]{𝑣, 𝑛} ∈ ran 𝐸) |
23 | | sbcel1g 3939 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 ∈ V → ([𝑣 / 𝑛]{𝑣, 𝑛} ∈ ran 𝐸 ↔ ⦋𝑣 / 𝑛⦌{𝑣, 𝑛} ∈ ran 𝐸)) |
24 | 5, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢
([𝑣 / 𝑛]{𝑣, 𝑛} ∈ ran 𝐸 ↔ ⦋𝑣 / 𝑛⦌{𝑣, 𝑛} ∈ ran 𝐸) |
25 | | csbprg 4191 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∈ V →
⦋𝑣 / 𝑛⦌{𝑣, 𝑛} = {⦋𝑣 / 𝑛⦌𝑣, ⦋𝑣 / 𝑛⦌𝑛}) |
26 | | csbconstg 3512 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 ∈ V →
⦋𝑣 / 𝑛⦌𝑣 = 𝑣) |
27 | | csbvarg 3955 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 ∈ V →
⦋𝑣 / 𝑛⦌𝑛 = 𝑣) |
28 | 26, 27 | preq12d 4220 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑣 ∈ V →
{⦋𝑣 / 𝑛⦌𝑣, ⦋𝑣 / 𝑛⦌𝑛} = {𝑣, 𝑣}) |
29 | 25, 28 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑣 ∈ V →
⦋𝑣 / 𝑛⦌{𝑣, 𝑛} = {𝑣, 𝑣}) |
30 | 5, 29 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
⊢
⦋𝑣 /
𝑛⦌{𝑣, 𝑛} = {𝑣, 𝑣} |
31 | 30 | eleq1i 2679 |
. . . . . . . . . . . . . . . . . . 19
⊢
(⦋𝑣 /
𝑛⦌{𝑣, 𝑛} ∈ ran 𝐸 ↔ {𝑣, 𝑣} ∈ ran 𝐸) |
32 | | equid 1926 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑣 = 𝑣 |
33 | | usgraedgrn 25910 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑉 USGrph 𝐸 ∧ {𝑣, 𝑣} ∈ ran 𝐸) → 𝑣 ≠ 𝑣) |
34 | | eqneqall 2793 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑣 = 𝑣 → (𝑣 ≠ 𝑣 → 𝐾 = 0)) |
35 | 32, 33, 34 | mpsyl 66 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑉 USGrph 𝐸 ∧ {𝑣, 𝑣} ∈ ran 𝐸) → 𝐾 = 0) |
36 | 35 | ex 449 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑉 USGrph 𝐸 → ({𝑣, 𝑣} ∈ ran 𝐸 → 𝐾 = 0)) |
37 | 36 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → ({𝑣, 𝑣} ∈ ran 𝐸 → 𝐾 = 0)) |
38 | 37 | com12 32 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ({𝑣, 𝑣} ∈ ran 𝐸 → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0)) |
39 | 38 | a1d 25 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ({𝑣, 𝑣} ∈ ran 𝐸 → (𝑉 ∈ V → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0))) |
40 | 39 | 2a1d 26 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝑣, 𝑣} ∈ ran 𝐸 → (𝑉 = {𝑣} → (𝐾 ∈ ℕ0 → (𝑉 ∈ V → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0))))) |
41 | 31, 40 | sylbi 206 |
. . . . . . . . . . . . . . . . . 18
⊢
(⦋𝑣 /
𝑛⦌{𝑣, 𝑛} ∈ ran 𝐸 → (𝑉 = {𝑣} → (𝐾 ∈ ℕ0 → (𝑉 ∈ V → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0))))) |
42 | 24, 41 | sylbi 206 |
. . . . . . . . . . . . . . . . 17
⊢
([𝑣 / 𝑛]{𝑣, 𝑛} ∈ ran 𝐸 → (𝑉 = {𝑣} → (𝐾 ∈ ℕ0 → (𝑉 ∈ V → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0))))) |
43 | 22, 42 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
((#‘{𝑛 ∈
{𝑣} ∣ {𝑣, 𝑛} ∈ ran 𝐸}) = 1 → (𝑉 = {𝑣} → (𝐾 ∈ ℕ0 → (𝑉 ∈ V → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0))))) |
44 | 21, 43 | syl6bi 242 |
. . . . . . . . . . . . . . 15
⊢ (𝐾 = 1 → ((#‘{𝑛 ∈ {𝑣} ∣ {𝑣, 𝑛} ∈ ran 𝐸}) = 𝐾 → (𝑉 = {𝑣} → (𝐾 ∈ ℕ0 → (𝑉 ∈ V → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0)))))) |
45 | 20, 44 | jaoi 393 |
. . . . . . . . . . . . . 14
⊢ ((𝐾 = 0 ∨ 𝐾 = 1) → ((#‘{𝑛 ∈ {𝑣} ∣ {𝑣, 𝑛} ∈ ran 𝐸}) = 𝐾 → (𝑉 = {𝑣} → (𝐾 ∈ ℕ0 → (𝑉 ∈ V → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0)))))) |
46 | 17, 45 | mpcom 37 |
. . . . . . . . . . . . 13
⊢
((#‘{𝑛 ∈
{𝑣} ∣ {𝑣, 𝑛} ∈ ran 𝐸}) = 𝐾 → (𝑉 = {𝑣} → (𝐾 ∈ ℕ0 → (𝑉 ∈ V → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0))))) |
47 | 46 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑉 = {𝑣} → ((#‘{𝑛 ∈ {𝑣} ∣ {𝑣, 𝑛} ∈ ran 𝐸}) = 𝐾 → (𝐾 ∈ ℕ0 → (𝑉 ∈ V → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0))))) |
48 | 16, 47 | sylbid 229 |
. . . . . . . . . . 11
⊢ (𝑉 = {𝑣} → (∀𝑘 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸}) = 𝐾 → (𝐾 ∈ ℕ0 → (𝑉 ∈ V → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0))))) |
49 | 48 | com24 93 |
. . . . . . . . . 10
⊢ (𝑉 = {𝑣} → (𝑉 ∈ V → (𝐾 ∈ ℕ0 →
(∀𝑘 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸}) = 𝐾 → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0))))) |
50 | 49 | exlimiv 1845 |
. . . . . . . . 9
⊢
(∃𝑣 𝑉 = {𝑣} → (𝑉 ∈ V → (𝐾 ∈ ℕ0 →
(∀𝑘 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸}) = 𝐾 → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0))))) |
51 | 50 | com12 32 |
. . . . . . . 8
⊢ (𝑉 ∈ V → (∃𝑣 𝑉 = {𝑣} → (𝐾 ∈ ℕ0 →
(∀𝑘 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸}) = 𝐾 → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0))))) |
52 | 3, 51 | sylbid 229 |
. . . . . . 7
⊢ (𝑉 ∈ V → ((#‘𝑉) = 1 → (𝐾 ∈ ℕ0 →
(∀𝑘 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸}) = 𝐾 → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → 𝐾 = 0))))) |
53 | 52 | com25 97 |
. . . . . 6
⊢ (𝑉 ∈ V → ((𝐸 ∈ V ∧ 𝑉 USGrph 𝐸) → (𝐾 ∈ ℕ0 →
(∀𝑘 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸}) = 𝐾 → ((#‘𝑉) = 1 → 𝐾 = 0))))) |
54 | 53 | expdimp 452 |
. . . . 5
⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (𝑉 USGrph 𝐸 → (𝐾 ∈ ℕ0 →
(∀𝑘 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸}) = 𝐾 → ((#‘𝑉) = 1 → 𝐾 = 0))))) |
55 | 2, 54 | mpcom 37 |
. . . 4
⊢ (𝑉 USGrph 𝐸 → (𝐾 ∈ ℕ0 →
(∀𝑘 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸}) = 𝐾 → ((#‘𝑉) = 1 → 𝐾 = 0)))) |
56 | 55 | 3imp 1249 |
. . 3
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑘 ∈ 𝑉 (#‘{𝑛 ∈ 𝑉 ∣ {𝑘, 𝑛} ∈ ran 𝐸}) = 𝐾) → ((#‘𝑉) = 1 → 𝐾 = 0)) |
57 | 1, 56 | syl 17 |
. 2
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 → ((#‘𝑉) = 1 → 𝐾 = 0)) |
58 | 57 | impcom 445 |
1
⊢
(((#‘𝑉) = 1
∧ 〈𝑉, 𝐸〉 RegUSGrph 𝐾) → 𝐾 = 0) |