Metamath Proof Explorer


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