Metamath Proof Explorer

Theorem 2pthfrgr

Description: Between any two (different) vertices in a friendship graph, tere is a 2-path (simple 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, 6-Dec-2017) (Revised by AV, 1-Apr-2021)

Ref Expression
Hypothesis 2pthfrgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion 2pthfrgr ( 𝐺 ∈ FriendGraph → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )

Proof

Step Hyp Ref Expression
1 2pthfrgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
3 1 2 2pthfrgrrn2 ⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑚 ∈ 𝑉 ( ( { 𝑎 , 𝑚 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑚 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏 ) ) )
4 frgrusgr ⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
5 usgruhgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ UHGraph )
6 4 5 syl ⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ UHGraph )
7 6 adantr ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ∈ 𝑉 ) → 𝐺 ∈ UHGraph )
8 7 adantr ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) → 𝐺 ∈ UHGraph )
9 8 adantr ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ∧ 𝑚 ∈ 𝑉 ) → 𝐺 ∈ UHGraph )
10 simpllr ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ∧ 𝑚 ∈ 𝑉 ) → 𝑎 ∈ 𝑉 )
11 simpr ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ∧ 𝑚 ∈ 𝑉 ) → 𝑚 ∈ 𝑉 )
12 eldifi ⊢ ( 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) → 𝑏 ∈ 𝑉 )
13 12 ad2antlr ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ∧ 𝑚 ∈ 𝑉 ) → 𝑏 ∈ 𝑉 )
14 10 11 13 3jca ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ∧ 𝑚 ∈ 𝑉 ) → ( 𝑎 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) )
15 9 14 jca ⊢ ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ∧ 𝑚 ∈ 𝑉 ) → ( 𝐺 ∈ UHGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) )
16 15 adantr ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ∧ 𝑚 ∈ 𝑉 ) ∧ ( ( { 𝑎 , 𝑚 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑚 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏 ) ) ) → ( 𝐺 ∈ UHGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) )
17 simprrl ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ∧ 𝑚 ∈ 𝑉 ) ∧ ( ( { 𝑎 , 𝑚 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑚 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏 ) ) ) → 𝑎 ≠ 𝑚 )
18 eldifsn ⊢ ( 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ↔ ( 𝑏 ∈ 𝑉 ∧ 𝑏 ≠ 𝑎 ) )
19 necom ⊢ ( 𝑏 ≠ 𝑎 ↔ 𝑎 ≠ 𝑏 )
20 19 biimpi ⊢ ( 𝑏 ≠ 𝑎 → 𝑎 ≠ 𝑏 )
21 18 20 simplbiim ⊢ ( 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) → 𝑎 ≠ 𝑏 )
22 21 ad3antlr ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ∧ 𝑚 ∈ 𝑉 ) ∧ ( ( { 𝑎 , 𝑚 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑚 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏 ) ) ) → 𝑎 ≠ 𝑏 )
23 simprrr ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ∧ 𝑚 ∈ 𝑉 ) ∧ ( ( { 𝑎 , 𝑚 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑚 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏 ) ) ) → 𝑚 ≠ 𝑏 )
24 simprl ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ∧ 𝑚 ∈ 𝑉 ) ∧ ( ( { 𝑎 , 𝑚 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑚 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏 ) ) ) → ( { 𝑎 , 𝑚 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑚 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) )
25 1 2 2pthon3v ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑚 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) ∧ ( 𝑎 ≠ 𝑚 ∧ 𝑎 ≠ 𝑏 ∧ 𝑚 ≠ 𝑏 ) ∧ ( { 𝑎 , 𝑚 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑚 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )
26 16 17 22 23 24 25 syl131anc ⊢ ( ( ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) ∧ 𝑚 ∈ 𝑉 ) ∧ ( ( { 𝑎 , 𝑚 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑚 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏 ) ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )
27 26 rexlimdva2 ⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ∈ 𝑉 ) ∧ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ) → ( ∃ 𝑚 ∈ 𝑉 ( ( { 𝑎 , 𝑚 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑚 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏 ) ) → ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
28 27 ralimdva ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑎 ∈ 𝑉 ) → ( ∀ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑚 ∈ 𝑉 ( ( { 𝑎 , 𝑚 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑚 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏 ) ) → ∀ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
29 28 ralimdva ⊢ ( 𝐺 ∈ FriendGraph → ( ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑚 ∈ 𝑉 ( ( { 𝑎 , 𝑚 } ∈ ( Edg ‘ 𝐺 ) ∧ { 𝑚 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) ∧ ( 𝑎 ≠ 𝑚 ∧ 𝑚 ≠ 𝑏 ) ) → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) ) )
30 3 29 mpd ⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑎 ∈ 𝑉 ∀ 𝑏 ∈ ( 𝑉 ∖ { 𝑎 } ) ∃ 𝑓 ∃ 𝑝 ( 𝑓 ( 𝑎 ( SPathsOn ‘ 𝐺 ) 𝑏 ) 𝑝 ∧ ( ♯ ‘ 𝑓 ) = 2 ) )