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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
frgrwopreg.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
frgrwopreg.a ⊢ 𝐴 = { 𝑥 ∈ 𝑉 ∣ ( 𝐷 ‘ 𝑥 ) = 𝐾 }
frgrwopreg.b ⊢ 𝐵 = ( 𝑉 ∖ 𝐴 )
Assertion frgrwopreg ( 𝐺 ∈ FriendGraph → ( ( ( ♯ ‘ 𝐴 ) = 1 ∨ 𝐴 = ∅ ) ∨ ( ( ♯ ‘ 𝐵 ) = 1 ∨ 𝐵 = ∅ ) ) )

Proof

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