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 ∧ ( ( 𝐴𝑉𝑋𝑉 ) ∧ ( 𝐵𝑉𝑌𝑉 ) ) ∧ ( ( 𝐷𝐴 ) = ( 𝐷𝑋 ) ∧ ( 𝐷𝐴 ) ≠ ( 𝐷𝐵 ) ∧ ( 𝐷𝑋 ) ≠ ( 𝐷𝑌 ) ) ) → ( ( { 𝐴 , 𝐵 } ∈ 𝐸 ∧ { 𝐵 , 𝑋 } ∈ 𝐸 ) ∧ ( { 𝑋 , 𝑌 } ∈ 𝐸 ∧ { 𝑌 , 𝐴 } ∈ 𝐸 ) ) )