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 ∈ V b ≠ c ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c a ∈ Edg ⁡ G
12 11 adantlr ⊢ G ∈ FriendGraph ∧ N ∈ V ∧ 1 < V → ∀ a ∈ V ∃ b ∈ V ∃ c ∈ V b ≠ c ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c a ∈ Edg ⁡ G
13 preq1 ⊢ a = N → a b = N b
14 13 eleq1d ⊢ a = N → a b ∈ Edg ⁡ G ↔ N b ∈ Edg ⁡ G
15 preq2 ⊢ a = N → c a = c N
16 15 eleq1d ⊢ a = N → c a ∈ Edg ⁡ G ↔ c N ∈ Edg ⁡ G
17 14 16 3anbi13d ⊢ a = N → a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c a ∈ Edg ⁡ G ↔ N b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c N ∈ Edg ⁡ G
18 17 anbi2d ⊢ a = N → b ≠ c ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c a ∈ Edg ⁡ G ↔ b ≠ c ∧ N b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c N ∈ Edg ⁡ G
19 18 2rexbidv ⊢ a = N → ∃ b ∈ V ∃ c ∈ V b ≠ c ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c a ∈ Edg ⁡ G ↔ ∃ b ∈ V ∃ c ∈ V b ≠ c ∧ N b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c N ∈ Edg ⁡ G
20 19 rspcva ⊢ N ∈ V ∧ ∀ a ∈ V ∃ b ∈ V ∃ c ∈ V b ≠ c ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c a ∈ Edg ⁡ G → ∃ b ∈ V ∃ c ∈ V b ≠ c ∧ N b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c N ∈ Edg ⁡ G
21 2 adantl ⊢ b ≠ c ∧ N b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c N ∈ Edg ⁡ G ∧ N ∈ V ∧ G ∈ FriendGraph → G ∈ USGraph
22 simplll ⊢ b ≠ c ∧ N b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c N ∈ Edg ⁡ G ∧ N ∈ V ∧ G ∈ FriendGraph → b ≠ c
23 3simpb ⊢ N b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c N ∈ Edg ⁡ G → N b ∈ Edg ⁡ G ∧ c N ∈ Edg ⁡ G
24 23 ad3antlr ⊢ b ≠ c ∧ N b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c N ∈ Edg ⁡ G ∧ N ∈ V ∧ G ∈ FriendGraph → N b ∈ Edg ⁡ G ∧ c N ∈ Edg ⁡ G
25 5 10 usgr2edg1 ⊢ G ∈ USGraph ∧ b ≠ c ∧ N b ∈ Edg ⁡ G ∧ c N ∈ Edg ⁡ G → ¬ ∃! x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x
26 21 22 24 25 syl21anc ⊢ b ≠ c ∧ N b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c N ∈ Edg ⁡ G ∧ N ∈ V ∧ G ∈ FriendGraph → ¬ ∃! x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x
27 26 a1d ⊢ b ≠ c ∧ N b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c N ∈ Edg ⁡ G ∧ N ∈ V ∧ G ∈ FriendGraph → 1 < V → ¬ ∃! x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x
28 27 ex ⊢ b ≠ c ∧ N b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c N ∈ Edg ⁡ G ∧ N ∈ V → G ∈ FriendGraph → 1 < V → ¬ ∃! x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x
29 28 ex ⊢ b ≠ c ∧ N b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c N ∈ Edg ⁡ G → N ∈ V → G ∈ FriendGraph → 1 < V → ¬ ∃! x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x
30 29 a1i ⊢ b ∈ V ∧ c ∈ V → b ≠ c ∧ N b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c N ∈ Edg ⁡ G → N ∈ V → G ∈ FriendGraph → 1 < V → ¬ ∃! x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x
31 30 rexlimivv ⊢ ∃ b ∈ V ∃ c ∈ V b ≠ c ∧ N b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c N ∈ Edg ⁡ G → N ∈ V → G ∈ FriendGraph → 1 < V → ¬ ∃! x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x
32 20 31 syl ⊢ N ∈ V ∧ ∀ a ∈ V ∃ b ∈ V ∃ c ∈ V b ≠ c ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c a ∈ Edg ⁡ G → N ∈ V → G ∈ FriendGraph → 1 < V → ¬ ∃! x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x
33 32 ex ⊢ N ∈ V → ∀ a ∈ V ∃ b ∈ V ∃ c ∈ V b ≠ c ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c a ∈ Edg ⁡ G → N ∈ V → G ∈ FriendGraph → 1 < V → ¬ ∃! x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x
34 33 pm2.43a ⊢ N ∈ V → ∀ a ∈ V ∃ b ∈ V ∃ c ∈ V b ≠ c ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c a ∈ Edg ⁡ G → G ∈ FriendGraph → 1 < V → ¬ ∃! x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x
35 34 com24 ⊢ N ∈ V → 1 < V → G ∈ FriendGraph → ∀ a ∈ V ∃ b ∈ V ∃ c ∈ V b ≠ c ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c a ∈ Edg ⁡ G → ¬ ∃! x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x
36 35 com3r ⊢ G ∈ FriendGraph → N ∈ V → 1 < V → ∀ a ∈ V ∃ b ∈ V ∃ c ∈ V b ≠ c ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c a ∈ Edg ⁡ G → ¬ ∃! x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x
37 36 imp31 ⊢ G ∈ FriendGraph ∧ N ∈ V ∧ 1 < V → ∀ a ∈ V ∃ b ∈ V ∃ c ∈ V b ≠ c ∧ a b ∈ Edg ⁡ G ∧ b c ∈ Edg ⁡ G ∧ c a ∈ Edg ⁡ G → ¬ ∃! x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x
38 12 37 mpd ⊢ G ∈ FriendGraph ∧ N ∈ V ∧ 1 < V → ¬ ∃! x ∈ dom ⁡ iEdg ⁡ G N ∈ 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 ↔ ∃ i x ∈ 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 ↔ ∃ i x ∈ dom ⁡ iEdg ⁡ G | N ∈ iEdg ⁡ G ⁡ x = i
45 reusn ⊢ ∃! x ∈ dom ⁡ iEdg ⁡ G N ∈ iEdg ⁡ G ⁡ x ↔ ∃ i x ∈ 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 ⁡ G N ∈ iEdg ⁡ G ⁡ x
47 46 necon3abid ⊢ G ∈ FriendGraph ∧ N ∈ V ∧ 1 < V → x ∈ dom ⁡ iEdg ⁡ G | N ∈ iEdg ⁡ G ⁡ x ≠ 1 ↔ ¬ ∃! x ∈ dom ⁡ iEdg ⁡ G N ∈ 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