Metamath Proof Explorer

Theorem frgrwopreg

Description: In a friendship graph there are either no vertices ( A = (/) ) or exactly one vertex ( ( #A ) = 1 ) having degree K , or all ( B = (/) ) or all except one vertices ( ( #B ) = 1 ) have degree K . (Contributed by Alexander van der Vekens, 31-Dec-2017) (Revised by AV, 10-May-2021) (Proof shortened by AV, 3-Jan-2022)

Ref Expression
Hypotheses frgrwopreg.v ⊢ V = Vtx ⁡ G
frgrwopreg.d ⊢ D = VtxDeg ⁡ G
frgrwopreg.a ⊢ A = x ∈ V | D ⁡ x = K
frgrwopreg.b ⊢ B = V ∖ A
Assertion frgrwopreg ⊢ G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅

Proof

Step Hyp Ref Expression
1 frgrwopreg.v ⊢ V = Vtx ⁡ G
2 frgrwopreg.d ⊢ D = VtxDeg ⁡ G
3 frgrwopreg.a ⊢ A = x ∈ V | D ⁡ x = K
4 frgrwopreg.b ⊢ B = V ∖ A
5 1 2 3 4 frgrwopreglem1 ⊢ A ∈ V ∧ B ∈ V
6 hashv01gt1 ⊢ A ∈ V → A = 0 ∨ A = 1 ∨ 1 < A
7 hasheq0 ⊢ A ∈ V → A = 0 ↔ A = ∅
8 biidd ⊢ A ∈ V → A = 1 ↔ A = 1
9 biidd ⊢ A ∈ V → 1 < A ↔ 1 < A
10 7 8 9 3orbi123d ⊢ A ∈ V → A = 0 ∨ A = 1 ∨ 1 < A ↔ A = ∅ ∨ A = 1 ∨ 1 < A
11 hashv01gt1 ⊢ B ∈ V → B = 0 ∨ B = 1 ∨ 1 < B
12 hasheq0 ⊢ B ∈ V → B = 0 ↔ B = ∅
13 biidd ⊢ B ∈ V → B = 1 ↔ B = 1
14 biidd ⊢ B ∈ V → 1 < B ↔ 1 < B
15 12 13 14 3orbi123d ⊢ B ∈ V → B = 0 ∨ B = 1 ∨ 1 < B ↔ B = ∅ ∨ B = 1 ∨ 1 < B
16 olc ⊢ B = ∅ → B = 1 ∨ B = ∅
17 16 olcd ⊢ B = ∅ → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
18 17 2a1d ⊢ B = ∅ → A = ∅ ∨ A = 1 ∨ 1 < A → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
19 orc ⊢ B = 1 → B = 1 ∨ B = ∅
20 19 olcd ⊢ B = 1 → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
21 20 2a1d ⊢ B = 1 → A = ∅ ∨ A = 1 ∨ 1 < A → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
22 olc ⊢ A = ∅ → A = 1 ∨ A = ∅
23 22 orcd ⊢ A = ∅ → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
24 23 2a1d ⊢ A = ∅ → 1 < B → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
25 orc ⊢ A = 1 → A = 1 ∨ A = ∅
26 25 orcd ⊢ A = 1 → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
27 26 2a1d ⊢ A = 1 → 1 < B → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
28 eqid ⊢ Edg ⁡ G = Edg ⁡ G
29 1 2 3 4 28 frgrwopreglem5 ⊢ G ∈ FriendGraph ∧ 1 < A ∧ 1 < B → ∃ a ∈ A ∃ x ∈ A ∃ b ∈ B ∃ y ∈ B a ≠ x ∧ b ≠ y ∧ a b ∈ Edg ⁡ G ∧ b x ∈ Edg ⁡ G ∧ x y ∈ Edg ⁡ G ∧ y a ∈ Edg ⁡ G
30 frgrusgr ⊢ G ∈ FriendGraph → G ∈ USGraph
31 simplll ⊢ G ∈ USGraph ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B ∧ a ≠ x ∧ b ≠ y → G ∈ USGraph
32 elrabi ⊢ a ∈ x ∈ V | D ⁡ x = K → a ∈ V
33 32 3 eleq2s ⊢ a ∈ A → a ∈ V
34 33 adantr ⊢ a ∈ A ∧ x ∈ A → a ∈ V
35 34 ad3antlr ⊢ G ∈ USGraph ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B ∧ a ≠ x ∧ b ≠ y → a ∈ V
36 rabidim1 ⊢ x ∈ x ∈ V | D ⁡ x = K → x ∈ V
37 36 3 eleq2s ⊢ x ∈ A → x ∈ V
38 37 adantl ⊢ a ∈ A ∧ x ∈ A → x ∈ V
39 38 ad3antlr ⊢ G ∈ USGraph ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B ∧ a ≠ x ∧ b ≠ y → x ∈ V
40 simprl ⊢ G ∈ USGraph ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B ∧ a ≠ x ∧ b ≠ y → a ≠ x
41 eldifi ⊢ b ∈ V ∖ A → b ∈ V
42 41 4 eleq2s ⊢ b ∈ B → b ∈ V
43 42 adantr ⊢ b ∈ B ∧ y ∈ B → b ∈ V
44 43 ad2antlr ⊢ G ∈ USGraph ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B ∧ a ≠ x ∧ b ≠ y → b ∈ V
45 eldifi ⊢ y ∈ V ∖ A → y ∈ V
46 45 4 eleq2s ⊢ y ∈ B → y ∈ V
47 46 adantl ⊢ b ∈ B ∧ y ∈ B → y ∈ V
48 47 ad2antlr ⊢ G ∈ USGraph ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B ∧ a ≠ x ∧ b ≠ y → y ∈ V
49 simprr ⊢ G ∈ USGraph ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B ∧ a ≠ x ∧ b ≠ y → b ≠ y
50 1 28 4cyclusnfrgr ⊢ G ∈ USGraph ∧ a ∈ V ∧ x ∈ V ∧ a ≠ x ∧ b ∈ V ∧ y ∈ V ∧ b ≠ y → a b ∈ Edg ⁡ G ∧ b x ∈ Edg ⁡ G ∧ x y ∈ Edg ⁡ G ∧ y a ∈ Edg ⁡ G → G ∉ FriendGraph
51 31 35 39 40 44 48 49 50 syl133anc ⊢ G ∈ USGraph ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B ∧ a ≠ x ∧ b ≠ y → a b ∈ Edg ⁡ G ∧ b x ∈ Edg ⁡ G ∧ x y ∈ Edg ⁡ G ∧ y a ∈ Edg ⁡ G → G ∉ FriendGraph
52 51 exp4b ⊢ G ∈ USGraph ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → a ≠ x ∧ b ≠ y → a b ∈ Edg ⁡ G ∧ b x ∈ Edg ⁡ G → x y ∈ Edg ⁡ G ∧ y a ∈ Edg ⁡ G → G ∉ FriendGraph
53 52 3impd ⊢ G ∈ USGraph ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → a ≠ x ∧ b ≠ y ∧ a b ∈ Edg ⁡ G ∧ b x ∈ Edg ⁡ G ∧ x y ∈ Edg ⁡ G ∧ y a ∈ Edg ⁡ G → G ∉ FriendGraph
54 df-nel ⊢ G ∉ FriendGraph ↔ ¬ G ∈ FriendGraph
55 pm2.21 ⊢ ¬ G ∈ FriendGraph → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
56 54 55 sylbi ⊢ G ∉ FriendGraph → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
57 53 56 syl6 ⊢ G ∈ USGraph ∧ a ∈ A ∧ x ∈ A ∧ b ∈ B ∧ y ∈ B → a ≠ x ∧ b ≠ y ∧ a b ∈ Edg ⁡ G ∧ b x ∈ Edg ⁡ G ∧ x y ∈ Edg ⁡ G ∧ y a ∈ Edg ⁡ G → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
58 57 rexlimdvva ⊢ G ∈ USGraph ∧ a ∈ A ∧ x ∈ A → ∃ b ∈ B ∃ y ∈ B a ≠ x ∧ b ≠ y ∧ a b ∈ Edg ⁡ G ∧ b x ∈ Edg ⁡ G ∧ x y ∈ Edg ⁡ G ∧ y a ∈ Edg ⁡ G → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
59 58 rexlimdvva ⊢ G ∈ USGraph → ∃ a ∈ A ∃ x ∈ A ∃ b ∈ B ∃ y ∈ B a ≠ x ∧ b ≠ y ∧ a b ∈ Edg ⁡ G ∧ b x ∈ Edg ⁡ G ∧ x y ∈ Edg ⁡ G ∧ y a ∈ Edg ⁡ G → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
60 59 com23 ⊢ G ∈ USGraph → G ∈ FriendGraph → ∃ a ∈ A ∃ x ∈ A ∃ b ∈ B ∃ y ∈ B a ≠ x ∧ b ≠ y ∧ a b ∈ Edg ⁡ G ∧ b x ∈ Edg ⁡ G ∧ x y ∈ Edg ⁡ G ∧ y a ∈ Edg ⁡ G → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
61 30 60 mpcom ⊢ G ∈ FriendGraph → ∃ a ∈ A ∃ x ∈ A ∃ b ∈ B ∃ y ∈ B a ≠ x ∧ b ≠ y ∧ a b ∈ Edg ⁡ G ∧ b x ∈ Edg ⁡ G ∧ x y ∈ Edg ⁡ G ∧ y a ∈ Edg ⁡ G → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
62 61 3ad2ant1 ⊢ G ∈ FriendGraph ∧ 1 < A ∧ 1 < B → ∃ a ∈ A ∃ x ∈ A ∃ b ∈ B ∃ y ∈ B a ≠ x ∧ b ≠ y ∧ a b ∈ Edg ⁡ G ∧ b x ∈ Edg ⁡ G ∧ x y ∈ Edg ⁡ G ∧ y a ∈ Edg ⁡ G → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
63 29 62 mpd ⊢ G ∈ FriendGraph ∧ 1 < A ∧ 1 < B → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
64 63 3exp ⊢ G ∈ FriendGraph → 1 < A → 1 < B → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
65 64 com3l ⊢ 1 < A → 1 < B → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
66 24 27 65 3jaoi ⊢ A = ∅ ∨ A = 1 ∨ 1 < A → 1 < B → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
67 66 com12 ⊢ 1 < B → A = ∅ ∨ A = 1 ∨ 1 < A → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
68 18 21 67 3jaoi ⊢ B = ∅ ∨ B = 1 ∨ 1 < B → A = ∅ ∨ A = 1 ∨ 1 < A → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
69 15 68 biimtrdi ⊢ B ∈ V → B = 0 ∨ B = 1 ∨ 1 < B → A = ∅ ∨ A = 1 ∨ 1 < A → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
70 11 69 mpd ⊢ B ∈ V → A = ∅ ∨ A = 1 ∨ 1 < A → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
71 70 com12 ⊢ A = ∅ ∨ A = 1 ∨ 1 < A → B ∈ V → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
72 10 71 biimtrdi ⊢ A ∈ V → A = 0 ∨ A = 1 ∨ 1 < A → B ∈ V → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
73 6 72 mpd ⊢ A ∈ V → B ∈ V → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
74 73 imp ⊢ A ∈ V ∧ B ∈ V → G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅
75 5 74 ax-mp ⊢ G ∈ FriendGraph → A = 1 ∨ A = ∅ ∨ B = 1 ∨ B = ∅