Step | Hyp | Ref
| Expression |
1 | | df-uhgr 25724 |
. . 3
⊢ UHGraph
= {𝑔 ∣
[(Vtx‘𝑔) /
𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})} |
2 | 1 | eleq2i 2680 |
. 2
⊢ (𝐺 ∈ UHGraph ↔ 𝐺 ∈ {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})}) |
3 | | fveq2 6103 |
. . . . 5
⊢ (ℎ = 𝐺 → (iEdg‘ℎ) = (iEdg‘𝐺)) |
4 | | isuhgr.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 |
. . . . . . 7
⊢ (ℎ = 𝐺 → (Vtx‘ℎ) = (Vtx‘𝐺)) |
11 | | isuhgr.v |
. . . . . . 7
⊢ 𝑉 = (Vtx‘𝐺) |
12 | 10, 11 | syl6eqr 2662 |
. . . . . 6
⊢ (ℎ = 𝐺 → (Vtx‘ℎ) = 𝑉) |
13 | 12 | pweqd 4113 |
. . . . 5
⊢ (ℎ = 𝐺 → 𝒫 (Vtx‘ℎ) = 𝒫 𝑉) |
14 | 13 | difeq1d 3689 |
. . . 4
⊢ (ℎ = 𝐺 → (𝒫 (Vtx‘ℎ) ∖ {∅}) = (𝒫
𝑉 ∖
{∅})) |
15 | 5, 9, 14 | feq123d 5947 |
. . 3
⊢ (ℎ = 𝐺 → ((iEdg‘ℎ):dom (iEdg‘ℎ)⟶(𝒫 (Vtx‘ℎ) ∖ {∅}) ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) |
16 | | fvex 6113 |
. . . . . 6
⊢
(Vtx‘𝑔) ∈
V |
17 | 16 | a1i 11 |
. . . . 5
⊢ (𝑔 = ℎ → (Vtx‘𝑔) ∈ V) |
18 | | fveq2 6103 |
. . . . 5
⊢ (𝑔 = ℎ → (Vtx‘𝑔) = (Vtx‘ℎ)) |
19 | | fvex 6113 |
. . . . . . 7
⊢
(iEdg‘𝑔)
∈ V |
20 | 19 | a1i 11 |
. . . . . 6
⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → (iEdg‘𝑔) ∈ V) |
21 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑔 = ℎ → (iEdg‘𝑔) = (iEdg‘ℎ)) |
22 | 21 | adantr 480 |
. . . . . 6
⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → (iEdg‘𝑔) = (iEdg‘ℎ)) |
23 | | simpr 476 |
. . . . . . 7
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (iEdg‘ℎ)) → 𝑒 = (iEdg‘ℎ)) |
24 | 23 | dmeqd 5248 |
. . . . . . 7
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (iEdg‘ℎ)) → dom 𝑒 = dom (iEdg‘ℎ)) |
25 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → 𝑣 = (Vtx‘ℎ)) |
26 | 25 | pweqd 4113 |
. . . . . . . . 9
⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → 𝒫 𝑣 = 𝒫 (Vtx‘ℎ)) |
27 | 26 | difeq1d 3689 |
. . . . . . . 8
⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → (𝒫 𝑣 ∖ {∅}) = (𝒫
(Vtx‘ℎ) ∖
{∅})) |
28 | 27 | adantr 480 |
. . . . . . 7
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (iEdg‘ℎ)) → (𝒫 𝑣 ∖ {∅}) = (𝒫
(Vtx‘ℎ) ∖
{∅})) |
29 | 23, 24, 28 | feq123d 5947 |
. . . . . 6
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (iEdg‘ℎ)) → (𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅}) ↔ (iEdg‘ℎ):dom (iEdg‘ℎ)⟶(𝒫
(Vtx‘ℎ) ∖
{∅}))) |
30 | 20, 22, 29 | sbcied2 3440 |
. . . . 5
⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → ([(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅}) ↔ (iEdg‘ℎ):dom (iEdg‘ℎ)⟶(𝒫
(Vtx‘ℎ) ∖
{∅}))) |
31 | 17, 18, 30 | sbcied2 3440 |
. . . 4
⊢ (𝑔 = ℎ → ([(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅}) ↔ (iEdg‘ℎ):dom (iEdg‘ℎ)⟶(𝒫
(Vtx‘ℎ) ∖
{∅}))) |
32 | 31 | cbvabv 2734 |
. . 3
⊢ {𝑔 ∣
[(Vtx‘𝑔) /
𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})} = {ℎ ∣ (iEdg‘ℎ):dom (iEdg‘ℎ)⟶(𝒫 (Vtx‘ℎ) ∖
{∅})} |
33 | 15, 32 | elab2g 3322 |
. 2
⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒⟶(𝒫 𝑣 ∖ {∅})} ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) |
34 | 2, 33 | syl5bb 271 |
1
⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ UHGraph ↔ 𝐸:dom 𝐸⟶(𝒫 𝑉 ∖ {∅}))) |