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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	4cyclusnfrgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	4cyclusnfrgr	⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) ) → ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐷 } ∈ 𝐸 ∧ { 𝐷 , 𝐴 } ∈ 𝐸 ) ) → 𝐺 ∉ FriendGraph ) )

Proof

Step	Hyp	Ref	Expression
1		4cyclusnfrgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		4cyclusnfrgr.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		simprl	⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) ) ∧ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐷 } ∈ 𝐸 ∧ { 𝐷 , 𝐴 } ∈ 𝐸 ) ) ) → ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) )
4		simprr	⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) ) ∧ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐷 } ∈ 𝐸 ∧ { 𝐷 , 𝐴 } ∈ 𝐸 ) ) ) → ( { 𝐶 , 𝐷 } ∈ 𝐸 ∧ { 𝐷 , 𝐴 } ∈ 𝐸 ) )
5		simpl3	⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) ) ∧ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐷 } ∈ 𝐸 ∧ { 𝐷 , 𝐴 } ∈ 𝐸 ) ) ) → ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) )
6		4cycl2vnunb	⊢ ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐷 } ∈ 𝐸 ∧ { 𝐷 , 𝐴 } ∈ 𝐸 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) ) → ¬ ∃! 𝑥 ∈ 𝑉 { { 𝐴 , 𝑥 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 )
7	3 4 5 6	syl3anc	⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) ) ∧ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐷 } ∈ 𝐸 ∧ { 𝐷 , 𝐴 } ∈ 𝐸 ) ) ) → ¬ ∃! 𝑥 ∈ 𝑉 { { 𝐴 , 𝑥 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 )
8	1 2	frcond1	⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ∃! 𝑥 ∈ 𝑉 { { 𝐴 , 𝑥 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 ) )
9		pm2.24	⊢ ( ∃! 𝑥 ∈ 𝑉 { { 𝐴 , 𝑥 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 → ( ¬ ∃! 𝑥 ∈ 𝑉 { { 𝐴 , 𝑥 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 → ¬ 𝐺 ∈ FriendGraph ) )
10	8 9	syl6com	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) → ( 𝐺 ∈ FriendGraph → ( ¬ ∃! 𝑥 ∈ 𝑉 { { 𝐴 , 𝑥 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 → ¬ 𝐺 ∈ FriendGraph ) ) )
11	10	3ad2ant2	⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) ) → ( 𝐺 ∈ FriendGraph → ( ¬ ∃! 𝑥 ∈ 𝑉 { { 𝐴 , 𝑥 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 → ¬ 𝐺 ∈ FriendGraph ) ) )
12	11	com23	⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) ) → ( ¬ ∃! 𝑥 ∈ 𝑉 { { 𝐴 , 𝑥 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 → ( 𝐺 ∈ FriendGraph → ¬ 𝐺 ∈ FriendGraph ) ) )
13	12	adantr	⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) ) ∧ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐷 } ∈ 𝐸 ∧ { 𝐷 , 𝐴 } ∈ 𝐸 ) ) ) → ( ¬ ∃! 𝑥 ∈ 𝑉 { { 𝐴 , 𝑥 } , { 𝑥 , 𝐶 } } ⊆ 𝐸 → ( 𝐺 ∈ FriendGraph → ¬ 𝐺 ∈ FriendGraph ) ) )
14	7 13	mpd	⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) ) ∧ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐷 } ∈ 𝐸 ∧ { 𝐷 , 𝐴 } ∈ 𝐸 ) ) ) → ( 𝐺 ∈ FriendGraph → ¬ 𝐺 ∈ FriendGraph ) )
15	14	pm2.01d	⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) ) ∧ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐷 } ∈ 𝐸 ∧ { 𝐷 , 𝐴 } ∈ 𝐸 ) ) ) → ¬ 𝐺 ∈ FriendGraph )
16		df-nel	⊢ ( 𝐺 ∉ FriendGraph ↔ ¬ 𝐺 ∈ FriendGraph )
17	15 16	sylibr	⊢ ( ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) ) ∧ ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐷 } ∈ 𝐸 ∧ { 𝐷 , 𝐴 } ∈ 𝐸 ) ) ) → 𝐺 ∉ FriendGraph )
18	17	ex	⊢ ( ( 𝐺 ∈ USGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ≠ 𝐶 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ∧ 𝐵 ≠ 𝐷 ) ) → ( ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝐶 } ∈ 𝐸 ) ∧ ( { 𝐶 , 𝐷 } ∈ 𝐸 ∧ { 𝐷 , 𝐴 } ∈ 𝐸 ) ) → 𝐺 ∉ FriendGraph ) )