Metamath Proof Explorer


Theorem 3cyclfrgrrn

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

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

Proof

Step Hyp Ref Expression
1 3cyclfrgrrn1.v 𝑉 = ( Vtx ‘ 𝐺 )
2 3cyclfrgrrn1.e 𝐸 = ( Edg ‘ 𝐺 )
3 1 fvexi 𝑉 ∈ V
4 hashgt12el2 ( ( 𝑉 ∈ V ∧ 1 < ( ♯ ‘ 𝑉 ) ∧ 𝑎𝑉 ) → ∃ 𝑥𝑉 𝑎𝑥 )
5 3 4 mp3an1 ( ( 1 < ( ♯ ‘ 𝑉 ) ∧ 𝑎𝑉 ) → ∃ 𝑥𝑉 𝑎𝑥 )
6 simpr ( ( ( 𝑥𝑉𝑎𝑥𝑎𝑉 ) ∧ 𝐺 ∈ FriendGraph ) → 𝐺 ∈ FriendGraph )
7 pm3.22 ( ( 𝑥𝑉𝑎𝑉 ) → ( 𝑎𝑉𝑥𝑉 ) )
8 7 3adant2 ( ( 𝑥𝑉𝑎𝑥𝑎𝑉 ) → ( 𝑎𝑉𝑥𝑉 ) )
9 8 adantr ( ( ( 𝑥𝑉𝑎𝑥𝑎𝑉 ) ∧ 𝐺 ∈ FriendGraph ) → ( 𝑎𝑉𝑥𝑉 ) )
10 simpl2 ( ( ( 𝑥𝑉𝑎𝑥𝑎𝑉 ) ∧ 𝐺 ∈ FriendGraph ) → 𝑎𝑥 )
11 1 2 3cyclfrgrrn1 ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑎𝑉𝑥𝑉 ) ∧ 𝑎𝑥 ) → ∃ 𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) )
12 6 9 10 11 syl3anc ( ( ( 𝑥𝑉𝑎𝑥𝑎𝑉 ) ∧ 𝐺 ∈ FriendGraph ) → ∃ 𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) )
13 12 3exp1 ( 𝑥𝑉 → ( 𝑎𝑥 → ( 𝑎𝑉 → ( 𝐺 ∈ FriendGraph → ∃ 𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) ) ) )
14 13 rexlimiv ( ∃ 𝑥𝑉 𝑎𝑥 → ( 𝑎𝑉 → ( 𝐺 ∈ FriendGraph → ∃ 𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) ) )
15 5 14 syl ( ( 1 < ( ♯ ‘ 𝑉 ) ∧ 𝑎𝑉 ) → ( 𝑎𝑉 → ( 𝐺 ∈ FriendGraph → ∃ 𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) ) )
16 15 expcom ( 𝑎𝑉 → ( 1 < ( ♯ ‘ 𝑉 ) → ( 𝑎𝑉 → ( 𝐺 ∈ FriendGraph → ∃ 𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) ) ) )
17 16 pm2.43a ( 𝑎𝑉 → ( 1 < ( ♯ ‘ 𝑉 ) → ( 𝐺 ∈ FriendGraph → ∃ 𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) ) )
18 17 com13 ( 𝐺 ∈ FriendGraph → ( 1 < ( ♯ ‘ 𝑉 ) → ( 𝑎𝑉 → ∃ 𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) ) )
19 18 imp ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ( 𝑎𝑉 → ∃ 𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) ) )
20 19 ralrimiv ( ( 𝐺 ∈ FriendGraph ∧ 1 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑎𝑉𝑏𝑉𝑐𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) )