Metamath Proof Explorer


Theorem 2pthfrgrrn

Description: Between any two (different) vertices in a friendship graph is a 2-path (path of length 2), see Proposition 1(b) of MertziosUnger p. 153 : "A friendship graph G ..., as well as the distance between any two nodes in G is at most two". (Contributed by Alexander van der Vekens, 15-Nov-2017) (Revised by AV, 1-Apr-2021)

Ref Expression
Hypotheses 2pthfrgrrn.v 𝑉 = ( Vtx ‘ 𝐺 )
2pthfrgrrn.e 𝐸 = ( Edg ‘ 𝐺 )
Assertion 2pthfrgrrn ( 𝐺 ∈ FriendGraph → ∀ 𝑎𝑉𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑏𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) )

Proof

Step Hyp Ref Expression
1 2pthfrgrrn.v 𝑉 = ( Vtx ‘ 𝐺 )
2 2pthfrgrrn.e 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 isfrgr ( 𝐺 ∈ FriendGraph ↔ ( 𝐺 ∈ USGraph ∧ ∀ 𝑎𝑉𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃! 𝑏𝑉 { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 ) )
4 reurex ( ∃! 𝑏𝑉 { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 → ∃ 𝑏𝑉 { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 )
5 prcom { 𝑎 , 𝑏 } = { 𝑏 , 𝑎 }
6 5 eleq1i ( { 𝑎 , 𝑏 } ∈ 𝐸 ↔ { 𝑏 , 𝑎 } ∈ 𝐸 )
7 6 anbi1i ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ↔ ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) )
8 zfpair2 { 𝑏 , 𝑎 } ∈ V
9 zfpair2 { 𝑏 , 𝑐 } ∈ V
10 8 9 prss ( ( { 𝑏 , 𝑎 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ↔ { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 )
11 7 10 sylbbr ( { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 → ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) )
12 11 reximi ( ∃ 𝑏𝑉 { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 → ∃ 𝑏𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) )
13 4 12 syl ( ∃! 𝑏𝑉 { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 → ∃ 𝑏𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) )
14 13 a1i ( ( 𝐺 ∈ USGraph ∧ ( 𝑎𝑉𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ) → ( ∃! 𝑏𝑉 { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 → ∃ 𝑏𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )
15 14 ralimdvva ( 𝐺 ∈ USGraph → ( ∀ 𝑎𝑉𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃! 𝑏𝑉 { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 → ∀ 𝑎𝑉𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑏𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ) )
16 15 imp ( ( 𝐺 ∈ USGraph ∧ ∀ 𝑎𝑉𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃! 𝑏𝑉 { { 𝑏 , 𝑎 } , { 𝑏 , 𝑐 } } ⊆ 𝐸 ) → ∀ 𝑎𝑉𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑏𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) )
17 3 16 sylbi ( 𝐺 ∈ FriendGraph → ∀ 𝑎𝑉𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑏𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) )