Metamath Proof Explorer

Theorem vdgn1frgrv2

Description: Any vertex in a friendship graph does not have degree 1, see remark 2 in MertziosUnger p. 153 (after Proposition 1): "... no node v of it [a friendship graph] may have deg(v) = 1.". (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 4-Apr-2021)

Ref Expression
Hypothesis vdn1frgrv2.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion vdgn1frgrv2 ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) → ( 1 < ( ♯ ‘ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 1 ) )

Proof

Step Hyp Ref Expression
1 vdn1frgrv2.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 frgrusgr ⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
3 2 anim1i ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) )
4 3 adantr ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) )
5 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
6 eqid ⊢ dom ( iEdg ‘ 𝐺 ) = dom ( iEdg ‘ 𝐺 )
7 eqid ⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
8 1 5 6 7 vtxdusgrval ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
9 4 8 syl ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) )
10 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
11 1 10 3cyclfrgrrn2 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) )
12 11 adantlr ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) )
13 preq1 ⊢ ( 𝑎 = 𝑁 → { 𝑎 , 𝑏 } = { 𝑁 , 𝑏 } )
14 13 eleq1d ⊢ ( 𝑎 = 𝑁 → ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) )
15 preq2 ⊢ ( 𝑎 = 𝑁 → { 𝑐 , 𝑎 } = { 𝑐 , 𝑁 } )
16 15 eleq1d ⊢ ( 𝑎 = 𝑁 → ( { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ↔ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) )
17 14 16 3anbi13d ⊢ ( 𝑎 = 𝑁 → ( ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ↔ ( { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) ) )
18 17 anbi2d ⊢ ( 𝑎 = 𝑁 → ( ( 𝑏 ≠ 𝑐 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ↔ ( 𝑏 ≠ 𝑐 ∧ ( { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
19 18 2rexbidv ⊢ ( 𝑎 = 𝑁 → ( ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ↔ ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) ) ) )
20 19 rspcva ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ∀ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) ) )
21 2 adantl ⊢ ( ( ( ( 𝑏 ≠ 𝑐 ∧ ( { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐺 ∈ FriendGraph ) → 𝐺 ∈ USGraph )
22 simplll ⊢ ( ( ( ( 𝑏 ≠ 𝑐 ∧ ( { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐺 ∈ FriendGraph ) → 𝑏 ≠ 𝑐 )
23 3simpb ⊢ ( ( { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) → ( { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) )
24 23 ad3antlr ⊢ ( ( ( ( 𝑏 ≠ 𝑐 ∧ ( { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐺 ∈ FriendGraph ) → ( { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) )
25 5 10 usgr2edg1 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑏 ≠ 𝑐 ) ∧ ( { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) ) → ¬ ∃! 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
26 21 22 24 25 syl21anc ⊢ ( ( ( ( 𝑏 ≠ 𝑐 ∧ ( { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐺 ∈ FriendGraph ) → ¬ ∃! 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
27 26 a1d ⊢ ( ( ( ( 𝑏 ≠ 𝑐 ∧ ( { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝑁 ∈ 𝑉 ) ∧ 𝐺 ∈ FriendGraph ) → ( 1 < ( ♯ ‘ 𝑉 ) → ¬ ∃! 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
28 27 ex ⊢ ( ( ( 𝑏 ≠ 𝑐 ∧ ( { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) ) ∧ 𝑁 ∈ 𝑉 ) → ( 𝐺 ∈ FriendGraph → ( 1 < ( ♯ ‘ 𝑉 ) → ¬ ∃! 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) )
29 28 ex ⊢ ( ( 𝑏 ≠ 𝑐 ∧ ( { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑁 ∈ 𝑉 → ( 𝐺 ∈ FriendGraph → ( 1 < ( ♯ ‘ 𝑉 ) → ¬ ∃! 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) )
30 29 a1i ⊢ ( ( 𝑏 ∈ 𝑉 ∧ 𝑐 ∈ 𝑉 ) → ( ( 𝑏 ≠ 𝑐 ∧ ( { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑁 ∈ 𝑉 → ( 𝐺 ∈ FriendGraph → ( 1 < ( ♯ ‘ 𝑉 ) → ¬ ∃! 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) ) )
31 30 rexlimivv ⊢ ( ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑁 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑁 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑁 ∈ 𝑉 → ( 𝐺 ∈ FriendGraph → ( 1 < ( ♯ ‘ 𝑉 ) → ¬ ∃! 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) )
32 20 31 syl ⊢ ( ( 𝑁 ∈ 𝑉 ∧ ∀ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) ) → ( 𝑁 ∈ 𝑉 → ( 𝐺 ∈ FriendGraph → ( 1 < ( ♯ ‘ 𝑉 ) → ¬ ∃! 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) )
33 32 ex ⊢ ( 𝑁 ∈ 𝑉 → ( ∀ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝑁 ∈ 𝑉 → ( 𝐺 ∈ FriendGraph → ( 1 < ( ♯ ‘ 𝑉 ) → ¬ ∃! 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) ) )
34 33 pm2.43a ⊢ ( 𝑁 ∈ 𝑉 → ( ∀ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) → ( 𝐺 ∈ FriendGraph → ( 1 < ( ♯ ‘ 𝑉 ) → ¬ ∃! 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) )
35 34 com24 ⊢ ( 𝑁 ∈ 𝑉 → ( 1 < ( ♯ ‘ 𝑉 ) → ( 𝐺 ∈ FriendGraph → ( ∀ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) → ¬ ∃! 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) )
36 35 com3r ⊢ ( 𝐺 ∈ FriendGraph → ( 𝑁 ∈ 𝑉 → ( 1 < ( ♯ ‘ 𝑉 ) → ( ∀ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) → ¬ ∃! 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) ) ) )
37 36 imp31 ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ∀ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑏 , 𝑐 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑐 , 𝑎 } ∈ ( Edg ‘ 𝐺 ) ) ) → ¬ ∃! 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
38 12 37 mpd ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ¬ ∃! 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) )
39 fvex ⊢ ( iEdg ‘ 𝐺 ) ∈ V
40 39 dmex ⊢ dom ( iEdg ‘ 𝐺 ) ∈ V
41 40 a1i ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → dom ( iEdg ‘ 𝐺 ) ∈ V )
42 rabexg ⊢ ( dom ( iEdg ‘ 𝐺 ) ∈ V → { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ∈ V )
43 hash1snb ⊢ ( { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ∈ V → ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 1 ↔ ∃ 𝑖 { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } = { 𝑖 } ) )
44 41 42 43 3syl ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 1 ↔ ∃ 𝑖 { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } = { 𝑖 } ) )
45 reusn ⊢ ( ∃! 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ↔ ∃ 𝑖 { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } = { 𝑖 } )
46 44 45 bitr4di ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) = 1 ↔ ∃! 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
47 46 necon3abid ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) ≠ 1 ↔ ¬ ∃! 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ) )
48 38 47 mpbird ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ♯ ‘ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ 𝑁 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) } ) ≠ 1 )
49 9 48 eqnetrd ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 1 )
50 49 ex ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑁 ∈ 𝑉 ) → ( 1 < ( ♯ ‘ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) ≠ 1 ) )