Metamath Proof Explorer

Theorem frgrwopreglem5a

Description: If a friendship graph has two vertices with the same degree and two other vertices with different degrees, then there is a 4-cycle in the graph. Alternate version of frgrwopreglem5 without a fixed degree and without using the sets A and B . (Contributed by Alexander van der Vekens, 31-Dec-2017) (Revised by AV, 4-Feb-2022)

Ref Expression
Hypotheses frgrncvvdeq.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
frgrncvvdeq.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
frgrwopreglem4a.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion frgrwopreglem5a ( ( 𝐺 ∈ FriendGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝑋 ) ∧ ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝐵 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) ) → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝑋 } ∈ 𝐸 ) ∧ ( { 𝑋 , 𝑌 } ∈ 𝐸 ∧ { 𝑌 , 𝐴 } ∈ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 frgrncvvdeq.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 frgrncvvdeq.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
3 frgrwopreglem4a.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
4 id ⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ FriendGraph )
5 simpl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → 𝐴 ∈ 𝑉 )
6 simpl ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 𝐵 ∈ 𝑉 )
7 5 6 anim12i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) )
8 simp2 ⊢ ( ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝑋 ) ∧ ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝐵 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) → ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝐵 ) )
9 1 2 3 frgrwopreglem4a ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝐵 ) ) → { 𝐴 , 𝐵 } ∈ 𝐸 )
10 4 7 8 9 syl3an ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝑋 ) ∧ ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝐵 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) ) → { 𝐴 , 𝐵 } ∈ 𝐸 )
11 simpr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → 𝑋 ∈ 𝑉 )
12 11 6 anim12ci ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) )
13 pm13.18 ⊢ ( ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝑋 ) ∧ ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝐵 ) ) → ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝐵 ) )
14 13 3adant3 ⊢ ( ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝑋 ) ∧ ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝐵 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) → ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝐵 ) )
15 14 necomd ⊢ ( ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝑋 ) ∧ ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝐵 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) → ( 𝐷 ‘ 𝐵 ) ≠ ( 𝐷 ‘ 𝑋 ) )
16 1 2 3 frgrwopreglem4a ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝐵 ) ≠ ( 𝐷 ‘ 𝑋 ) ) → { 𝐵 , 𝑋 } ∈ 𝐸 )
17 4 12 15 16 syl3an ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝑋 ) ∧ ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝐵 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) ) → { 𝐵 , 𝑋 } ∈ 𝐸 )
18 simpr ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 𝑌 ∈ 𝑉 )
19 11 18 anim12i ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) )
20 simp3 ⊢ ( ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝑋 ) ∧ ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝐵 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) → ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) )
21 1 2 3 frgrwopreglem4a ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) → { 𝑋 , 𝑌 } ∈ 𝐸 )
22 4 19 20 21 syl3an ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝑋 ) ∧ ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝐵 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) ) → { 𝑋 , 𝑌 } ∈ 𝐸 )
23 5 18 anim12ci ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) → ( 𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) )
24 pm13.181 ⊢ ( ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝑋 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) → ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝑌 ) )
25 24 3adant2 ⊢ ( ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝑋 ) ∧ ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝐵 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) → ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝑌 ) )
26 25 necomd ⊢ ( ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝑋 ) ∧ ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝐵 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) → ( 𝐷 ‘ 𝑌 ) ≠ ( 𝐷 ‘ 𝐴 ) )
27 1 2 3 frgrwopreglem4a ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑌 ) ≠ ( 𝐷 ‘ 𝐴 ) ) → { 𝑌 , 𝐴 } ∈ 𝐸 )
28 4 23 26 27 syl3an ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝑋 ) ∧ ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝐵 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) ) → { 𝑌 , 𝐴 } ∈ 𝐸 )
29 22 28 jca ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝑋 ) ∧ ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝐵 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) ) → ( { 𝑋 , 𝑌 } ∈ 𝐸 ∧ { 𝑌 , 𝐴 } ∈ 𝐸 ) )
30 10 17 29 jca31 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( ( 𝐴 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ) ∧ ( ( 𝐷 ‘ 𝐴 ) = ( 𝐷 ‘ 𝑋 ) ∧ ( 𝐷 ‘ 𝐴 ) ≠ ( 𝐷 ‘ 𝐵 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) ) → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝑋 } ∈ 𝐸 ) ∧ ( { 𝑋 , 𝑌 } ∈ 𝐸 ∧ { 𝑌 , 𝐴 } ∈ 𝐸 ) ) )