Step | Hyp | Ref
| Expression |
1 | | df-br 4584 |
. . . . 5
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 ↔ 〈〈𝑉, 𝐸〉, 𝐾〉 ∈ RegUSGrph ) |
2 | | df-rusgra 26452 |
. . . . . 6
⊢
RegUSGrph = {〈〈𝑣,
𝑒〉, 𝑘〉 ∣ (𝑣 USGrph 𝑒 ∧ 〈𝑣, 𝑒〉 RegGrph 𝑘)} |
3 | 2 | eleq2i 2680 |
. . . . 5
⊢
(〈〈𝑉,
𝐸〉, 𝐾〉 ∈ RegUSGrph ↔
〈〈𝑉, 𝐸〉, 𝐾〉 ∈ {〈〈𝑣, 𝑒〉, 𝑘〉 ∣ (𝑣 USGrph 𝑒 ∧ 〈𝑣, 𝑒〉 RegGrph 𝑘)}) |
4 | 1, 3 | bitri 263 |
. . . 4
⊢
(〈𝑉, 𝐸〉 RegUSGrph 𝐾 ↔ 〈〈𝑉, 𝐸〉, 𝐾〉 ∈ {〈〈𝑣, 𝑒〉, 𝑘〉 ∣ (𝑣 USGrph 𝑒 ∧ 〈𝑣, 𝑒〉 RegGrph 𝑘)}) |
5 | | breq12 4588 |
. . . . . . 7
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → (𝑣 USGrph 𝑒 ↔ 𝑉 USGrph 𝐸)) |
6 | 5 | 3adant3 1074 |
. . . . . 6
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ∧ 𝑘 = 𝐾) → (𝑣 USGrph 𝑒 ↔ 𝑉 USGrph 𝐸)) |
7 | | opeq12 4342 |
. . . . . . . 8
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸) → 〈𝑣, 𝑒〉 = 〈𝑉, 𝐸〉) |
8 | 7 | 3adant3 1074 |
. . . . . . 7
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ∧ 𝑘 = 𝐾) → 〈𝑣, 𝑒〉 = 〈𝑉, 𝐸〉) |
9 | | simp3 1056 |
. . . . . . 7
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ∧ 𝑘 = 𝐾) → 𝑘 = 𝐾) |
10 | 8, 9 | breq12d 4596 |
. . . . . 6
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ∧ 𝑘 = 𝐾) → (〈𝑣, 𝑒〉 RegGrph 𝑘 ↔ 〈𝑉, 𝐸〉 RegGrph 𝐾)) |
11 | 6, 10 | anbi12d 743 |
. . . . 5
⊢ ((𝑣 = 𝑉 ∧ 𝑒 = 𝐸 ∧ 𝑘 = 𝐾) → ((𝑣 USGrph 𝑒 ∧ 〈𝑣, 𝑒〉 RegGrph 𝑘) ↔ (𝑉 USGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegGrph 𝐾))) |
12 | 11 | eloprabga 6645 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐾 ∈ 𝑍) → (〈〈𝑉, 𝐸〉, 𝐾〉 ∈ {〈〈𝑣, 𝑒〉, 𝑘〉 ∣ (𝑣 USGrph 𝑒 ∧ 〈𝑣, 𝑒〉 RegGrph 𝑘)} ↔ (𝑉 USGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegGrph 𝐾))) |
13 | 4, 12 | syl5bb 271 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐾 ∈ 𝑍) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 ↔ (𝑉 USGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegGrph 𝐾))) |
14 | | isrgra 26453 |
. . . 4
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐾 ∈ 𝑍) → (〈𝑉, 𝐸〉 RegGrph 𝐾 ↔ (𝐾 ∈ ℕ0 ∧
∀𝑝 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾))) |
15 | 14 | anbi2d 736 |
. . 3
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐾 ∈ 𝑍) → ((𝑉 USGrph 𝐸 ∧ 〈𝑉, 𝐸〉 RegGrph 𝐾) ↔ (𝑉 USGrph 𝐸 ∧ (𝐾 ∈ ℕ0 ∧
∀𝑝 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾)))) |
16 | 13, 15 | bitrd 267 |
. 2
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐾 ∈ 𝑍) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 ↔ (𝑉 USGrph 𝐸 ∧ (𝐾 ∈ ℕ0 ∧
∀𝑝 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾)))) |
17 | | 3anass 1035 |
. 2
⊢ ((𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑝 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾) ↔ (𝑉 USGrph 𝐸 ∧ (𝐾 ∈ ℕ0 ∧
∀𝑝 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾))) |
18 | 16, 17 | syl6bbr 277 |
1
⊢ ((𝑉 ∈ 𝑋 ∧ 𝐸 ∈ 𝑌 ∧ 𝐾 ∈ 𝑍) → (〈𝑉, 𝐸〉 RegUSGrph 𝐾 ↔ (𝑉 USGrph 𝐸 ∧ 𝐾 ∈ ℕ0 ∧
∀𝑝 ∈ 𝑉 ((𝑉 VDeg 𝐸)‘𝑝) = 𝐾))) |