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 < ( ♯ ‘ 𝑉 ) ) → ∀ 𝑎 ∈ 𝑉 ∃ 𝑏 ∈ 𝑉 ∃ 𝑐 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ∧ { 𝑐 , 𝑎 } ∈ 𝐸 ) )