Metamath Proof Explorer

Theorem 4cyclusnfrgr

Description: A graph with a 4-cycle is not a friendhip graph. (Contributed by Alexander van der Vekens, 19-Dec-2017) (Revised by AV, 2-Apr-2021)

Ref Expression
Hypotheses 4cyclusnfrgr.v ⊢V=Vtx⁡G
4cyclusnfrgr.e ⊢E=Edg⁡G
Assertion 4cyclusnfrgr ⊢G∈USGraph∧A∈V∧C∈V∧A≠C∧B∈V∧D∈V∧B≠D→AB∈E∧BC∈E∧CD∈E∧DA∈E→G∉FriendGraph

Proof

Step Hyp Ref Expression
1 4cyclusnfrgr.v ⊢V=Vtx⁡G
2 4cyclusnfrgr.e ⊢E=Edg⁡G
3 simprl ⊢G∈USGraph∧A∈V∧C∈V∧A≠C∧B∈V∧D∈V∧B≠D∧AB∈E∧BC∈E∧CD∈E∧DA∈E→AB∈E∧BC∈E
4 simprr ⊢G∈USGraph∧A∈V∧C∈V∧A≠C∧B∈V∧D∈V∧B≠D∧AB∈E∧BC∈E∧CD∈E∧DA∈E→CD∈E∧DA∈E
5 simpl3 ⊢G∈USGraph∧A∈V∧C∈V∧A≠C∧B∈V∧D∈V∧B≠D∧AB∈E∧BC∈E∧CD∈E∧DA∈E→B∈V∧D∈V∧B≠D
6 4cycl2vnunb ⊢AB∈E∧BC∈E∧CD∈E∧DA∈E∧B∈V∧D∈V∧B≠D→¬∃!x∈VAxxC⊆E
7 3 4 5 6 syl3anc ⊢G∈USGraph∧A∈V∧C∈V∧A≠C∧B∈V∧D∈V∧B≠D∧AB∈E∧BC∈E∧CD∈E∧DA∈E→¬∃!x∈VAxxC⊆E
8 1 2 frcond1 ⊢G∈FriendGraph→A∈V∧C∈V∧A≠C→∃!x∈VAxxC⊆E
9 pm2.24 ⊢∃!x∈VAxxC⊆E→¬∃!x∈VAxxC⊆E→¬G∈FriendGraph
10 8 9 syl6com ⊢A∈V∧C∈V∧A≠C→G∈FriendGraph→¬∃!x∈VAxxC⊆E→¬G∈FriendGraph
11 10 3ad2ant2 ⊢G∈USGraph∧A∈V∧C∈V∧A≠C∧B∈V∧D∈V∧B≠D→G∈FriendGraph→¬∃!x∈VAxxC⊆E→¬G∈FriendGraph
12 11 com23 ⊢G∈USGraph∧A∈V∧C∈V∧A≠C∧B∈V∧D∈V∧B≠D→¬∃!x∈VAxxC⊆E→G∈FriendGraph→¬G∈FriendGraph
13 12 adantr ⊢G∈USGraph∧A∈V∧C∈V∧A≠C∧B∈V∧D∈V∧B≠D∧AB∈E∧BC∈E∧CD∈E∧DA∈E→¬∃!x∈VAxxC⊆E→G∈FriendGraph→¬G∈FriendGraph
14 7 13 mpd ⊢G∈USGraph∧A∈V∧C∈V∧A≠C∧B∈V∧D∈V∧B≠D∧AB∈E∧BC∈E∧CD∈E∧DA∈E→G∈FriendGraph→¬G∈FriendGraph
15 14 pm2.01d ⊢G∈USGraph∧A∈V∧C∈V∧A≠C∧B∈V∧D∈V∧B≠D∧AB∈E∧BC∈E∧CD∈E∧DA∈E→¬G∈FriendGraph
16 df-nel ⊢G∉FriendGraph↔¬G∈FriendGraph
17 15 16 sylibr ⊢G∈USGraph∧A∈V∧C∈V∧A≠C∧B∈V∧D∈V∧B≠D∧AB∈E∧BC∈E∧CD∈E∧DA∈E→G∉FriendGraph
18 17 ex ⊢G∈USGraph∧A∈V∧C∈V∧A≠C∧B∈V∧D∈V∧B≠D→AB∈E∧BC∈E∧CD∈E∧DA∈E→G∉FriendGraph