Step | Hyp | Ref
| Expression |
1 | | df-upgr 25749 |
. . 3
⊢ UPGraph
= {𝑔 ∣
[(Vtx‘𝑔) /
𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}} |
2 | 1 | eleq2i 2680 |
. 2
⊢ (𝐺 ∈ UPGraph ↔ 𝐺 ∈ {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}}) |
3 | | fveq2 6103 |
. . . . 5
⊢ (ℎ = 𝐺 → (iEdg‘ℎ) = (iEdg‘𝐺)) |
4 | | isupgr.e |
. . . . 5
⊢ 𝐸 = (iEdg‘𝐺) |
5 | 3, 4 | syl6eqr 2662 |
. . . 4
⊢ (ℎ = 𝐺 → (iEdg‘ℎ) = 𝐸) |
6 | 3 | dmeqd 5248 |
. . . . 5
⊢ (ℎ = 𝐺 → dom (iEdg‘ℎ) = dom (iEdg‘𝐺)) |
7 | 4 | eqcomi 2619 |
. . . . . 6
⊢
(iEdg‘𝐺) =
𝐸 |
8 | 7 | dmeqi 5247 |
. . . . 5
⊢ dom
(iEdg‘𝐺) = dom 𝐸 |
9 | 6, 8 | syl6eq 2660 |
. . . 4
⊢ (ℎ = 𝐺 → dom (iEdg‘ℎ) = dom 𝐸) |
10 | | fveq2 6103 |
. . . . . . . 8
⊢ (ℎ = 𝐺 → (Vtx‘ℎ) = (Vtx‘𝐺)) |
11 | | isupgr.v |
. . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐺) |
12 | 10, 11 | syl6eqr 2662 |
. . . . . . 7
⊢ (ℎ = 𝐺 → (Vtx‘ℎ) = 𝑉) |
13 | 12 | pweqd 4113 |
. . . . . 6
⊢ (ℎ = 𝐺 → 𝒫 (Vtx‘ℎ) = 𝒫 𝑉) |
14 | 13 | difeq1d 3689 |
. . . . 5
⊢ (ℎ = 𝐺 → (𝒫 (Vtx‘ℎ) ∖ {∅}) = (𝒫
𝑉 ∖
{∅})) |
15 | 14 | rabeqdv 3167 |
. . . 4
⊢ (ℎ = 𝐺 → {𝑥 ∈ (𝒫 (Vtx‘ℎ) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} =
{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
16 | 5, 9, 15 | feq123d 5947 |
. . 3
⊢ (ℎ = 𝐺 → ((iEdg‘ℎ):dom (iEdg‘ℎ)⟶{𝑥 ∈ (𝒫 (Vtx‘ℎ) ∖ {∅}) ∣
(#‘𝑥) ≤ 2} ↔
𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})) |
17 | | fvex 6113 |
. . . . . 6
⊢
(Vtx‘𝑔) ∈
V |
18 | 17 | a1i 11 |
. . . . 5
⊢ (𝑔 = ℎ → (Vtx‘𝑔) ∈ V) |
19 | | fveq2 6103 |
. . . . 5
⊢ (𝑔 = ℎ → (Vtx‘𝑔) = (Vtx‘ℎ)) |
20 | | fvex 6113 |
. . . . . . 7
⊢
(iEdg‘𝑔)
∈ V |
21 | 20 | a1i 11 |
. . . . . 6
⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → (iEdg‘𝑔) ∈ V) |
22 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑔 = ℎ → (iEdg‘𝑔) = (iEdg‘ℎ)) |
23 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → (iEdg‘𝑔) = (iEdg‘ℎ)) |
24 | | simpr 476 |
. . . . . . 7
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (iEdg‘ℎ)) → 𝑒 = (iEdg‘ℎ)) |
25 | 24 | dmeqd 5248 |
. . . . . . 7
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (iEdg‘ℎ)) → dom 𝑒 = dom (iEdg‘ℎ)) |
26 | | pweq 4111 |
. . . . . . . . . 10
⊢ (𝑣 = (Vtx‘ℎ) → 𝒫 𝑣 = 𝒫 (Vtx‘ℎ)) |
27 | 26 | ad2antlr 759 |
. . . . . . . . 9
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (iEdg‘ℎ)) → 𝒫 𝑣 = 𝒫 (Vtx‘ℎ)) |
28 | 27 | difeq1d 3689 |
. . . . . . . 8
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (iEdg‘ℎ)) → (𝒫 𝑣 ∖ {∅}) = (𝒫
(Vtx‘ℎ) ∖
{∅})) |
29 | 28 | rabeqdv 3167 |
. . . . . . 7
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (iEdg‘ℎ)) → {𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} = {𝑥 ∈ (𝒫 (Vtx‘ℎ) ∖ {∅}) ∣
(#‘𝑥) ≤
2}) |
30 | 24, 25, 29 | feq123d 5947 |
. . . . . 6
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (iEdg‘ℎ)) → (𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} ↔
(iEdg‘ℎ):dom
(iEdg‘ℎ)⟶{𝑥 ∈ (𝒫
(Vtx‘ℎ) ∖
{∅}) ∣ (#‘𝑥) ≤ 2})) |
31 | 21, 23, 30 | sbcied2 3440 |
. . . . 5
⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → ([(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} ↔
(iEdg‘ℎ):dom
(iEdg‘ℎ)⟶{𝑥 ∈ (𝒫
(Vtx‘ℎ) ∖
{∅}) ∣ (#‘𝑥) ≤ 2})) |
32 | 18, 19, 31 | sbcied2 3440 |
. . . 4
⊢ (𝑔 = ℎ → ([(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} ↔
(iEdg‘ℎ):dom
(iEdg‘ℎ)⟶{𝑥 ∈ (𝒫
(Vtx‘ℎ) ∖
{∅}) ∣ (#‘𝑥) ≤ 2})) |
33 | 32 | cbvabv 2734 |
. . 3
⊢ {𝑔 ∣
[(Vtx‘𝑔) /
𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}} = {ℎ ∣ (iEdg‘ℎ):dom (iEdg‘ℎ)⟶{𝑥 ∈ (𝒫 (Vtx‘ℎ) ∖ {∅}) ∣
(#‘𝑥) ≤
2}} |
34 | 16, 33 | elab2g 3322 |
. 2
⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣ (#‘𝑥) ≤ 2}} ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})) |
35 | 2, 34 | syl5bb 271 |
1
⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UPGraph ↔ 𝐸:dom 𝐸⟶{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2})) |