Step | Hyp | Ref
| Expression |
1 | | uvtxel.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
2 | 1 | uvtxval 27754 |
. . . 4
⊢
(UnivVtx‘𝐺) =
{𝑣 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)} |
3 | 2 | a1i 11 |
. . 3
⊢ (𝐸 = ∅ →
(UnivVtx‘𝐺) = {𝑣 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)}) |
4 | 3 | neeq1d 3003 |
. 2
⊢ (𝐸 = ∅ →
((UnivVtx‘𝐺) ≠
∅ ↔ {𝑣 ∈
𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)} ≠ ∅)) |
5 | | rabn0 4319 |
. . 3
⊢ ({𝑣 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)} ≠ ∅ ↔ ∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)) |
6 | 5 | a1i 11 |
. 2
⊢ (𝐸 = ∅ → ({𝑣 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)} ≠ ∅ ↔ ∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣))) |
7 | | falseral0 4450 |
. . . . . . . . . 10
⊢
((∀𝑛 ¬
𝑛 ∈ ∅ ∧
∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) → (𝑉 ∖ {𝑣}) = ∅) |
8 | 7 | ex 413 |
. . . . . . . . 9
⊢
(∀𝑛 ¬
𝑛 ∈ ∅ →
(∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅ → (𝑉 ∖ {𝑣}) = ∅)) |
9 | | noel 4264 |
. . . . . . . . 9
⊢ ¬
𝑛 ∈
∅ |
10 | 8, 9 | mpg 1800 |
. . . . . . . 8
⊢
(∀𝑛 ∈
(𝑉 ∖ {𝑣})𝑛 ∈ ∅ → (𝑉 ∖ {𝑣}) = ∅) |
11 | | ssdif0 4297 |
. . . . . . . . 9
⊢ (𝑉 ⊆ {𝑣} ↔ (𝑉 ∖ {𝑣}) = ∅) |
12 | | sssn 4759 |
. . . . . . . . . 10
⊢ (𝑉 ⊆ {𝑣} ↔ (𝑉 = ∅ ∨ 𝑉 = {𝑣})) |
13 | | ne0i 4268 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ 𝑉 → 𝑉 ≠ ∅) |
14 | | eqneqall 2954 |
. . . . . . . . . . . 12
⊢ (𝑉 = ∅ → (𝑉 ≠ ∅ → 𝑉 = {𝑣})) |
15 | 13, 14 | syl5 34 |
. . . . . . . . . . 11
⊢ (𝑉 = ∅ → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
16 | | ax-1 6 |
. . . . . . . . . . 11
⊢ (𝑉 = {𝑣} → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
17 | 15, 16 | jaoi 854 |
. . . . . . . . . 10
⊢ ((𝑉 = ∅ ∨ 𝑉 = {𝑣}) → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
18 | 12, 17 | sylbi 216 |
. . . . . . . . 9
⊢ (𝑉 ⊆ {𝑣} → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
19 | 11, 18 | sylbir 234 |
. . . . . . . 8
⊢ ((𝑉 ∖ {𝑣}) = ∅ → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
20 | 10, 19 | syl 17 |
. . . . . . 7
⊢
(∀𝑛 ∈
(𝑉 ∖ {𝑣})𝑛 ∈ ∅ → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
21 | 20 | impcom 408 |
. . . . . 6
⊢ ((𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) → 𝑉 = {𝑣}) |
22 | | vsnid 4598 |
. . . . . . . 8
⊢ 𝑣 ∈ {𝑣} |
23 | | eleq2 2827 |
. . . . . . . 8
⊢ (𝑉 = {𝑣} → (𝑣 ∈ 𝑉 ↔ 𝑣 ∈ {𝑣})) |
24 | 22, 23 | mpbiri 257 |
. . . . . . 7
⊢ (𝑉 = {𝑣} → 𝑣 ∈ 𝑉) |
25 | | ralel 3075 |
. . . . . . . 8
⊢
∀𝑛 ∈
∅ 𝑛 ∈
∅ |
26 | | difeq1 4050 |
. . . . . . . . . 10
⊢ (𝑉 = {𝑣} → (𝑉 ∖ {𝑣}) = ({𝑣} ∖ {𝑣})) |
27 | | difid 4304 |
. . . . . . . . . 10
⊢ ({𝑣} ∖ {𝑣}) = ∅ |
28 | 26, 27 | eqtrdi 2794 |
. . . . . . . . 9
⊢ (𝑉 = {𝑣} → (𝑉 ∖ {𝑣}) = ∅) |
29 | 28 | raleqdv 3348 |
. . . . . . . 8
⊢ (𝑉 = {𝑣} → (∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅ ↔ ∀𝑛 ∈ ∅ 𝑛 ∈
∅)) |
30 | 25, 29 | mpbiri 257 |
. . . . . . 7
⊢ (𝑉 = {𝑣} → ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) |
31 | 24, 30 | jca 512 |
. . . . . 6
⊢ (𝑉 = {𝑣} → (𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅)) |
32 | 21, 31 | impbii 208 |
. . . . 5
⊢ ((𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) ↔ 𝑉 = {𝑣}) |
33 | 32 | a1i 11 |
. . . 4
⊢ (𝐸 = ∅ → ((𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) ↔ 𝑉 = {𝑣})) |
34 | 33 | exbidv 1924 |
. . 3
⊢ (𝐸 = ∅ → (∃𝑣(𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) ↔ ∃𝑣 𝑉 = {𝑣})) |
35 | | isuvtx.e |
. . . . . . . 8
⊢ 𝐸 = (Edg‘𝐺) |
36 | 35 | eqeq1i 2743 |
. . . . . . 7
⊢ (𝐸 = ∅ ↔
(Edg‘𝐺) =
∅) |
37 | | nbgr0edg 27724 |
. . . . . . 7
⊢
((Edg‘𝐺) =
∅ → (𝐺 NeighbVtx
𝑣) =
∅) |
38 | 36, 37 | sylbi 216 |
. . . . . 6
⊢ (𝐸 = ∅ → (𝐺 NeighbVtx 𝑣) = ∅) |
39 | 38 | eleq2d 2824 |
. . . . 5
⊢ (𝐸 = ∅ → (𝑛 ∈ (𝐺 NeighbVtx 𝑣) ↔ 𝑛 ∈ ∅)) |
40 | 39 | rexralbidv 3230 |
. . . 4
⊢ (𝐸 = ∅ → (∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣) ↔ ∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅)) |
41 | | df-rex 3070 |
. . . 4
⊢
(∃𝑣 ∈
𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅ ↔ ∃𝑣(𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅)) |
42 | 40, 41 | bitrdi 287 |
. . 3
⊢ (𝐸 = ∅ → (∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣) ↔ ∃𝑣(𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅))) |
43 | 1 | fvexi 6788 |
. . . 4
⊢ 𝑉 ∈ V |
44 | | hash1snb 14134 |
. . . 4
⊢ (𝑉 ∈ V →
((♯‘𝑉) = 1
↔ ∃𝑣 𝑉 = {𝑣})) |
45 | 43, 44 | mp1i 13 |
. . 3
⊢ (𝐸 = ∅ →
((♯‘𝑉) = 1
↔ ∃𝑣 𝑉 = {𝑣})) |
46 | 34, 42, 45 | 3bitr4d 311 |
. 2
⊢ (𝐸 = ∅ → (∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣) ↔ (♯‘𝑉) = 1)) |
47 | 4, 6, 46 | 3bitrd 305 |
1
⊢ (𝐸 = ∅ →
((UnivVtx‘𝐺) ≠
∅ ↔ (♯‘𝑉) = 1)) |