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 → A B ∈ E ∧ B C ∈ E ∧ C D ∈ E ∧ D A ∈ 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 ∧ A B ∈ E ∧ B C ∈ E ∧ C D ∈ E ∧ D A ∈ E → A B ∈ E ∧ B C ∈ E
4 simprr ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ B ∈ V ∧ D ∈ V ∧ B ≠ D ∧ A B ∈ E ∧ B C ∈ E ∧ C D ∈ E ∧ D A ∈ E → C D ∈ E ∧ D A ∈ E
5 simpl3 ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ B ∈ V ∧ D ∈ V ∧ B ≠ D ∧ A B ∈ E ∧ B C ∈ E ∧ C D ∈ E ∧ D A ∈ E → B ∈ V ∧ D ∈ V ∧ B ≠ D
6 4cycl2vnunb ⊢ A B ∈ E ∧ B C ∈ E ∧ C D ∈ E ∧ D A ∈ E ∧ B ∈ V ∧ D ∈ V ∧ B ≠ D → ¬ ∃! x ∈ V A x x C ⊆ E
7 3 4 5 6 syl3anc ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ B ∈ V ∧ D ∈ V ∧ B ≠ D ∧ A B ∈ E ∧ B C ∈ E ∧ C D ∈ E ∧ D A ∈ E → ¬ ∃! x ∈ V A x x C ⊆ E
8 1 2 frcond1 ⊢ G ∈ FriendGraph → A ∈ V ∧ C ∈ V ∧ A ≠ C → ∃! x ∈ V A x x C ⊆ E
9 pm2.24 ⊢ ∃! x ∈ V A x x C ⊆ E → ¬ ∃! x ∈ V A x x C ⊆ E → ¬ G ∈ FriendGraph
10 8 9 syl6com ⊢ A ∈ V ∧ C ∈ V ∧ A ≠ C → G ∈ FriendGraph → ¬ ∃! x ∈ V A x x C ⊆ E → ¬ G ∈ FriendGraph
11 10 3ad2ant2 ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ B ∈ V ∧ D ∈ V ∧ B ≠ D → G ∈ FriendGraph → ¬ ∃! x ∈ V A x x C ⊆ E → ¬ G ∈ FriendGraph
12 11 com23 ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ B ∈ V ∧ D ∈ V ∧ B ≠ D → ¬ ∃! x ∈ V A x x C ⊆ E → G ∈ FriendGraph → ¬ G ∈ FriendGraph
13 12 adantr ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ B ∈ V ∧ D ∈ V ∧ B ≠ D ∧ A B ∈ E ∧ B C ∈ E ∧ C D ∈ E ∧ D A ∈ E → ¬ ∃! x ∈ V A x x C ⊆ E → G ∈ FriendGraph → ¬ G ∈ FriendGraph
14 7 13 mpd ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ B ∈ V ∧ D ∈ V ∧ B ≠ D ∧ A B ∈ E ∧ B C ∈ E ∧ C D ∈ E ∧ D A ∈ E → G ∈ FriendGraph → ¬ G ∈ FriendGraph
15 14 pm2.01d ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ B ∈ V ∧ D ∈ V ∧ B ≠ D ∧ A B ∈ E ∧ B C ∈ E ∧ C D ∈ E ∧ D A ∈ 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 ∧ A B ∈ E ∧ B C ∈ E ∧ C D ∈ E ∧ D A ∈ E → G ∉ FriendGraph
18 17 ex ⊢ G ∈ USGraph ∧ A ∈ V ∧ C ∈ V ∧ A ≠ C ∧ B ∈ V ∧ D ∈ V ∧ B ≠ D → A B ∈ E ∧ B C ∈ E ∧ C D ∈ E ∧ D A ∈ E → G ∉ FriendGraph