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 ⊢V=Vtx⁡G
Assertion vdgn1frgrv2 ⊢G∈FriendGraph∧N∈V→1<V→VtxDeg⁡G⁡N≠1

Proof

Step Hyp Ref Expression
1 vdn1frgrv2.v ⊢V=Vtx⁡G
2 frgrusgr ⊢G∈FriendGraph→G∈USGraph
3 2 anim1i ⊢G∈FriendGraph∧N∈V→G∈USGraph∧N∈V
4 3 adantr ⊢G∈FriendGraph∧N∈V∧1<V→G∈USGraph∧N∈V
5 eqid ⊢iEdg⁡G=iEdg⁡G
6 eqid ⊢dom⁡iEdg⁡G=dom⁡iEdg⁡G
7 eqid ⊢VtxDeg⁡G=VtxDeg⁡G
8 1 5 6 7 vtxdusgrval ⊢G∈USGraph∧N∈V→VtxDeg⁡G⁡N=x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x
9 4 8 syl ⊢G∈FriendGraph∧N∈V∧1<V→VtxDeg⁡G⁡N=x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x
10 eqid ⊢Edg⁡G=Edg⁡G
11 1 10 3cyclfrgrrn2 ⊢G∈FriendGraph∧1<V→∀a∈V∃b∈V∃c∈Vb≠c∧ab∈Edg⁡G∧bc∈Edg⁡G∧ca∈Edg⁡G
12 11 adantlr ⊢G∈FriendGraph∧N∈V∧1<V→∀a∈V∃b∈V∃c∈Vb≠c∧ab∈Edg⁡G∧bc∈Edg⁡G∧ca∈Edg⁡G
13 preq1 ⊢a=N→ab=Nb
14 13 eleq1d ⊢a=N→ab∈Edg⁡G↔Nb∈Edg⁡G
15 preq2 ⊢a=N→ca=cN
16 15 eleq1d ⊢a=N→ca∈Edg⁡G↔cN∈Edg⁡G
17 14 16 3anbi13d ⊢a=N→ab∈Edg⁡G∧bc∈Edg⁡G∧ca∈Edg⁡G↔Nb∈Edg⁡G∧bc∈Edg⁡G∧cN∈Edg⁡G
18 17 anbi2d ⊢a=N→b≠c∧ab∈Edg⁡G∧bc∈Edg⁡G∧ca∈Edg⁡G↔b≠c∧Nb∈Edg⁡G∧bc∈Edg⁡G∧cN∈Edg⁡G
19 18 2rexbidv ⊢a=N→∃b∈V∃c∈Vb≠c∧ab∈Edg⁡G∧bc∈Edg⁡G∧ca∈Edg⁡G↔∃b∈V∃c∈Vb≠c∧Nb∈Edg⁡G∧bc∈Edg⁡G∧cN∈Edg⁡G
20 19 rspcva ⊢N∈V∧∀a∈V∃b∈V∃c∈Vb≠c∧ab∈Edg⁡G∧bc∈Edg⁡G∧ca∈Edg⁡G→∃b∈V∃c∈Vb≠c∧Nb∈Edg⁡G∧bc∈Edg⁡G∧cN∈Edg⁡G
21 2 adantl ⊢b≠c∧Nb∈Edg⁡G∧bc∈Edg⁡G∧cN∈Edg⁡G∧N∈V∧G∈FriendGraph→G∈USGraph
22 simplll ⊢b≠c∧Nb∈Edg⁡G∧bc∈Edg⁡G∧cN∈Edg⁡G∧N∈V∧G∈FriendGraph→b≠c
23 3simpb ⊢Nb∈Edg⁡G∧bc∈Edg⁡G∧cN∈Edg⁡G→Nb∈Edg⁡G∧cN∈Edg⁡G
24 23 ad3antlr ⊢b≠c∧Nb∈Edg⁡G∧bc∈Edg⁡G∧cN∈Edg⁡G∧N∈V∧G∈FriendGraph→Nb∈Edg⁡G∧cN∈Edg⁡G
25 5 10 usgr2edg1 ⊢G∈USGraph∧b≠c∧Nb∈Edg⁡G∧cN∈Edg⁡G→¬∃!x∈dom⁡iEdg⁡GN∈iEdg⁡G⁡x
26 21 22 24 25 syl21anc ⊢b≠c∧Nb∈Edg⁡G∧bc∈Edg⁡G∧cN∈Edg⁡G∧N∈V∧G∈FriendGraph→¬∃!x∈dom⁡iEdg⁡GN∈iEdg⁡G⁡x
27 26 a1d ⊢b≠c∧Nb∈Edg⁡G∧bc∈Edg⁡G∧cN∈Edg⁡G∧N∈V∧G∈FriendGraph→1<V→¬∃!x∈dom⁡iEdg⁡GN∈iEdg⁡G⁡x
28 27 ex ⊢b≠c∧Nb∈Edg⁡G∧bc∈Edg⁡G∧cN∈Edg⁡G∧N∈V→G∈FriendGraph→1<V→¬∃!x∈dom⁡iEdg⁡GN∈iEdg⁡G⁡x
29 28 ex ⊢b≠c∧Nb∈Edg⁡G∧bc∈Edg⁡G∧cN∈Edg⁡G→N∈V→G∈FriendGraph→1<V→¬∃!x∈dom⁡iEdg⁡GN∈iEdg⁡G⁡x
30 29 a1i ⊢b∈V∧c∈V→b≠c∧Nb∈Edg⁡G∧bc∈Edg⁡G∧cN∈Edg⁡G→N∈V→G∈FriendGraph→1<V→¬∃!x∈dom⁡iEdg⁡GN∈iEdg⁡G⁡x
31 30 rexlimivv ⊢∃b∈V∃c∈Vb≠c∧Nb∈Edg⁡G∧bc∈Edg⁡G∧cN∈Edg⁡G→N∈V→G∈FriendGraph→1<V→¬∃!x∈dom⁡iEdg⁡GN∈iEdg⁡G⁡x
32 20 31 syl ⊢N∈V∧∀a∈V∃b∈V∃c∈Vb≠c∧ab∈Edg⁡G∧bc∈Edg⁡G∧ca∈Edg⁡G→N∈V→G∈FriendGraph→1<V→¬∃!x∈dom⁡iEdg⁡GN∈iEdg⁡G⁡x
33 32 ex ⊢N∈V→∀a∈V∃b∈V∃c∈Vb≠c∧ab∈Edg⁡G∧bc∈Edg⁡G∧ca∈Edg⁡G→N∈V→G∈FriendGraph→1<V→¬∃!x∈dom⁡iEdg⁡GN∈iEdg⁡G⁡x
34 33 pm2.43a ⊢N∈V→∀a∈V∃b∈V∃c∈Vb≠c∧ab∈Edg⁡G∧bc∈Edg⁡G∧ca∈Edg⁡G→G∈FriendGraph→1<V→¬∃!x∈dom⁡iEdg⁡GN∈iEdg⁡G⁡x
35 34 com24 ⊢N∈V→1<V→G∈FriendGraph→∀a∈V∃b∈V∃c∈Vb≠c∧ab∈Edg⁡G∧bc∈Edg⁡G∧ca∈Edg⁡G→¬∃!x∈dom⁡iEdg⁡GN∈iEdg⁡G⁡x
36 35 com3r ⊢G∈FriendGraph→N∈V→1<V→∀a∈V∃b∈V∃c∈Vb≠c∧ab∈Edg⁡G∧bc∈Edg⁡G∧ca∈Edg⁡G→¬∃!x∈dom⁡iEdg⁡GN∈iEdg⁡G⁡x
37 36 imp31 ⊢G∈FriendGraph∧N∈V∧1<V→∀a∈V∃b∈V∃c∈Vb≠c∧ab∈Edg⁡G∧bc∈Edg⁡G∧ca∈Edg⁡G→¬∃!x∈dom⁡iEdg⁡GN∈iEdg⁡G⁡x
38 12 37 mpd ⊢G∈FriendGraph∧N∈V∧1<V→¬∃!x∈dom⁡iEdg⁡GN∈iEdg⁡G⁡x
39 fvex ⊢iEdg⁡G∈V
40 39 dmex ⊢dom⁡iEdg⁡G∈V
41 40 a1i ⊢G∈FriendGraph∧N∈V∧1<V→dom⁡iEdg⁡G∈V
42 rabexg ⊢dom⁡iEdg⁡G∈V→x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x∈V
43 hash1snb ⊢x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x∈V→x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x=1↔∃ix∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x=i
44 41 42 43 3syl ⊢G∈FriendGraph∧N∈V∧1<V→x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x=1↔∃ix∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x=i
45 reusn ⊢∃!x∈dom⁡iEdg⁡GN∈iEdg⁡G⁡x↔∃ix∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x=i
46 44 45 bitr4di ⊢G∈FriendGraph∧N∈V∧1<V→x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x=1↔∃!x∈dom⁡iEdg⁡GN∈iEdg⁡G⁡x
47 46 necon3abid ⊢G∈FriendGraph∧N∈V∧1<V→x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x≠1↔¬∃!x∈dom⁡iEdg⁡GN∈iEdg⁡G⁡x
48 38 47 mpbird ⊢G∈FriendGraph∧N∈V∧1<V→x∈dom⁡iEdg⁡G|N∈iEdg⁡G⁡x≠1
49 9 48 eqnetrd ⊢G∈FriendGraph∧N∈V∧1<V→VtxDeg⁡G⁡N≠1
50 49 ex ⊢G∈FriendGraph∧N∈V→1<V→VtxDeg⁡G⁡N≠1