Step | Hyp | Ref
| Expression |
1 | | uvtxel.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
2 | 1 | uvtxval 27096 |
. . . 4
⊢
(UnivVtx‘𝐺) =
{𝑣 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)} |
3 | 2 | a1i 11 |
. . 3
⊢ (𝐸 = ∅ →
(UnivVtx‘𝐺) = {𝑣 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)}) |
4 | 3 | neeq1d 3072 |
. 2
⊢ (𝐸 = ∅ →
((UnivVtx‘𝐺) ≠
∅ ↔ {𝑣 ∈
𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)} ≠ ∅)) |
5 | | rabn0 4336 |
. . 3
⊢ ({𝑣 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)} ≠ ∅ ↔ ∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)) |
6 | 5 | a1i 11 |
. 2
⊢ (𝐸 = ∅ → ({𝑣 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)} ≠ ∅ ↔ ∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣))) |
7 | | falseral0 4455 |
. . . . . . . . . 10
⊢
((∀𝑛 ¬
𝑛 ∈ ∅ ∧
∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) → (𝑉 ∖ {𝑣}) = ∅) |
8 | 7 | ex 413 |
. . . . . . . . 9
⊢
(∀𝑛 ¬
𝑛 ∈ ∅ →
(∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅ → (𝑉 ∖ {𝑣}) = ∅)) |
9 | | noel 4293 |
. . . . . . . . 9
⊢ ¬
𝑛 ∈
∅ |
10 | 8, 9 | mpg 1789 |
. . . . . . . 8
⊢
(∀𝑛 ∈
(𝑉 ∖ {𝑣})𝑛 ∈ ∅ → (𝑉 ∖ {𝑣}) = ∅) |
11 | | ssdif0 4320 |
. . . . . . . . 9
⊢ (𝑉 ⊆ {𝑣} ↔ (𝑉 ∖ {𝑣}) = ∅) |
12 | | sssn 4751 |
. . . . . . . . . 10
⊢ (𝑉 ⊆ {𝑣} ↔ (𝑉 = ∅ ∨ 𝑉 = {𝑣})) |
13 | | ne0i 4297 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ 𝑉 → 𝑉 ≠ ∅) |
14 | | eqneqall 3024 |
. . . . . . . . . . . 12
⊢ (𝑉 = ∅ → (𝑉 ≠ ∅ → 𝑉 = {𝑣})) |
15 | 13, 14 | syl5 34 |
. . . . . . . . . . 11
⊢ (𝑉 = ∅ → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
16 | | ax-1 6 |
. . . . . . . . . . 11
⊢ (𝑉 = {𝑣} → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
17 | 15, 16 | jaoi 851 |
. . . . . . . . . 10
⊢ ((𝑉 = ∅ ∨ 𝑉 = {𝑣}) → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
18 | 12, 17 | sylbi 218 |
. . . . . . . . 9
⊢ (𝑉 ⊆ {𝑣} → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
19 | 11, 18 | sylbir 236 |
. . . . . . . 8
⊢ ((𝑉 ∖ {𝑣}) = ∅ → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
20 | 10, 19 | syl 17 |
. . . . . . 7
⊢
(∀𝑛 ∈
(𝑉 ∖ {𝑣})𝑛 ∈ ∅ → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
21 | 20 | impcom 408 |
. . . . . 6
⊢ ((𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) → 𝑉 = {𝑣}) |
22 | | vsnid 4592 |
. . . . . . . 8
⊢ 𝑣 ∈ {𝑣} |
23 | | eleq2 2898 |
. . . . . . . 8
⊢ (𝑉 = {𝑣} → (𝑣 ∈ 𝑉 ↔ 𝑣 ∈ {𝑣})) |
24 | 22, 23 | mpbiri 259 |
. . . . . . 7
⊢ (𝑉 = {𝑣} → 𝑣 ∈ 𝑉) |
25 | | ralel 3146 |
. . . . . . . 8
⊢
∀𝑛 ∈
∅ 𝑛 ∈
∅ |
26 | | difeq1 4089 |
. . . . . . . . . 10
⊢ (𝑉 = {𝑣} → (𝑉 ∖ {𝑣}) = ({𝑣} ∖ {𝑣})) |
27 | | difid 4327 |
. . . . . . . . . 10
⊢ ({𝑣} ∖ {𝑣}) = ∅ |
28 | 26, 27 | syl6eq 2869 |
. . . . . . . . 9
⊢ (𝑉 = {𝑣} → (𝑉 ∖ {𝑣}) = ∅) |
29 | 28 | raleqdv 3413 |
. . . . . . . 8
⊢ (𝑉 = {𝑣} → (∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅ ↔ ∀𝑛 ∈ ∅ 𝑛 ∈
∅)) |
30 | 25, 29 | mpbiri 259 |
. . . . . . 7
⊢ (𝑉 = {𝑣} → ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) |
31 | 24, 30 | jca 512 |
. . . . . 6
⊢ (𝑉 = {𝑣} → (𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅)) |
32 | 21, 31 | impbii 210 |
. . . . 5
⊢ ((𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) ↔ 𝑉 = {𝑣}) |
33 | 32 | a1i 11 |
. . . 4
⊢ (𝐸 = ∅ → ((𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) ↔ 𝑉 = {𝑣})) |
34 | 33 | exbidv 1913 |
. . 3
⊢ (𝐸 = ∅ → (∃𝑣(𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) ↔ ∃𝑣 𝑉 = {𝑣})) |
35 | | isuvtx.e |
. . . . . . . 8
⊢ 𝐸 = (Edg‘𝐺) |
36 | 35 | eqeq1i 2823 |
. . . . . . 7
⊢ (𝐸 = ∅ ↔
(Edg‘𝐺) =
∅) |
37 | | nbgr0edg 27066 |
. . . . . . 7
⊢
((Edg‘𝐺) =
∅ → (𝐺 NeighbVtx
𝑣) =
∅) |
38 | 36, 37 | sylbi 218 |
. . . . . 6
⊢ (𝐸 = ∅ → (𝐺 NeighbVtx 𝑣) = ∅) |
39 | 38 | eleq2d 2895 |
. . . . 5
⊢ (𝐸 = ∅ → (𝑛 ∈ (𝐺 NeighbVtx 𝑣) ↔ 𝑛 ∈ ∅)) |
40 | 39 | rexralbidv 3298 |
. . . 4
⊢ (𝐸 = ∅ → (∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣) ↔ ∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅)) |
41 | | df-rex 3141 |
. . . 4
⊢
(∃𝑣 ∈
𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅ ↔ ∃𝑣(𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅)) |
42 | 40, 41 | syl6bb 288 |
. . 3
⊢ (𝐸 = ∅ → (∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣) ↔ ∃𝑣(𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅))) |
43 | 1 | fvexi 6677 |
. . . 4
⊢ 𝑉 ∈ V |
44 | | hash1snb 13768 |
. . . 4
⊢ (𝑉 ∈ V →
((♯‘𝑉) = 1
↔ ∃𝑣 𝑉 = {𝑣})) |
45 | 43, 44 | mp1i 13 |
. . 3
⊢ (𝐸 = ∅ →
((♯‘𝑉) = 1
↔ ∃𝑣 𝑉 = {𝑣})) |
46 | 34, 42, 45 | 3bitr4d 312 |
. 2
⊢ (𝐸 = ∅ → (∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣) ↔ (♯‘𝑉) = 1)) |
47 | 4, 6, 46 | 3bitrd 306 |
1
⊢ (𝐸 = ∅ →
((UnivVtx‘𝐺) ≠
∅ ↔ (♯‘𝑉) = 1)) |