Metamath Proof Explorer


Theorem uvtx01vtx

Description: If a graph/class has no edges, it has universal vertices if and only if it has exactly one vertex. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 30-Oct-2020) (Revised by AV, 14-Feb-2022)

Ref Expression
Hypotheses uvtxel.v 𝑉 = ( Vtx ‘ 𝐺 )
isuvtx.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion uvtx01vtx ( 𝐸 = ∅ → ( ( UnivVtx ‘ 𝐺 ) ≠ ∅ ↔ ( ♯ ‘ 𝑉 ) = 1 ) )

Proof

Step Hyp Ref Expression
1 uvtxel.v 𝑉 = ( Vtx ‘ 𝐺 )
2 isuvtx.e 𝐸 = ( Edg ‘ 𝐺 )
3 1 uvtxval ( UnivVtx ‘ 𝐺 ) = { 𝑣𝑉 ∣ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) }
4 3 a1i ( 𝐸 = ∅ → ( UnivVtx ‘ 𝐺 ) = { 𝑣𝑉 ∣ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) } )
5 4 neeq1d ( 𝐸 = ∅ → ( ( UnivVtx ‘ 𝐺 ) ≠ ∅ ↔ { 𝑣𝑉 ∣ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) } ≠ ∅ ) )
6 rabn0 ( { 𝑣𝑉 ∣ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) } ≠ ∅ ↔ ∃ 𝑣𝑉𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) )
7 6 a1i ( 𝐸 = ∅ → ( { 𝑣𝑉 ∣ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) } ≠ ∅ ↔ ∃ 𝑣𝑉𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
8 falseral0 ( ( ∀ 𝑛 ¬ 𝑛 ∈ ∅ ∧ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ∅ ) → ( 𝑉 ∖ { 𝑣 } ) = ∅ )
9 8 ex ( ∀ 𝑛 ¬ 𝑛 ∈ ∅ → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ∅ → ( 𝑉 ∖ { 𝑣 } ) = ∅ ) )
10 noel ¬ 𝑛 ∈ ∅
11 9 10 mpg ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ∅ → ( 𝑉 ∖ { 𝑣 } ) = ∅ )
12 ssdif0 ( 𝑉 ⊆ { 𝑣 } ↔ ( 𝑉 ∖ { 𝑣 } ) = ∅ )
13 sssn ( 𝑉 ⊆ { 𝑣 } ↔ ( 𝑉 = ∅ ∨ 𝑉 = { 𝑣 } ) )
14 ne0i ( 𝑣𝑉𝑉 ≠ ∅ )
15 eqneqall ( 𝑉 = ∅ → ( 𝑉 ≠ ∅ → 𝑉 = { 𝑣 } ) )
16 14 15 syl5 ( 𝑉 = ∅ → ( 𝑣𝑉𝑉 = { 𝑣 } ) )
17 ax-1 ( 𝑉 = { 𝑣 } → ( 𝑣𝑉𝑉 = { 𝑣 } ) )
18 16 17 jaoi ( ( 𝑉 = ∅ ∨ 𝑉 = { 𝑣 } ) → ( 𝑣𝑉𝑉 = { 𝑣 } ) )
19 13 18 sylbi ( 𝑉 ⊆ { 𝑣 } → ( 𝑣𝑉𝑉 = { 𝑣 } ) )
20 12 19 sylbir ( ( 𝑉 ∖ { 𝑣 } ) = ∅ → ( 𝑣𝑉𝑉 = { 𝑣 } ) )
21 11 20 syl ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ∅ → ( 𝑣𝑉𝑉 = { 𝑣 } ) )
22 21 impcom ( ( 𝑣𝑉 ∧ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ∅ ) → 𝑉 = { 𝑣 } )
23 vsnid 𝑣 ∈ { 𝑣 }
24 eleq2 ( 𝑉 = { 𝑣 } → ( 𝑣𝑉𝑣 ∈ { 𝑣 } ) )
25 23 24 mpbiri ( 𝑉 = { 𝑣 } → 𝑣𝑉 )
26 ralel 𝑛 ∈ ∅ 𝑛 ∈ ∅
27 difeq1 ( 𝑉 = { 𝑣 } → ( 𝑉 ∖ { 𝑣 } ) = ( { 𝑣 } ∖ { 𝑣 } ) )
28 difid ( { 𝑣 } ∖ { 𝑣 } ) = ∅
29 27 28 eqtrdi ( 𝑉 = { 𝑣 } → ( 𝑉 ∖ { 𝑣 } ) = ∅ )
30 29 raleqdv ( 𝑉 = { 𝑣 } → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ∅ ↔ ∀ 𝑛 ∈ ∅ 𝑛 ∈ ∅ ) )
31 26 30 mpbiri ( 𝑉 = { 𝑣 } → ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ∅ )
32 25 31 jca ( 𝑉 = { 𝑣 } → ( 𝑣𝑉 ∧ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ∅ ) )
33 22 32 impbii ( ( 𝑣𝑉 ∧ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ∅ ) ↔ 𝑉 = { 𝑣 } )
34 33 a1i ( 𝐸 = ∅ → ( ( 𝑣𝑉 ∧ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ∅ ) ↔ 𝑉 = { 𝑣 } ) )
35 34 exbidv ( 𝐸 = ∅ → ( ∃ 𝑣 ( 𝑣𝑉 ∧ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ∅ ) ↔ ∃ 𝑣 𝑉 = { 𝑣 } ) )
36 2 eqeq1i ( 𝐸 = ∅ ↔ ( Edg ‘ 𝐺 ) = ∅ )
37 nbgr0edg ( ( Edg ‘ 𝐺 ) = ∅ → ( 𝐺 NeighbVtx 𝑣 ) = ∅ )
38 36 37 sylbi ( 𝐸 = ∅ → ( 𝐺 NeighbVtx 𝑣 ) = ∅ )
39 38 eleq2d ( 𝐸 = ∅ → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ 𝑛 ∈ ∅ ) )
40 39 rexralbidv ( 𝐸 = ∅ → ( ∃ 𝑣𝑉𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ∃ 𝑣𝑉𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ∅ ) )
41 df-rex ( ∃ 𝑣𝑉𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ∅ ↔ ∃ 𝑣 ( 𝑣𝑉 ∧ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ∅ ) )
42 40 41 bitrdi ( 𝐸 = ∅ → ( ∃ 𝑣𝑉𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ∃ 𝑣 ( 𝑣𝑉 ∧ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ∅ ) ) )
43 1 fvexi 𝑉 ∈ V
44 hash1snb ( 𝑉 ∈ V → ( ( ♯ ‘ 𝑉 ) = 1 ↔ ∃ 𝑣 𝑉 = { 𝑣 } ) )
45 43 44 mp1i ( 𝐸 = ∅ → ( ( ♯ ‘ 𝑉 ) = 1 ↔ ∃ 𝑣 𝑉 = { 𝑣 } ) )
46 35 42 45 3bitr4d ( 𝐸 = ∅ → ( ∃ 𝑣𝑉𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ( ♯ ‘ 𝑉 ) = 1 ) )
47 5 7 46 3bitrd ( 𝐸 = ∅ → ( ( UnivVtx ‘ 𝐺 ) ≠ ∅ ↔ ( ♯ ‘ 𝑉 ) = 1 ) )