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 ) )

Metamath Proof Explorer

Theorem uvtx01vtx

Proof