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