Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . 3
⊢
(Vtx‘𝐺) =
(Vtx‘𝐺) |
2 | | eqid 2733 |
. . 3
⊢
(iEdg‘𝐺) =
(iEdg‘𝐺) |
3 | 1, 2 | upgrf 28346 |
. 2
⊢ (𝐺 ∈ UPGraph →
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑝 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑝) ≤
2}) |
4 | | fvex 6905 |
. . . 4
⊢
(Vtx‘𝐺) ∈
V |
5 | | fvex 6905 |
. . . 4
⊢
(iEdg‘𝐺)
∈ V |
6 | 4, 5 | pm3.2i 472 |
. . 3
⊢
((Vtx‘𝐺)
∈ V ∧ (iEdg‘𝐺) ∈ V) |
7 | | opex 5465 |
. . . . 5
⊢
⟨(Vtx‘𝐺),
(iEdg‘𝐺)⟩ ∈
V |
8 | | eqid 2733 |
. . . . . 6
⊢
(Vtx‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩) = (Vtx‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩) |
9 | | eqid 2733 |
. . . . . 6
⊢
(iEdg‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩) =
(iEdg‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩) |
10 | 8, 9 | isupgr 28344 |
. . . . 5
⊢
(⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ∈ V →
(⟨(Vtx‘𝐺),
(iEdg‘𝐺)⟩ ∈
UPGraph ↔ (iEdg‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩):dom
(iEdg‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩)⟶{𝑝 ∈ (𝒫
(Vtx‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩) ∖ {∅}) ∣
(♯‘𝑝) ≤
2})) |
11 | 7, 10 | mp1i 13 |
. . . 4
⊢
(((Vtx‘𝐺)
∈ V ∧ (iEdg‘𝐺) ∈ V) → (⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ∈ UPGraph ↔
(iEdg‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩):dom
(iEdg‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩)⟶{𝑝 ∈ (𝒫
(Vtx‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩) ∖ {∅}) ∣
(♯‘𝑝) ≤
2})) |
12 | | opiedgfv 28267 |
. . . . 5
⊢
(((Vtx‘𝐺)
∈ V ∧ (iEdg‘𝐺) ∈ V) →
(iEdg‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩) = (iEdg‘𝐺)) |
13 | 12 | dmeqd 5906 |
. . . . 5
⊢
(((Vtx‘𝐺)
∈ V ∧ (iEdg‘𝐺) ∈ V) → dom
(iEdg‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩) = dom (iEdg‘𝐺)) |
14 | | opvtxfv 28264 |
. . . . . . . 8
⊢
(((Vtx‘𝐺)
∈ V ∧ (iEdg‘𝐺) ∈ V) →
(Vtx‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩) = (Vtx‘𝐺)) |
15 | 14 | pweqd 4620 |
. . . . . . 7
⊢
(((Vtx‘𝐺)
∈ V ∧ (iEdg‘𝐺) ∈ V) → 𝒫
(Vtx‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩) = 𝒫 (Vtx‘𝐺)) |
16 | 15 | difeq1d 4122 |
. . . . . 6
⊢
(((Vtx‘𝐺)
∈ V ∧ (iEdg‘𝐺) ∈ V) → (𝒫
(Vtx‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩) ∖ {∅}) = (𝒫
(Vtx‘𝐺) ∖
{∅})) |
17 | 16 | rabeqdv 3448 |
. . . . 5
⊢
(((Vtx‘𝐺)
∈ V ∧ (iEdg‘𝐺) ∈ V) → {𝑝 ∈ (𝒫
(Vtx‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩) ∖ {∅}) ∣
(♯‘𝑝) ≤ 2} =
{𝑝 ∈ (𝒫
(Vtx‘𝐺) ∖
{∅}) ∣ (♯‘𝑝) ≤ 2}) |
18 | 12, 13, 17 | feq123d 6707 |
. . . 4
⊢
(((Vtx‘𝐺)
∈ V ∧ (iEdg‘𝐺) ∈ V) →
((iEdg‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩):dom
(iEdg‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩)⟶{𝑝 ∈ (𝒫
(Vtx‘⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩) ∖ {∅}) ∣
(♯‘𝑝) ≤ 2}
↔ (iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑝 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑝) ≤
2})) |
19 | 11, 18 | bitrd 279 |
. . 3
⊢
(((Vtx‘𝐺)
∈ V ∧ (iEdg‘𝐺) ∈ V) → (⟨(Vtx‘𝐺), (iEdg‘𝐺)⟩ ∈ UPGraph ↔
(iEdg‘𝐺):dom
(iEdg‘𝐺)⟶{𝑝 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑝) ≤
2})) |
20 | 6, 19 | mp1i 13 |
. 2
⊢ (𝐺 ∈ UPGraph →
(⟨(Vtx‘𝐺),
(iEdg‘𝐺)⟩ ∈
UPGraph ↔ (iEdg‘𝐺):dom (iEdg‘𝐺)⟶{𝑝 ∈ (𝒫 (Vtx‘𝐺) ∖ {∅}) ∣
(♯‘𝑝) ≤
2})) |
21 | 3, 20 | mpbird 257 |
1
⊢ (𝐺 ∈ UPGraph →
⟨(Vtx‘𝐺),
(iEdg‘𝐺)⟩ ∈
UPGraph) |