Metamath Proof Explorer

Theorem frgrwopreglem4a

Description: In a friendship graph any two vertices with different degrees are connected. Alternate version of frgrwopreglem4 without a fixed degree and without using the sets A and B . (Contributed by Alexander van der Vekens, 30-Dec-2017) (Revised by AV, 4-Feb-2022)

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

Proof

Step Hyp Ref Expression
1 frgrncvvdeq.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 frgrncvvdeq.d ⊢ 𝐷 = ( VtxDeg ‘ 𝐺 )
3 frgrwopreglem4a.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
4 fveq2 ⊢ ( 𝑋 = 𝑌 → ( 𝐷 ‘ 𝑋 ) = ( 𝐷 ‘ 𝑌 ) )
5 4 a1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 = 𝑌 → ( 𝐷 ‘ 𝑋 ) = ( 𝐷 ‘ 𝑌 ) ) )
6 5 necon3d ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) → 𝑋 ≠ 𝑌 ) )
7 6 imp ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) → 𝑋 ≠ 𝑌 )
8 7 3adant1 ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) → 𝑋 ≠ 𝑌 )
9 1 2 frgrncvvdeq ⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ( 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) → ( 𝐷 ‘ 𝑥 ) = ( 𝐷 ‘ 𝑦 ) ) )
10 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐺 NeighbVtx 𝑥 ) = ( 𝐺 NeighbVtx 𝑋 ) )
11 neleq2 ⊢ ( ( 𝐺 NeighbVtx 𝑥 ) = ( 𝐺 NeighbVtx 𝑋 ) → ( 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ↔ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑋 ) ) )
12 10 11 syl ⊢ ( 𝑥 = 𝑋 → ( 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ↔ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑋 ) ) )
13 fveqeq2 ⊢ ( 𝑥 = 𝑋 → ( ( 𝐷 ‘ 𝑥 ) = ( 𝐷 ‘ 𝑦 ) ↔ ( 𝐷 ‘ 𝑋 ) = ( 𝐷 ‘ 𝑦 ) ) )
14 12 13 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) → ( 𝐷 ‘ 𝑥 ) = ( 𝐷 ‘ 𝑦 ) ) ↔ ( 𝑦 ∉ ( 𝐺 NeighbVtx 𝑋 ) → ( 𝐷 ‘ 𝑋 ) = ( 𝐷 ‘ 𝑦 ) ) ) )
15 neleq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ∉ ( 𝐺 NeighbVtx 𝑋 ) ↔ 𝑌 ∉ ( 𝐺 NeighbVtx 𝑋 ) ) )
16 fveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝐷 ‘ 𝑦 ) = ( 𝐷 ‘ 𝑌 ) )
17 16 eqeq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝐷 ‘ 𝑋 ) = ( 𝐷 ‘ 𝑦 ) ↔ ( 𝐷 ‘ 𝑋 ) = ( 𝐷 ‘ 𝑌 ) ) )
18 15 17 imbi12d ⊢ ( 𝑦 = 𝑌 → ( ( 𝑦 ∉ ( 𝐺 NeighbVtx 𝑋 ) → ( 𝐷 ‘ 𝑋 ) = ( 𝐷 ‘ 𝑦 ) ) ↔ ( 𝑌 ∉ ( 𝐺 NeighbVtx 𝑋 ) → ( 𝐷 ‘ 𝑋 ) = ( 𝐷 ‘ 𝑌 ) ) ) )
19 simpll ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → 𝑋 ∈ 𝑉 )
20 sneq ⊢ ( 𝑥 = 𝑋 → { 𝑥 } = { 𝑋 } )
21 20 difeq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑉 ∖ { 𝑥 } ) = ( 𝑉 ∖ { 𝑋 } ) )
22 21 adantl ⊢ ( ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) ∧ 𝑥 = 𝑋 ) → ( 𝑉 ∖ { 𝑥 } ) = ( 𝑉 ∖ { 𝑋 } ) )
23 simpr ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → 𝑌 ∈ 𝑉 )
24 necom ⊢ ( 𝑋 ≠ 𝑌 ↔ 𝑌 ≠ 𝑋 )
25 24 biimpi ⊢ ( 𝑋 ≠ 𝑌 → 𝑌 ≠ 𝑋 )
26 23 25 anim12i ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝑌 ∈ 𝑉 ∧ 𝑌 ≠ 𝑋 ) )
27 eldifsn ⊢ ( 𝑌 ∈ ( 𝑉 ∖ { 𝑋 } ) ↔ ( 𝑌 ∈ 𝑉 ∧ 𝑌 ≠ 𝑋 ) )
28 26 27 sylibr ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → 𝑌 ∈ ( 𝑉 ∖ { 𝑋 } ) )
29 14 18 19 22 28 rspc2vd ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ( 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) → ( 𝐷 ‘ 𝑥 ) = ( 𝐷 ‘ 𝑦 ) ) → ( 𝑌 ∉ ( 𝐺 NeighbVtx 𝑋 ) → ( 𝐷 ‘ 𝑋 ) = ( 𝐷 ‘ 𝑌 ) ) ) )
30 nnel ⊢ ( ¬ 𝑌 ∉ ( 𝐺 NeighbVtx 𝑋 ) ↔ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) )
31 nbgrsym ⊢ ( 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ↔ 𝑋 ∈ ( 𝐺 NeighbVtx 𝑌 ) )
32 frgrusgr ⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph )
33 3 nbusgreledg ⊢ ( 𝐺 ∈ USGraph → ( 𝑋 ∈ ( 𝐺 NeighbVtx 𝑌 ) ↔ { 𝑋 , 𝑌 } ∈ 𝐸 ) )
34 32 33 syl ⊢ ( 𝐺 ∈ FriendGraph → ( 𝑋 ∈ ( 𝐺 NeighbVtx 𝑌 ) ↔ { 𝑋 , 𝑌 } ∈ 𝐸 ) )
35 34 biimpd ⊢ ( 𝐺 ∈ FriendGraph → ( 𝑋 ∈ ( 𝐺 NeighbVtx 𝑌 ) → { 𝑋 , 𝑌 } ∈ 𝐸 ) )
36 31 35 biimtrid ⊢ ( 𝐺 ∈ FriendGraph → ( 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) → { 𝑋 , 𝑌 } ∈ 𝐸 ) )
37 36 imp ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) → { 𝑋 , 𝑌 } ∈ 𝐸 )
38 37 a1d ⊢ ( ( 𝐺 ∈ FriendGraph ∧ 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) ) → ( ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) → { 𝑋 , 𝑌 } ∈ 𝐸 ) )
39 38 expcom ⊢ ( 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) → ( 𝐺 ∈ FriendGraph → ( ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) → { 𝑋 , 𝑌 } ∈ 𝐸 ) ) )
40 39 a1d ⊢ ( 𝑌 ∈ ( 𝐺 NeighbVtx 𝑋 ) → ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝐺 ∈ FriendGraph → ( ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) → { 𝑋 , 𝑌 } ∈ 𝐸 ) ) ) )
41 30 40 sylbi ⊢ ( ¬ 𝑌 ∉ ( 𝐺 NeighbVtx 𝑋 ) → ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝐺 ∈ FriendGraph → ( ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) → { 𝑋 , 𝑌 } ∈ 𝐸 ) ) ) )
42 eqneqall ⊢ ( ( 𝐷 ‘ 𝑋 ) = ( 𝐷 ‘ 𝑌 ) → ( ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) → { 𝑋 , 𝑌 } ∈ 𝐸 ) )
43 42 2a1d ⊢ ( ( 𝐷 ‘ 𝑋 ) = ( 𝐷 ‘ 𝑌 ) → ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝐺 ∈ FriendGraph → ( ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) → { 𝑋 , 𝑌 } ∈ 𝐸 ) ) ) )
44 41 43 ja ⊢ ( ( 𝑌 ∉ ( 𝐺 NeighbVtx 𝑋 ) → ( 𝐷 ‘ 𝑋 ) = ( 𝐷 ‘ 𝑌 ) ) → ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( 𝐺 ∈ FriendGraph → ( ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) → { 𝑋 , 𝑌 } ∈ 𝐸 ) ) ) )
45 44 com12 ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑌 ∉ ( 𝐺 NeighbVtx 𝑋 ) → ( 𝐷 ‘ 𝑋 ) = ( 𝐷 ‘ 𝑌 ) ) → ( 𝐺 ∈ FriendGraph → ( ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) → { 𝑋 , 𝑌 } ∈ 𝐸 ) ) ) )
46 29 45 syld ⊢ ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ( 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) → ( 𝐷 ‘ 𝑥 ) = ( 𝐷 ‘ 𝑦 ) ) → ( 𝐺 ∈ FriendGraph → ( ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) → { 𝑋 , 𝑌 } ∈ 𝐸 ) ) ) )
47 46 com3l ⊢ ( ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ( 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) → ( 𝐷 ‘ 𝑥 ) = ( 𝐷 ‘ 𝑦 ) ) → ( 𝐺 ∈ FriendGraph → ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) → { 𝑋 , 𝑌 } ∈ 𝐸 ) ) ) )
48 9 47 mpcom ⊢ ( 𝐺 ∈ FriendGraph → ( ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) → { 𝑋 , 𝑌 } ∈ 𝐸 ) ) )
49 48 expd ⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑋 ≠ 𝑌 → ( ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) → { 𝑋 , 𝑌 } ∈ 𝐸 ) ) ) )
50 49 com34 ⊢ ( 𝐺 ∈ FriendGraph → ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) → ( 𝑋 ≠ 𝑌 → { 𝑋 , 𝑌 } ∈ 𝐸 ) ) ) )
51 50 3imp ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) → ( 𝑋 ≠ 𝑌 → { 𝑋 , 𝑌 } ∈ 𝐸 ) )
52 8 51 mpd ⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) ∧ ( 𝐷 ‘ 𝑋 ) ≠ ( 𝐷 ‘ 𝑌 ) ) → { 𝑋 , 𝑌 } ∈ 𝐸 )