Step | Hyp | Ref
| Expression |
1 | | df-br 4584 |
. 2
⊢
(〈𝑉, 𝐸〉 RegGrph 𝐾 ↔ 〈〈𝑉, 𝐸〉, 𝐾〉 ∈ RegGrph ) |
2 | | df-rgra 26451 |
. . . 4
⊢ RegGrph
= {〈〈𝑣, 𝑒〉, 𝑘〉 ∣ (𝑘 ∈ ℕ0 ∧
∀𝑝 ∈ 𝑣 ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘)} |
3 | 2 | eleq2i 2680 |
. . 3
⊢
(〈〈𝑉,
𝐸〉, 𝐾〉 ∈ RegGrph ↔
〈〈𝑉, 𝐸〉, 𝐾〉 ∈ {〈〈𝑣, 𝑒〉, 𝑘〉 ∣ (𝑘 ∈ ℕ0 ∧
∀𝑝 ∈ 𝑣 ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘)}) |
4 | | eleq1 2676 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (𝑘 ∈ ℕ0 ↔ 𝐾 ∈
ℕ0)) |
5 | 4 | 3ad2ant3 1077 |
. . . . 5
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ∧ 𝑘 = 𝐾) → (𝑘 ∈ ℕ0 ↔ 𝐾 ∈
ℕ0)) |
6 | | simp1 1054 |
. . . . . 6
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ∧ 𝑘 = 𝐾) → 𝑣 = 𝑉) |
7 | | oveq12 6558 |
. . . . . . . . 9
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑣 VDeg 𝑒) = (𝑉 VDeg 𝐸)) |
8 | 7 | fveq1d 6105 |
. . . . . . . 8
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → ((𝑣 VDeg 𝑒)‘𝑝) = ((𝑉 VDeg 𝐸)‘𝑝)) |
9 | 8 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ∧ 𝑘 = 𝐾) → ((𝑣 VDeg 𝑒)‘𝑝) = ((𝑉 VDeg 𝐸)‘𝑝)) |
10 | | simp3 1056 |
. . . . . . 7
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ∧ 𝑘 = 𝐾) → 𝑘 = 𝐾) |
11 | 9, 10 | eqeq12d 2625 |
. . . . . 6
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ∧ 𝑘 = 𝐾) → (((𝑣 VDeg 𝑒)‘𝑝) = 𝑘 ↔ ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾)) |
12 | 6, 11 | raleqbidv 3129 |
. . . . 5
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ∧ 𝑘 = 𝐾) → (∀𝑝 ∈ 𝑣 ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘 ↔ ∀𝑝 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾)) |
13 | 5, 12 | anbi12d 743 |
. . . 4
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ∧ 𝑘 = 𝐾) → ((𝑘 ∈ ℕ0 ∧
∀𝑝 ∈ 𝑣 ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘) ↔ (𝐾 ∈ ℕ0 ∧
∀𝑝 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾))) |
14 | 13 | eloprabga 6645 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐾 ∈ 𝑍) → (〈〈𝑉, 𝐸〉, 𝐾〉 ∈ {〈〈𝑣, 𝑒〉, 𝑘〉 ∣ (𝑘 ∈ ℕ0 ∧
∀𝑝 ∈ 𝑣 ((𝑣 VDeg 𝑒)‘𝑝) = 𝑘)} ↔ (𝐾 ∈ ℕ0 ∧
∀𝑝 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾))) |
15 | 3, 14 | syl5bb 271 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐾 ∈ 𝑍) → (〈〈𝑉, 𝐸〉, 𝐾〉 ∈ RegGrph ↔ (𝐾 ∈ ℕ0
∧ ∀𝑝 ∈
𝑉 ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾))) |
16 | 1, 15 | syl5bb 271 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐾 ∈ 𝑍) → (〈𝑉, 𝐸〉 RegGrph 𝐾 ↔ (𝐾 ∈ ℕ0 ∧
∀𝑝 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾))) |