This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cplgr1v

Description: A graph with one vertex is complete. (Contributed by Alexander van der Vekens, 13-Oct-2017) (Revised by AV, 1-Nov-2020) (Revised by AV, 23-Mar-2021) (Proof shortened by AV, 14-Feb-2022)

Ref Expression
Hypothesis cplgr0v.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion cplgr1v ( ( ♯ ‘ 𝑉 ) = 1 → 𝐺 ∈ ComplGraph )

Proof

Step Hyp Ref Expression
1 cplgr0v.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 simpr ⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ 𝑉 )
3 ral0 ⊢ ∀ 𝑛 ∈ ∅ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 )
4 1 fvexi ⊢ 𝑉 ∈ V
5 hash1snb ⊢ ( 𝑉 ∈ V → ( ( ♯ ‘ 𝑉 ) = 1 ↔ ∃ 𝑛 𝑉 = { 𝑛 } ) )
6 4 5 ax-mp ⊢ ( ( ♯ ‘ 𝑉 ) = 1 ↔ ∃ 𝑛 𝑉 = { 𝑛 } )
7 velsn ⊢ ( 𝑣 ∈ { 𝑛 } ↔ 𝑣 = 𝑛 )
8 sneq ⊢ ( 𝑣 = 𝑛 → { 𝑣 } = { 𝑛 } )
9 8 difeq2d ⊢ ( 𝑣 = 𝑛 → ( { 𝑛 } ∖ { 𝑣 } ) = ( { 𝑛 } ∖ { 𝑛 } ) )
10 difid ⊢ ( { 𝑛 } ∖ { 𝑛 } ) = ∅
11 9 10 eqtrdi ⊢ ( 𝑣 = 𝑛 → ( { 𝑛 } ∖ { 𝑣 } ) = ∅ )
12 7 11 sylbi ⊢ ( 𝑣 ∈ { 𝑛 } → ( { 𝑛 } ∖ { 𝑣 } ) = ∅ )
13 12 a1i ⊢ ( 𝑉 = { 𝑛 } → ( 𝑣 ∈ { 𝑛 } → ( { 𝑛 } ∖ { 𝑣 } ) = ∅ ) )
14 eleq2 ⊢ ( 𝑉 = { 𝑛 } → ( 𝑣 ∈ 𝑉 ↔ 𝑣 ∈ { 𝑛 } ) )
15 difeq1 ⊢ ( 𝑉 = { 𝑛 } → ( 𝑉 ∖ { 𝑣 } ) = ( { 𝑛 } ∖ { 𝑣 } ) )
16 15 eqeq1d ⊢ ( 𝑉 = { 𝑛 } → ( ( 𝑉 ∖ { 𝑣 } ) = ∅ ↔ ( { 𝑛 } ∖ { 𝑣 } ) = ∅ ) )
17 13 14 16 3imtr4d ⊢ ( 𝑉 = { 𝑛 } → ( 𝑣 ∈ 𝑉 → ( 𝑉 ∖ { 𝑣 } ) = ∅ ) )
18 17 exlimiv ⊢ ( ∃ 𝑛 𝑉 = { 𝑛 } → ( 𝑣 ∈ 𝑉 → ( 𝑉 ∖ { 𝑣 } ) = ∅ ) )
19 6 18 sylbi ⊢ ( ( ♯ ‘ 𝑉 ) = 1 → ( 𝑣 ∈ 𝑉 → ( 𝑉 ∖ { 𝑣 } ) = ∅ ) )
20 19 imp ⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ 𝑣 ∈ 𝑉 ) → ( 𝑉 ∖ { 𝑣 } ) = ∅ )
21 20 raleqdv ⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ 𝑣 ∈ 𝑉 ) → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ∀ 𝑛 ∈ ∅ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
22 3 21 mpbiri ⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ 𝑣 ∈ 𝑉 ) → ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) )
23 1 uvtxel ⊢ ( 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ↔ ( 𝑣 ∈ 𝑉 ∧ ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
24 2 22 23 sylanbrc ⊢ ( ( ( ♯ ‘ 𝑉 ) = 1 ∧ 𝑣 ∈ 𝑉 ) → 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) )
25 24 ralrimiva ⊢ ( ( ♯ ‘ 𝑉 ) = 1 → ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) )
26 1 cplgr1vlem ⊢ ( ( ♯ ‘ 𝑉 ) = 1 → 𝐺 ∈ V )
27 1 iscplgr ⊢ ( 𝐺 ∈ V → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ) )
28 26 27 syl ⊢ ( ( ♯ ‘ 𝑉 ) = 1 → ( 𝐺 ∈ ComplGraph ↔ ∀ 𝑣 ∈ 𝑉 𝑣 ∈ ( UnivVtx ‘ 𝐺 ) ) )
29 25 28 mpbird ⊢ ( ( ♯ ‘ 𝑉 ) = 1 → 𝐺 ∈ ComplGraph )