Step | Hyp | Ref
| Expression |
1 | | eleq1 2828 |
. . . . 5
⊢ (𝑘 = 𝐾 → (𝑘 ∈ ℕ0*
↔ 𝐾 ∈
ℕ0*)) |
2 | 1 | adantl 482 |
. . . 4
⊢ ((𝑔 = 𝐺 ∧ 𝑘 = 𝐾) → (𝑘 ∈ ℕ0*
↔ 𝐾 ∈
ℕ0*)) |
3 | | fveq2 6771 |
. . . . . 6
⊢ (𝑔 = 𝐺 → (Vtx‘𝑔) = (Vtx‘𝐺)) |
4 | 3 | adantr 481 |
. . . . 5
⊢ ((𝑔 = 𝐺 ∧ 𝑘 = 𝐾) → (Vtx‘𝑔) = (Vtx‘𝐺)) |
5 | | fveq2 6771 |
. . . . . . . 8
⊢ (𝑔 = 𝐺 → (VtxDeg‘𝑔) = (VtxDeg‘𝐺)) |
6 | 5 | fveq1d 6773 |
. . . . . . 7
⊢ (𝑔 = 𝐺 → ((VtxDeg‘𝑔)‘𝑣) = ((VtxDeg‘𝐺)‘𝑣)) |
7 | 6 | adantr 481 |
. . . . . 6
⊢ ((𝑔 = 𝐺 ∧ 𝑘 = 𝐾) → ((VtxDeg‘𝑔)‘𝑣) = ((VtxDeg‘𝐺)‘𝑣)) |
8 | | simpr 485 |
. . . . . 6
⊢ ((𝑔 = 𝐺 ∧ 𝑘 = 𝐾) → 𝑘 = 𝐾) |
9 | 7, 8 | eqeq12d 2756 |
. . . . 5
⊢ ((𝑔 = 𝐺 ∧ 𝑘 = 𝐾) → (((VtxDeg‘𝑔)‘𝑣) = 𝑘 ↔ ((VtxDeg‘𝐺)‘𝑣) = 𝐾)) |
10 | 4, 9 | raleqbidv 3335 |
. . . 4
⊢ ((𝑔 = 𝐺 ∧ 𝑘 = 𝐾) → (∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘 ↔ ∀𝑣 ∈ (Vtx‘𝐺)((VtxDeg‘𝐺)‘𝑣) = 𝐾)) |
11 | 2, 10 | anbi12d 631 |
. . 3
⊢ ((𝑔 = 𝐺 ∧ 𝑘 = 𝐾) → ((𝑘 ∈ ℕ0* ∧
∀𝑣 ∈
(Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘) ↔ (𝐾 ∈ ℕ0*
∧ ∀𝑣 ∈
(Vtx‘𝐺)((VtxDeg‘𝐺)‘𝑣) = 𝐾))) |
12 | | df-rgr 27935 |
. . 3
⊢ RegGraph
= {〈𝑔, 𝑘〉 ∣ (𝑘 ∈
ℕ0* ∧ ∀𝑣 ∈ (Vtx‘𝑔)((VtxDeg‘𝑔)‘𝑣) = 𝑘)} |
13 | 11, 12 | brabga 5450 |
. 2
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegGraph 𝐾 ↔ (𝐾 ∈ ℕ0*
∧ ∀𝑣 ∈
(Vtx‘𝐺)((VtxDeg‘𝐺)‘𝑣) = 𝐾))) |
14 | | isrgr.v |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
15 | | isrgr.d |
. . . . . . . 8
⊢ 𝐷 = (VtxDeg‘𝐺) |
16 | 15 | fveq1i 6772 |
. . . . . . 7
⊢ (𝐷‘𝑣) = ((VtxDeg‘𝐺)‘𝑣) |
17 | 16 | eqeq1i 2745 |
. . . . . 6
⊢ ((𝐷‘𝑣) = 𝐾 ↔ ((VtxDeg‘𝐺)‘𝑣) = 𝐾) |
18 | 14, 17 | raleqbii 3163 |
. . . . 5
⊢
(∀𝑣 ∈
𝑉 (𝐷‘𝑣) = 𝐾 ↔ ∀𝑣 ∈ (Vtx‘𝐺)((VtxDeg‘𝐺)‘𝑣) = 𝐾) |
19 | 18 | bicomi 223 |
. . . 4
⊢
(∀𝑣 ∈
(Vtx‘𝐺)((VtxDeg‘𝐺)‘𝑣) = 𝐾 ↔ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾) |
20 | 19 | a1i 11 |
. . 3
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (∀𝑣 ∈ (Vtx‘𝐺)((VtxDeg‘𝐺)‘𝑣) = 𝐾 ↔ ∀𝑣 ∈ 𝑉 (𝐷‘𝑣) = 𝐾)) |
21 | 20 | anbi2d 629 |
. 2
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → ((𝐾 ∈ ℕ0*
∧ ∀𝑣 ∈
(Vtx‘𝐺)((VtxDeg‘𝐺)‘𝑣) = 𝐾) ↔ (𝐾 ∈ ℕ0*
∧ ∀𝑣 ∈
𝑉 (𝐷‘𝑣) = 𝐾))) |
22 | 13, 21 | bitrd 278 |
1
⊢ ((𝐺 ∈ 𝑊 ∧ 𝐾 ∈ 𝑍) → (𝐺 RegGraph 𝐾 ↔ (𝐾 ∈ ℕ0*
∧ ∀𝑣 ∈
𝑉 (𝐷‘𝑣) = 𝐾))) |