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