Metamath Proof Explorer

Theorem 2pthfrgrrn2

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, 16-Nov-2017) (Revised by AV, 1-Apr-2021)

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

Proof

Step Hyp Ref Expression
1 2pthfrgrrn.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 2pthfrgrrn.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 1 2 2pthfrgrrn ⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑎 ∈ 𝑉 ∀ 𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) )
4 frgrusgr ⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
5 2 usgredgne ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝑎 , 𝑏 } ∈ 𝐸 ) → 𝑎 ≠ 𝑏 )
6 5 ex ⊢ ( 𝐺 ∈ USGraph → ( { 𝑎 , 𝑏 } ∈ 𝐸 → 𝑎 ≠ 𝑏 ) )
7 2 usgredgne ⊢ ( ( 𝐺 ∈ USGraph ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → 𝑏 ≠ 𝑐 )
8 7 ex ⊢ ( 𝐺 ∈ USGraph → ( { 𝑏 , 𝑐 } ∈ 𝐸 → 𝑏 ≠ 𝑐 ) )
9 6 8 anim12d ⊢ ( 𝐺 ∈ USGraph → ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ) ) )
10 4 9 syl ⊢ ( 𝐺 ∈ FriendGraph → ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ) ) )
11 10 ad2antrr ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ) ∧ 𝑏 ∈ 𝑉 ) → ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ) ) )
12 11 ancld ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ) ∧ 𝑏 ∈ 𝑉 ) → ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ) ) ) )
13 12 reximdva ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ) → ( ∃ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → ∃ 𝑏 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ) ) ) )
14 13 ralimdvva ⊢ ( 𝐺 ∈ FriendGraph → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑏 ∈ 𝑉 ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) → ∀ 𝑎 ∈ 𝑉 ∀ 𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑏 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ) ) ) )
15 3 14 mpd ⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑎 ∈ 𝑉 ∀ 𝑐 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑏 ∈ 𝑉 ( ( { 𝑎 , 𝑏 } ∈ 𝐸 ∧ { 𝑏 , 𝑐 } ∈ 𝐸 ) ∧ ( 𝑎 ≠ 𝑏 ∧ 𝑏 ≠ 𝑐 ) ) )