Step |
Hyp |
Ref |
Expression |
1 |
|
uvtxnm1nbgr.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
1
|
nbgrssovtx |
⊢ ( 𝐺 NeighbVtx 𝑈 ) ⊆ ( 𝑉 ∖ { 𝑈 } ) |
3 |
2
|
sseli |
⊢ ( 𝑣 ∈ ( 𝐺 NeighbVtx 𝑈 ) → 𝑣 ∈ ( 𝑉 ∖ { 𝑈 } ) ) |
4 |
|
eldifsn |
⊢ ( 𝑣 ∈ ( 𝑉 ∖ { 𝑈 } ) ↔ ( 𝑣 ∈ 𝑉 ∧ 𝑣 ≠ 𝑈 ) ) |
5 |
1
|
nbusgrvtxm1 |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → ( ( 𝑣 ∈ 𝑉 ∧ 𝑣 ≠ 𝑈 ) → 𝑣 ∈ ( 𝐺 NeighbVtx 𝑈 ) ) ) ) |
6 |
5
|
imp |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) ∧ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( ( 𝑣 ∈ 𝑉 ∧ 𝑣 ≠ 𝑈 ) → 𝑣 ∈ ( 𝐺 NeighbVtx 𝑈 ) ) ) |
7 |
4 6
|
syl5bi |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) ∧ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( 𝑣 ∈ ( 𝑉 ∖ { 𝑈 } ) → 𝑣 ∈ ( 𝐺 NeighbVtx 𝑈 ) ) ) |
8 |
3 7
|
impbid2 |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) ∧ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( 𝑣 ∈ ( 𝐺 NeighbVtx 𝑈 ) ↔ 𝑣 ∈ ( 𝑉 ∖ { 𝑈 } ) ) ) |
9 |
8
|
eqrdv |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) ∧ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( 𝐺 NeighbVtx 𝑈 ) = ( 𝑉 ∖ { 𝑈 } ) ) |
10 |
1
|
uvtxnbgrb |
⊢ ( 𝑈 ∈ 𝑉 → ( 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( 𝐺 NeighbVtx 𝑈 ) = ( 𝑉 ∖ { 𝑈 } ) ) ) |
11 |
10
|
ad2antlr |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) ∧ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → ( 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( 𝐺 NeighbVtx 𝑈 ) = ( 𝑉 ∖ { 𝑈 } ) ) ) |
12 |
9 11
|
mpbird |
⊢ ( ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) ∧ ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) ) → 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) ) |
13 |
12
|
ex |
⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( ♯ ‘ 𝑉 ) − 1 ) → 𝑈 ∈ ( UnivVtx ‘ 𝐺 ) ) ) |