| Step | Hyp | Ref
| Expression |
| 1 | | upgrun.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ UPGraph) |
| 2 | | upgrun.vg |
. . . . . 6
⊢ 𝑉 = (Vtx‘𝐺) |
| 3 | | upgrun.e |
. . . . . 6
⊢ 𝐸 = (iEdg‘𝐺) |
| 4 | 2, 3 | upgrf 29103 |
. . . . 5
⊢ (𝐺 ∈ UPGraph → 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
| 5 | 1, 4 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
| 6 | | upgrun.h |
. . . . . 6
⊢ (𝜑 → 𝐻 ∈ UPGraph) |
| 7 | | eqid 2737 |
. . . . . . 7
⊢
(Vtx‘𝐻) =
(Vtx‘𝐻) |
| 8 | | upgrun.f |
. . . . . . 7
⊢ 𝐹 = (iEdg‘𝐻) |
| 9 | 7, 8 | upgrf 29103 |
. . . . . 6
⊢ (𝐻 ∈ UPGraph → 𝐹:dom 𝐹⟶{𝑥 ∈ (𝒫 (Vtx‘𝐻) ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
| 10 | 6, 9 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐹:dom 𝐹⟶{𝑥 ∈ (𝒫 (Vtx‘𝐻) ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
| 11 | | upgrun.vh |
. . . . . . . . . 10
⊢ (𝜑 → (Vtx‘𝐻) = 𝑉) |
| 12 | 11 | eqcomd 2743 |
. . . . . . . . 9
⊢ (𝜑 → 𝑉 = (Vtx‘𝐻)) |
| 13 | 12 | pweqd 4617 |
. . . . . . . 8
⊢ (𝜑 → 𝒫 𝑉 = 𝒫 (Vtx‘𝐻)) |
| 14 | 13 | difeq1d 4125 |
. . . . . . 7
⊢ (𝜑 → (𝒫 𝑉 ∖ {∅}) = (𝒫
(Vtx‘𝐻) ∖
{∅})) |
| 15 | 14 | rabeqdv 3452 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2} =
{𝑥 ∈ (𝒫
(Vtx‘𝐻) ∖
{∅}) ∣ (♯‘𝑥) ≤ 2}) |
| 16 | 15 | feq3d 6723 |
. . . . 5
⊢ (𝜑 → (𝐹:dom 𝐹⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
↔ 𝐹:dom 𝐹⟶{𝑥 ∈ (𝒫 (Vtx‘𝐻) ∖ {∅}) ∣
(♯‘𝑥) ≤
2})) |
| 17 | 10, 16 | mpbird 257 |
. . . 4
⊢ (𝜑 → 𝐹:dom 𝐹⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
| 18 | | upgrun.i |
. . . 4
⊢ (𝜑 → (dom 𝐸 ∩ dom 𝐹) = ∅) |
| 19 | 5, 17, 18 | fun2d 6772 |
. . 3
⊢ (𝜑 → (𝐸 ∪ 𝐹):(dom 𝐸 ∪ dom 𝐹)⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
| 20 | | upgrun.un |
. . . 4
⊢ (𝜑 → (iEdg‘𝑈) = (𝐸 ∪ 𝐹)) |
| 21 | 20 | dmeqd 5916 |
. . . . 5
⊢ (𝜑 → dom (iEdg‘𝑈) = dom (𝐸 ∪ 𝐹)) |
| 22 | | dmun 5921 |
. . . . 5
⊢ dom
(𝐸 ∪ 𝐹) = (dom 𝐸 ∪ dom 𝐹) |
| 23 | 21, 22 | eqtrdi 2793 |
. . . 4
⊢ (𝜑 → dom (iEdg‘𝑈) = (dom 𝐸 ∪ dom 𝐹)) |
| 24 | | upgrun.v |
. . . . . . 7
⊢ (𝜑 → (Vtx‘𝑈) = 𝑉) |
| 25 | 24 | pweqd 4617 |
. . . . . 6
⊢ (𝜑 → 𝒫 (Vtx‘𝑈) = 𝒫 𝑉) |
| 26 | 25 | difeq1d 4125 |
. . . . 5
⊢ (𝜑 → (𝒫
(Vtx‘𝑈) ∖
{∅}) = (𝒫 𝑉
∖ {∅})) |
| 27 | 26 | rabeqdv 3452 |
. . . 4
⊢ (𝜑 → {𝑥 ∈ (𝒫 (Vtx‘𝑈) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2} =
{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
| 28 | 20, 23, 27 | feq123d 6725 |
. . 3
⊢ (𝜑 → ((iEdg‘𝑈):dom (iEdg‘𝑈)⟶{𝑥 ∈ (𝒫 (Vtx‘𝑈) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
↔ (𝐸 ∪ 𝐹):(dom 𝐸 ∪ dom 𝐹)⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤
2})) |
| 29 | 19, 28 | mpbird 257 |
. 2
⊢ (𝜑 → (iEdg‘𝑈):dom (iEdg‘𝑈)⟶{𝑥 ∈ (𝒫 (Vtx‘𝑈) ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
| 30 | | upgrun.u |
. . 3
⊢ (𝜑 → 𝑈 ∈ 𝑊) |
| 31 | | eqid 2737 |
. . . 4
⊢
(Vtx‘𝑈) =
(Vtx‘𝑈) |
| 32 | | eqid 2737 |
. . . 4
⊢
(iEdg‘𝑈) =
(iEdg‘𝑈) |
| 33 | 31, 32 | isupgr 29101 |
. . 3
⊢ (𝑈 ∈ 𝑊 → (𝑈 ∈ UPGraph ↔ (iEdg‘𝑈):dom (iEdg‘𝑈)⟶{𝑥 ∈ (𝒫 (Vtx‘𝑈) ∖ {∅}) ∣
(♯‘𝑥) ≤
2})) |
| 34 | 30, 33 | syl 17 |
. 2
⊢ (𝜑 → (𝑈 ∈ UPGraph ↔ (iEdg‘𝑈):dom (iEdg‘𝑈)⟶{𝑥 ∈ (𝒫 (Vtx‘𝑈) ∖ {∅}) ∣
(♯‘𝑥) ≤
2})) |
| 35 | 29, 34 | mpbird 257 |
1
⊢ (𝜑 → 𝑈 ∈ UPGraph) |