Step |
Hyp |
Ref |
Expression |
1 |
|
frgrregorufr0.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
frgrregorufr0.e |
⊢ 𝐸 = ( Edg ‘ 𝐺 ) |
3 |
|
frgrregorufr0.d |
⊢ 𝐷 = ( VtxDeg ‘ 𝐺 ) |
4 |
1 2 3
|
frgrregorufr0 |
⊢ ( 𝐺 ∈ FriendGraph → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) |
5 |
|
orc |
⊢ ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) |
6 |
5
|
a1d |
⊢ ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 → ( ∃ 𝑎 ∈ 𝑉 ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) |
7 |
|
fveq2 |
⊢ ( 𝑣 = 𝑎 → ( 𝐷 ‘ 𝑣 ) = ( 𝐷 ‘ 𝑎 ) ) |
8 |
7
|
neeq1d |
⊢ ( 𝑣 = 𝑎 → ( ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ↔ ( 𝐷 ‘ 𝑎 ) ≠ 𝐾 ) ) |
9 |
8
|
rspcva |
⊢ ( ( 𝑎 ∈ 𝑉 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ) → ( 𝐷 ‘ 𝑎 ) ≠ 𝐾 ) |
10 |
|
df-ne |
⊢ ( ( 𝐷 ‘ 𝑎 ) ≠ 𝐾 ↔ ¬ ( 𝐷 ‘ 𝑎 ) = 𝐾 ) |
11 |
|
pm2.21 |
⊢ ( ¬ ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) |
12 |
10 11
|
sylbi |
⊢ ( ( 𝐷 ‘ 𝑎 ) ≠ 𝐾 → ( ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) |
13 |
9 12
|
syl |
⊢ ( ( 𝑎 ∈ 𝑉 ∧ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ) → ( ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) |
14 |
13
|
ancoms |
⊢ ( ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∧ 𝑎 ∈ 𝑉 ) → ( ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) |
15 |
14
|
rexlimdva |
⊢ ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 → ( ∃ 𝑎 ∈ 𝑉 ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) |
16 |
|
olc |
⊢ ( ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) |
17 |
16
|
a1d |
⊢ ( ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 → ( ∃ 𝑎 ∈ 𝑉 ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) |
18 |
6 15 17
|
3jaoi |
⊢ ( ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) ≠ 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) → ( ∃ 𝑎 ∈ 𝑉 ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) |
19 |
4 18
|
syl |
⊢ ( 𝐺 ∈ FriendGraph → ( ∃ 𝑎 ∈ 𝑉 ( 𝐷 ‘ 𝑎 ) = 𝐾 → ( ∀ 𝑣 ∈ 𝑉 ( 𝐷 ‘ 𝑣 ) = 𝐾 ∨ ∃ 𝑣 ∈ 𝑉 ∀ 𝑤 ∈ ( 𝑉 ∖ { 𝑣 } ) { 𝑣 , 𝑤 } ∈ 𝐸 ) ) ) |