Step | Hyp | Ref
| Expression |
1 | | uvtxael.v |
. . . . 5
⊢ 𝑉 = (Vtx‘𝐺) |
2 | 1 | uvtxaval 40613 |
. . . 4
⊢ (𝐺 ∈ 𝑊 → (UnivVtx‘𝐺) = {𝑣 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)}) |
3 | 2 | adantr 480 |
. . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐸 = ∅) → (UnivVtx‘𝐺) = {𝑣 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)}) |
4 | 3 | neeq1d 2841 |
. 2
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐸 = ∅) → ((UnivVtx‘𝐺) ≠ ∅ ↔ {𝑣 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)} ≠ ∅)) |
5 | | rabn0 3912 |
. . 3
⊢ ({𝑣 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)} ≠ ∅ ↔ ∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)) |
6 | 5 | a1i 11 |
. 2
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐸 = ∅) → ({𝑣 ∈ 𝑉 ∣ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣)} ≠ ∅ ↔ ∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣))) |
7 | | falseral0 40308 |
. . . . . . . . . 10
⊢
((∀𝑛 ¬
𝑛 ∈ ∅ ∧
∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) → (𝑉 ∖ {𝑣}) = ∅) |
8 | 7 | ex 449 |
. . . . . . . . 9
⊢
(∀𝑛 ¬
𝑛 ∈ ∅ →
(∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅ → (𝑉 ∖ {𝑣}) = ∅)) |
9 | | noel 3878 |
. . . . . . . . 9
⊢ ¬
𝑛 ∈
∅ |
10 | 8, 9 | mpg 1715 |
. . . . . . . 8
⊢
(∀𝑛 ∈
(𝑉 ∖ {𝑣})𝑛 ∈ ∅ → (𝑉 ∖ {𝑣}) = ∅) |
11 | | ssdif0 3896 |
. . . . . . . . 9
⊢ (𝑉 ⊆ {𝑣} ↔ (𝑉 ∖ {𝑣}) = ∅) |
12 | | sssn 4298 |
. . . . . . . . . 10
⊢ (𝑉 ⊆ {𝑣} ↔ (𝑉 = ∅ ∨ 𝑉 = {𝑣})) |
13 | | ne0i 3880 |
. . . . . . . . . . . 12
⊢ (𝑣 ∈ 𝑉 → 𝑉 ≠ ∅) |
14 | | eqneqall 2793 |
. . . . . . . . . . . 12
⊢ (𝑉 = ∅ → (𝑉 ≠ ∅ → 𝑉 = {𝑣})) |
15 | 13, 14 | syl5 33 |
. . . . . . . . . . 11
⊢ (𝑉 = ∅ → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
16 | | ax-1 6 |
. . . . . . . . . . 11
⊢ (𝑉 = {𝑣} → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
17 | 15, 16 | jaoi 393 |
. . . . . . . . . 10
⊢ ((𝑉 = ∅ ∨ 𝑉 = {𝑣}) → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
18 | 12, 17 | sylbi 206 |
. . . . . . . . 9
⊢ (𝑉 ⊆ {𝑣} → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
19 | 11, 18 | sylbir 224 |
. . . . . . . 8
⊢ ((𝑉 ∖ {𝑣}) = ∅ → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
20 | 10, 19 | syl 17 |
. . . . . . 7
⊢
(∀𝑛 ∈
(𝑉 ∖ {𝑣})𝑛 ∈ ∅ → (𝑣 ∈ 𝑉 → 𝑉 = {𝑣})) |
21 | 20 | impcom 445 |
. . . . . 6
⊢ ((𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) → 𝑉 = {𝑣}) |
22 | | vsnid 4156 |
. . . . . . . 8
⊢ 𝑣 ∈ {𝑣} |
23 | | eleq2 2677 |
. . . . . . . 8
⊢ (𝑉 = {𝑣} → (𝑣 ∈ 𝑉 ↔ 𝑣 ∈ {𝑣})) |
24 | 22, 23 | mpbiri 247 |
. . . . . . 7
⊢ (𝑉 = {𝑣} → 𝑣 ∈ 𝑉) |
25 | | ral0 4028 |
. . . . . . . 8
⊢
∀𝑛 ∈
∅ 𝑛 ∈
∅ |
26 | | difeq1 3683 |
. . . . . . . . . 10
⊢ (𝑉 = {𝑣} → (𝑉 ∖ {𝑣}) = ({𝑣} ∖ {𝑣})) |
27 | | difid 3902 |
. . . . . . . . . 10
⊢ ({𝑣} ∖ {𝑣}) = ∅ |
28 | 26, 27 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑉 = {𝑣} → (𝑉 ∖ {𝑣}) = ∅) |
29 | 28 | raleqdv 3121 |
. . . . . . . 8
⊢ (𝑉 = {𝑣} → (∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅ ↔ ∀𝑛 ∈ ∅ 𝑛 ∈
∅)) |
30 | 25, 29 | mpbiri 247 |
. . . . . . 7
⊢ (𝑉 = {𝑣} → ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) |
31 | 24, 30 | jca 553 |
. . . . . 6
⊢ (𝑉 = {𝑣} → (𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅)) |
32 | 21, 31 | impbii 198 |
. . . . 5
⊢ ((𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) ↔ 𝑉 = {𝑣}) |
33 | 32 | a1i 11 |
. . . 4
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐸 = ∅) → ((𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) ↔ 𝑉 = {𝑣})) |
34 | 33 | exbidv 1837 |
. . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐸 = ∅) → (∃𝑣(𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅) ↔ ∃𝑣 𝑉 = {𝑣})) |
35 | | isuvtxa.e |
. . . . . . . . . 10
⊢ 𝐸 = (Edg‘𝐺) |
36 | 35 | eqeq1i 2615 |
. . . . . . . . 9
⊢ (𝐸 = ∅ ↔
(Edg‘𝐺) =
∅) |
37 | | nbgr0edg 40579 |
. . . . . . . . 9
⊢
((Edg‘𝐺) =
∅ → (𝐺 NeighbVtx
𝑣) =
∅) |
38 | 36, 37 | sylbi 206 |
. . . . . . . 8
⊢ (𝐸 = ∅ → (𝐺 NeighbVtx 𝑣) = ∅) |
39 | 38 | eleq2d 2673 |
. . . . . . 7
⊢ (𝐸 = ∅ → (𝑛 ∈ (𝐺 NeighbVtx 𝑣) ↔ 𝑛 ∈ ∅)) |
40 | 39 | ralbidv 2969 |
. . . . . 6
⊢ (𝐸 = ∅ → (∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣) ↔ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅)) |
41 | 40 | rexbidv 3034 |
. . . . 5
⊢ (𝐸 = ∅ → (∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣) ↔ ∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅)) |
42 | 41 | adantl 481 |
. . . 4
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐸 = ∅) → (∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣) ↔ ∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅)) |
43 | | df-rex 2902 |
. . . 4
⊢
(∃𝑣 ∈
𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅ ↔ ∃𝑣(𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅)) |
44 | 42, 43 | syl6bb 275 |
. . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐸 = ∅) → (∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣) ↔ ∃𝑣(𝑣 ∈ 𝑉 ∧ ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ ∅))) |
45 | | fvex 6113 |
. . . . 5
⊢
(Vtx‘𝐺) ∈
V |
46 | 1, 45 | eqeltri 2684 |
. . . 4
⊢ 𝑉 ∈ V |
47 | | hash1snb 13068 |
. . . 4
⊢ (𝑉 ∈ V → ((#‘𝑉) = 1 ↔ ∃𝑣 𝑉 = {𝑣})) |
48 | 46, 47 | mp1i 13 |
. . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐸 = ∅) → ((#‘𝑉) = 1 ↔ ∃𝑣 𝑉 = {𝑣})) |
49 | 34, 44, 48 | 3bitr4d 299 |
. 2
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐸 = ∅) → (∃𝑣 ∈ 𝑉 ∀𝑛 ∈ (𝑉 ∖ {𝑣})𝑛 ∈ (𝐺 NeighbVtx 𝑣) ↔ (#‘𝑉) = 1)) |
50 | 4, 6, 49 | 3bitrd 293 |
1
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐸 = ∅) → ((UnivVtx‘𝐺) ≠ ∅ ↔
(#‘𝑉) =
1)) |