Step | Hyp | Ref
| Expression |
1 | | df-uspgr 27241 |
. . 3
⊢ USPGraph
= {𝑔 ∣
[(Vtx‘𝑔) /
𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) ≤
2}} |
2 | 1 | eleq2i 2829 |
. 2
⊢ (𝐺 ∈ USPGraph ↔ 𝐺 ∈ {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) ≤
2}}) |
3 | | fveq2 6717 |
. . . . 5
⊢ (ℎ = 𝐺 → (iEdg‘ℎ) = (iEdg‘𝐺)) |
4 | | isuspgr.e |
. . . . 5
⊢ 𝐸 = (iEdg‘𝐺) |
5 | 3, 4 | eqtr4di 2796 |
. . . 4
⊢ (ℎ = 𝐺 → (iEdg‘ℎ) = 𝐸) |
6 | 3 | dmeqd 5774 |
. . . . 5
⊢ (ℎ = 𝐺 → dom (iEdg‘ℎ) = dom (iEdg‘𝐺)) |
7 | 4 | eqcomi 2746 |
. . . . . 6
⊢
(iEdg‘𝐺) =
𝐸 |
8 | 7 | dmeqi 5773 |
. . . . 5
⊢ dom
(iEdg‘𝐺) = dom 𝐸 |
9 | 6, 8 | eqtrdi 2794 |
. . . 4
⊢ (ℎ = 𝐺 → dom (iEdg‘ℎ) = dom 𝐸) |
10 | | fveq2 6717 |
. . . . . . . 8
⊢ (ℎ = 𝐺 → (Vtx‘ℎ) = (Vtx‘𝐺)) |
11 | | isuspgr.v |
. . . . . . . 8
⊢ 𝑉 = (Vtx‘𝐺) |
12 | 10, 11 | eqtr4di 2796 |
. . . . . . 7
⊢ (ℎ = 𝐺 → (Vtx‘ℎ) = 𝑉) |
13 | 12 | pweqd 4532 |
. . . . . 6
⊢ (ℎ = 𝐺 → 𝒫 (Vtx‘ℎ) = 𝒫 𝑉) |
14 | 13 | difeq1d 4036 |
. . . . 5
⊢ (ℎ = 𝐺 → (𝒫 (Vtx‘ℎ) ∖ {∅}) = (𝒫
𝑉 ∖
{∅})) |
15 | 14 | rabeqdv 3395 |
. . . 4
⊢ (ℎ = 𝐺 → {𝑥 ∈ (𝒫 (Vtx‘ℎ) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2} =
{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤
2}) |
16 | 5, 9, 15 | f1eq123d 6653 |
. . 3
⊢ (ℎ = 𝐺 → ((iEdg‘ℎ):dom (iEdg‘ℎ)–1-1→{𝑥 ∈ (𝒫 (Vtx‘ℎ) ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤
2})) |
17 | | fvexd 6732 |
. . . . 5
⊢ (𝑔 = ℎ → (Vtx‘𝑔) ∈ V) |
18 | | fveq2 6717 |
. . . . 5
⊢ (𝑔 = ℎ → (Vtx‘𝑔) = (Vtx‘ℎ)) |
19 | | fvexd 6732 |
. . . . . 6
⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → (iEdg‘𝑔) ∈ V) |
20 | | fveq2 6717 |
. . . . . . 7
⊢ (𝑔 = ℎ → (iEdg‘𝑔) = (iEdg‘ℎ)) |
21 | 20 | adantr 484 |
. . . . . 6
⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → (iEdg‘𝑔) = (iEdg‘ℎ)) |
22 | | simpr 488 |
. . . . . . 7
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (iEdg‘ℎ)) → 𝑒 = (iEdg‘ℎ)) |
23 | 22 | dmeqd 5774 |
. . . . . . 7
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (iEdg‘ℎ)) → dom 𝑒 = dom (iEdg‘ℎ)) |
24 | | pweq 4529 |
. . . . . . . . . 10
⊢ (𝑣 = (Vtx‘ℎ) → 𝒫 𝑣 = 𝒫 (Vtx‘ℎ)) |
25 | 24 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (iEdg‘ℎ)) → 𝒫 𝑣 = 𝒫 (Vtx‘ℎ)) |
26 | 25 | difeq1d 4036 |
. . . . . . . 8
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (iEdg‘ℎ)) → (𝒫 𝑣 ∖ {∅}) = (𝒫
(Vtx‘ℎ) ∖
{∅})) |
27 | 26 | rabeqdv 3395 |
. . . . . . 7
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (iEdg‘ℎ)) → {𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2} =
{𝑥 ∈ (𝒫
(Vtx‘ℎ) ∖
{∅}) ∣ (♯‘𝑥) ≤ 2}) |
28 | 22, 23, 27 | f1eq123d 6653 |
. . . . . 6
⊢ (((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) ∧ 𝑒 = (iEdg‘ℎ)) → (𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
↔ (iEdg‘ℎ):dom
(iEdg‘ℎ)–1-1→{𝑥 ∈ (𝒫 (Vtx‘ℎ) ∖ {∅}) ∣
(♯‘𝑥) ≤
2})) |
29 | 19, 21, 28 | sbcied2 3741 |
. . . . 5
⊢ ((𝑔 = ℎ ∧ 𝑣 = (Vtx‘ℎ)) → ([(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
↔ (iEdg‘ℎ):dom
(iEdg‘ℎ)–1-1→{𝑥 ∈ (𝒫 (Vtx‘ℎ) ∖ {∅}) ∣
(♯‘𝑥) ≤
2})) |
30 | 17, 18, 29 | sbcied2 3741 |
. . . 4
⊢ (𝑔 = ℎ → ([(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
↔ (iEdg‘ℎ):dom
(iEdg‘ℎ)–1-1→{𝑥 ∈ (𝒫 (Vtx‘ℎ) ∖ {∅}) ∣
(♯‘𝑥) ≤
2})) |
31 | 30 | cbvabv 2811 |
. . 3
⊢ {𝑔 ∣
[(Vtx‘𝑔) /
𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}}
= {ℎ ∣
(iEdg‘ℎ):dom
(iEdg‘ℎ)–1-1→{𝑥 ∈ (𝒫 (Vtx‘ℎ) ∖ {∅}) ∣
(♯‘𝑥) ≤
2}} |
32 | 16, 31 | elab2g 3589 |
. 2
⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ {𝑔 ∣ [(Vtx‘𝑔) / 𝑣][(iEdg‘𝑔) / 𝑒]𝑒:dom 𝑒–1-1→{𝑥 ∈ (𝒫 𝑣 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}}
↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤
2})) |
33 | 2, 32 | syl5bb 286 |
1
⊢ (𝐺 ∈ 𝑈 → (𝐺 ∈ USPGraph ↔ 𝐸:dom 𝐸–1-1→{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤
2})) |