Metamath Proof Explorer


Theorem nbuhgr2vtx1edgb

Description: If a hypergraph has two vertices, and there is an edge between the vertices, then each vertex is the neighbor of the other vertex. (Contributed by AV, 2-Nov-2020) (Proof shortened by AV, 13-Feb-2022)

Ref Expression
Hypotheses nbgr2vtx1edg.v 𝑉 = ( Vtx ‘ 𝐺 )
nbgr2vtx1edg.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion nbuhgr2vtx1edgb ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 2 ) → ( 𝑉𝐸 ↔ ∀ 𝑣𝑉𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )

Proof

Step Hyp Ref Expression
1 nbgr2vtx1edg.v 𝑉 = ( Vtx ‘ 𝐺 )
2 nbgr2vtx1edg.e 𝐸 = ( Edg ‘ 𝐺 )
3 1 fvexi 𝑉 ∈ V
4 hash2prb ( 𝑉 ∈ V → ( ( ♯ ‘ 𝑉 ) = 2 ↔ ∃ 𝑎𝑉𝑏𝑉 ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) ) )
5 3 4 ax-mp ( ( ♯ ‘ 𝑉 ) = 2 ↔ ∃ 𝑎𝑉𝑏𝑉 ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) )
6 simpr ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) → ( 𝑎𝑉𝑏𝑉 ) )
7 6 ancomd ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) → ( 𝑏𝑉𝑎𝑉 ) )
8 7 ad2antrr ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → ( 𝑏𝑉𝑎𝑉 ) )
9 id ( 𝑎𝑏𝑎𝑏 )
10 9 necomd ( 𝑎𝑏𝑏𝑎 )
11 10 adantr ( ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) → 𝑏𝑎 )
12 11 ad2antlr ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → 𝑏𝑎 )
13 prcom { 𝑎 , 𝑏 } = { 𝑏 , 𝑎 }
14 13 eleq1i ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { 𝑏 , 𝑎 } ∈ 𝐸 )
15 14 biimpi ( { 𝑎 , 𝑏 } ∈ 𝐸 → { 𝑏 , 𝑎 } ∈ 𝐸 )
16 sseq2 ( 𝑒 = { 𝑏 , 𝑎 } → ( { 𝑎 , 𝑏 } ⊆ 𝑒 ↔ { 𝑎 , 𝑏 } ⊆ { 𝑏 , 𝑎 } ) )
17 16 adantl ( ( { 𝑎 , 𝑏 } ∈ 𝐸𝑒 = { 𝑏 , 𝑎 } ) → ( { 𝑎 , 𝑏 } ⊆ 𝑒 ↔ { 𝑎 , 𝑏 } ⊆ { 𝑏 , 𝑎 } ) )
18 13 eqimssi { 𝑎 , 𝑏 } ⊆ { 𝑏 , 𝑎 }
19 18 a1i ( { 𝑎 , 𝑏 } ∈ 𝐸 → { 𝑎 , 𝑏 } ⊆ { 𝑏 , 𝑎 } )
20 15 17 19 rspcedvd ( { 𝑎 , 𝑏 } ∈ 𝐸 → ∃ 𝑒𝐸 { 𝑎 , 𝑏 } ⊆ 𝑒 )
21 20 adantl ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → ∃ 𝑒𝐸 { 𝑎 , 𝑏 } ⊆ 𝑒 )
22 1 2 nbgrel ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ↔ ( ( 𝑏𝑉𝑎𝑉 ) ∧ 𝑏𝑎 ∧ ∃ 𝑒𝐸 { 𝑎 , 𝑏 } ⊆ 𝑒 ) )
23 8 12 21 22 syl3anbrc ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) )
24 6 ad2antrr ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → ( 𝑎𝑉𝑏𝑉 ) )
25 simplrl ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → 𝑎𝑏 )
26 id ( { 𝑎 , 𝑏 } ∈ 𝐸 → { 𝑎 , 𝑏 } ∈ 𝐸 )
27 sseq2 ( 𝑒 = { 𝑎 , 𝑏 } → ( { 𝑏 , 𝑎 } ⊆ 𝑒 ↔ { 𝑏 , 𝑎 } ⊆ { 𝑎 , 𝑏 } ) )
28 27 adantl ( ( { 𝑎 , 𝑏 } ∈ 𝐸𝑒 = { 𝑎 , 𝑏 } ) → ( { 𝑏 , 𝑎 } ⊆ 𝑒 ↔ { 𝑏 , 𝑎 } ⊆ { 𝑎 , 𝑏 } ) )
29 prcom { 𝑏 , 𝑎 } = { 𝑎 , 𝑏 }
30 29 eqimssi { 𝑏 , 𝑎 } ⊆ { 𝑎 , 𝑏 }
31 30 a1i ( { 𝑎 , 𝑏 } ∈ 𝐸 → { 𝑏 , 𝑎 } ⊆ { 𝑎 , 𝑏 } )
32 26 28 31 rspcedvd ( { 𝑎 , 𝑏 } ∈ 𝐸 → ∃ 𝑒𝐸 { 𝑏 , 𝑎 } ⊆ 𝑒 )
33 32 adantl ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → ∃ 𝑒𝐸 { 𝑏 , 𝑎 } ⊆ 𝑒 )
34 1 2 nbgrel ( 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ↔ ( ( 𝑎𝑉𝑏𝑉 ) ∧ 𝑎𝑏 ∧ ∃ 𝑒𝐸 { 𝑏 , 𝑎 } ⊆ 𝑒 ) )
35 24 25 33 34 syl3anbrc ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) )
36 23 35 jca ( ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) ) ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) )
37 36 ex ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 → ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ) )
38 1 2 nbuhgr2vtx1edgblem ( ( 𝐺 ∈ UHGraph ∧ 𝑉 = { 𝑎 , 𝑏 } ∧ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) → { 𝑎 , 𝑏 } ∈ 𝐸 )
39 38 3exp ( 𝐺 ∈ UHGraph → ( 𝑉 = { 𝑎 , 𝑏 } → ( 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) ) )
40 39 adantr ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) → ( 𝑉 = { 𝑎 , 𝑏 } → ( 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) ) )
41 40 adantld ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) → ( ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) → ( 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) ) )
42 41 imp ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) ) → ( 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
43 42 adantld ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) ) → ( ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) → { 𝑎 , 𝑏 } ∈ 𝐸 ) )
44 37 43 impbid ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) ) → ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ) )
45 eleq1 ( 𝑉 = { 𝑎 , 𝑏 } → ( 𝑉𝐸 ↔ { 𝑎 , 𝑏 } ∈ 𝐸 ) )
46 45 adantl ( ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) → ( 𝑉𝐸 ↔ { 𝑎 , 𝑏 } ∈ 𝐸 ) )
47 id ( 𝑉 = { 𝑎 , 𝑏 } → 𝑉 = { 𝑎 , 𝑏 } )
48 difeq1 ( 𝑉 = { 𝑎 , 𝑏 } → ( 𝑉 ∖ { 𝑣 } ) = ( { 𝑎 , 𝑏 } ∖ { 𝑣 } ) )
49 48 raleqdv ( 𝑉 = { 𝑎 , 𝑏 } → ( ∀ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
50 47 49 raleqbidv ( 𝑉 = { 𝑎 , 𝑏 } → ( ∀ 𝑣𝑉𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ∀ 𝑣 ∈ { 𝑎 , 𝑏 } ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
51 vex 𝑎 ∈ V
52 vex 𝑏 ∈ V
53 sneq ( 𝑣 = 𝑎 → { 𝑣 } = { 𝑎 } )
54 53 difeq2d ( 𝑣 = 𝑎 → ( { 𝑎 , 𝑏 } ∖ { 𝑣 } ) = ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) )
55 oveq2 ( 𝑣 = 𝑎 → ( 𝐺 NeighbVtx 𝑣 ) = ( 𝐺 NeighbVtx 𝑎 ) )
56 55 eleq2d ( 𝑣 = 𝑎 → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
57 54 56 raleqbidv ( 𝑣 = 𝑎 → ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
58 sneq ( 𝑣 = 𝑏 → { 𝑣 } = { 𝑏 } )
59 58 difeq2d ( 𝑣 = 𝑏 → ( { 𝑎 , 𝑏 } ∖ { 𝑣 } ) = ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) )
60 oveq2 ( 𝑣 = 𝑏 → ( 𝐺 NeighbVtx 𝑣 ) = ( 𝐺 NeighbVtx 𝑏 ) )
61 60 eleq2d ( 𝑣 = 𝑏 → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) )
62 59 61 raleqbidv ( 𝑣 = 𝑏 → ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) )
63 51 52 57 62 ralpr ( ∀ 𝑣 ∈ { 𝑎 , 𝑏 } ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) )
64 difprsn1 ( 𝑎𝑏 → ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) = { 𝑏 } )
65 64 raleqdv ( 𝑎𝑏 → ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ↔ ∀ 𝑛 ∈ { 𝑏 } 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
66 eleq1 ( 𝑛 = 𝑏 → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ↔ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
67 52 66 ralsn ( ∀ 𝑛 ∈ { 𝑏 } 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ↔ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) )
68 65 67 bitrdi ( 𝑎𝑏 → ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ↔ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ) )
69 difprsn2 ( 𝑎𝑏 → ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) = { 𝑎 } )
70 69 raleqdv ( 𝑎𝑏 → ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ↔ ∀ 𝑛 ∈ { 𝑎 } 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) )
71 eleq1 ( 𝑛 = 𝑎 → ( 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ↔ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) )
72 51 71 ralsn ( ∀ 𝑛 ∈ { 𝑎 } 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ↔ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) )
73 70 72 bitrdi ( 𝑎𝑏 → ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ↔ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) )
74 68 73 anbi12d ( 𝑎𝑏 → ( ( ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑎 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑏 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ↔ ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ) )
75 63 74 syl5bb ( 𝑎𝑏 → ( ∀ 𝑣 ∈ { 𝑎 , 𝑏 } ∀ 𝑛 ∈ ( { 𝑎 , 𝑏 } ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ) )
76 50 75 sylan9bbr ( ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) → ( ∀ 𝑣𝑉𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ↔ ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ) )
77 46 76 bibi12d ( ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) → ( ( 𝑉𝐸 ↔ ∀ 𝑣𝑉𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) ↔ ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ) ) )
78 77 adantl ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) ) → ( ( 𝑉𝐸 ↔ ∀ 𝑣𝑉𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) ↔ ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ ( 𝑏 ∈ ( 𝐺 NeighbVtx 𝑎 ) ∧ 𝑎 ∈ ( 𝐺 NeighbVtx 𝑏 ) ) ) ) )
79 44 78 mpbird ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) ∧ ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) ) → ( 𝑉𝐸 ↔ ∀ 𝑣𝑉𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )
80 79 ex ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎𝑉𝑏𝑉 ) ) → ( ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) → ( 𝑉𝐸 ↔ ∀ 𝑣𝑉𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) ) )
81 80 rexlimdvva ( 𝐺 ∈ UHGraph → ( ∃ 𝑎𝑉𝑏𝑉 ( 𝑎𝑏𝑉 = { 𝑎 , 𝑏 } ) → ( 𝑉𝐸 ↔ ∀ 𝑣𝑉𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) ) )
82 5 81 syl5bi ( 𝐺 ∈ UHGraph → ( ( ♯ ‘ 𝑉 ) = 2 → ( 𝑉𝐸 ↔ ∀ 𝑣𝑉𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) ) )
83 82 imp ( ( 𝐺 ∈ UHGraph ∧ ( ♯ ‘ 𝑉 ) = 2 ) → ( 𝑉𝐸 ↔ ∀ 𝑣𝑉𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) 𝑛 ∈ ( 𝐺 NeighbVtx 𝑣 ) ) )