Step |
Hyp |
Ref |
Expression |
1 |
|
frgrncvvdeq.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
frgrncvvdeq.d |
⊢ 𝐷 = ( VtxDeg ‘ 𝐺 ) |
3 |
|
ovexd |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( 𝐺 NeighbVtx 𝑥 ) ∈ V ) |
4 |
|
eqid |
⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) |
5 |
|
eqid |
⊢ ( 𝐺 NeighbVtx 𝑥 ) = ( 𝐺 NeighbVtx 𝑥 ) |
6 |
|
eqid |
⊢ ( 𝐺 NeighbVtx 𝑦 ) = ( 𝐺 NeighbVtx 𝑦 ) |
7 |
|
simpl |
⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) → 𝑥 ∈ 𝑉 ) |
8 |
7
|
ad2antlr |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → 𝑥 ∈ 𝑉 ) |
9 |
|
eldifi |
⊢ ( 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) → 𝑦 ∈ 𝑉 ) |
10 |
9
|
adantl |
⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) → 𝑦 ∈ 𝑉 ) |
11 |
10
|
ad2antlr |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → 𝑦 ∈ 𝑉 ) |
12 |
|
eldif |
⊢ ( 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ↔ ( 𝑦 ∈ 𝑉 ∧ ¬ 𝑦 ∈ { 𝑥 } ) ) |
13 |
|
velsn |
⊢ ( 𝑦 ∈ { 𝑥 } ↔ 𝑦 = 𝑥 ) |
14 |
13
|
biimpri |
⊢ ( 𝑦 = 𝑥 → 𝑦 ∈ { 𝑥 } ) |
15 |
14
|
equcoms |
⊢ ( 𝑥 = 𝑦 → 𝑦 ∈ { 𝑥 } ) |
16 |
15
|
necon3bi |
⊢ ( ¬ 𝑦 ∈ { 𝑥 } → 𝑥 ≠ 𝑦 ) |
17 |
12 16
|
simplbiim |
⊢ ( 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) → 𝑥 ≠ 𝑦 ) |
18 |
17
|
adantl |
⊢ ( ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) → 𝑥 ≠ 𝑦 ) |
19 |
18
|
ad2antlr |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → 𝑥 ≠ 𝑦 ) |
20 |
|
simpr |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) |
21 |
|
simpl |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) → 𝐺 ∈ FriendGraph ) |
22 |
21
|
adantr |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → 𝐺 ∈ FriendGraph ) |
23 |
|
eqid |
⊢ ( 𝑎 ∈ ( 𝐺 NeighbVtx 𝑥 ) ↦ ( ℩ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑦 ) { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) ) = ( 𝑎 ∈ ( 𝐺 NeighbVtx 𝑥 ) ↦ ( ℩ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑦 ) { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) ) |
24 |
1 4 5 6 8 11 19 20 22 23
|
frgrncvvdeqlem10 |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( 𝑎 ∈ ( 𝐺 NeighbVtx 𝑥 ) ↦ ( ℩ 𝑏 ∈ ( 𝐺 NeighbVtx 𝑦 ) { 𝑎 , 𝑏 } ∈ ( Edg ‘ 𝐺 ) ) ) : ( 𝐺 NeighbVtx 𝑥 ) –1-1-onto→ ( 𝐺 NeighbVtx 𝑦 ) ) |
25 |
3 24
|
hasheqf1od |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑥 ) ) = ( ♯ ‘ ( 𝐺 NeighbVtx 𝑦 ) ) ) |
26 |
|
frgrusgr |
⊢ ( 𝐺 ∈ FriendGraph → 𝐺 ∈ USGraph ) |
27 |
26 7
|
anim12i |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) → ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ 𝑉 ) ) |
28 |
27
|
adantr |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ 𝑉 ) ) |
29 |
1
|
hashnbusgrvd |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑥 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑥 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) |
30 |
28 29
|
syl |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑥 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) ) |
31 |
26 10
|
anim12i |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) → ( 𝐺 ∈ USGraph ∧ 𝑦 ∈ 𝑉 ) ) |
32 |
31
|
adantr |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( 𝐺 ∈ USGraph ∧ 𝑦 ∈ 𝑉 ) ) |
33 |
1
|
hashnbusgrvd |
⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑦 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑦 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑦 ) ) |
34 |
32 33
|
syl |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑦 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑦 ) ) |
35 |
25 30 34
|
3eqtr3d |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑦 ) ) |
36 |
2
|
fveq1i |
⊢ ( 𝐷 ‘ 𝑥 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑥 ) |
37 |
2
|
fveq1i |
⊢ ( 𝐷 ‘ 𝑦 ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑦 ) |
38 |
35 36 37
|
3eqtr4g |
⊢ ( ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) ∧ 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) ) → ( 𝐷 ‘ 𝑥 ) = ( 𝐷 ‘ 𝑦 ) ) |
39 |
38
|
ex |
⊢ ( ( 𝐺 ∈ FriendGraph ∧ ( 𝑥 ∈ 𝑉 ∧ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ) ) → ( 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) → ( 𝐷 ‘ 𝑥 ) = ( 𝐷 ‘ 𝑦 ) ) ) |
40 |
39
|
ralrimivva |
⊢ ( 𝐺 ∈ FriendGraph → ∀ 𝑥 ∈ 𝑉 ∀ 𝑦 ∈ ( 𝑉 ∖ { 𝑥 } ) ( 𝑦 ∉ ( 𝐺 NeighbVtx 𝑥 ) → ( 𝐷 ‘ 𝑥 ) = ( 𝐷 ‘ 𝑦 ) ) ) |