Theorem 3cyclfrgrrn2

Description: Every vertex in a friendship graph (with more than 1 vertex) is part of a 3-cycle. (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 2-Apr-2021)

	Ref	Expression
Hypotheses	3cyclfrgrrn1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	3cyclfrgrrn1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	3cyclfrgrrn2	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) )

Proof

Step	Hyp	Ref	Expression
1		3cyclfrgrrn1.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		3cyclfrgrrn1.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3	1 2	3cyclfrgrrn	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) )
4		frgrusgr	⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
5	2	usgredgne	⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → 𝑏 ≠ 𝑐 )
6	5	expcom	⊢ ( { 𝑏 , 𝑐 } ∈ 𝐸 → ( 𝐺 ∈ USGraph → 𝑏 ≠ 𝑐 ) )
7	6	3ad2ant2	⊢ ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → ( 𝐺 ∈ USGraph → 𝑏 ≠ 𝑐 ) )
8	4 7	syl5com	⊢ ( 𝐺 ∈ FriendGraph → ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → 𝑏 ≠ 𝑐 ) )
9	8	adantr	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → 𝑏 ≠ 𝑐 ) )
10	9	ancrd	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → ( 𝑏 ≠ 𝑐 ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) ) )
11	10	reximdv	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ∃ 𝑐 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) ) )
12	11	reximdv	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) ) )
13	12	ralimdv	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( ∀ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) → ∀ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) ) )
14	3 13	mpd	⊢ ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( 𝑏 ≠ 𝑐 ∧ ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) )