Step |
Hyp |
Ref |
Expression |
1 |
|
isuhgr.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
2 |
|
isuhgr.e |
⊢ 𝐸 = ( iEdg ‘ 𝐺 ) |
3 |
|
df-uhgr |
⊢ UHGraph = { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) } |
4 |
3
|
eleq2i |
⊢ ( 𝐺 ∈ UHGraph ↔ 𝐺 ∈ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) } ) |
5 |
|
fveq2 |
⊢ ( ℎ = 𝐺 → ( iEdg ‘ ℎ ) = ( iEdg ‘ 𝐺 ) ) |
6 |
5 2
|
eqtr4di |
⊢ ( ℎ = 𝐺 → ( iEdg ‘ ℎ ) = 𝐸 ) |
7 |
5
|
dmeqd |
⊢ ( ℎ = 𝐺 → dom ( iEdg ‘ ℎ ) = dom ( iEdg ‘ 𝐺 ) ) |
8 |
2
|
eqcomi |
⊢ ( iEdg ‘ 𝐺 ) = 𝐸 |
9 |
8
|
dmeqi |
⊢ dom ( iEdg ‘ 𝐺 ) = dom 𝐸 |
10 |
7 9
|
eqtrdi |
⊢ ( ℎ = 𝐺 → dom ( iEdg ‘ ℎ ) = dom 𝐸 ) |
11 |
|
fveq2 |
⊢ ( ℎ = 𝐺 → ( Vtx ‘ ℎ ) = ( Vtx ‘ 𝐺 ) ) |
12 |
11 1
|
eqtr4di |
⊢ ( ℎ = 𝐺 → ( Vtx ‘ ℎ ) = 𝑉 ) |
13 |
12
|
pweqd |
⊢ ( ℎ = 𝐺 → 𝒫 ( Vtx ‘ ℎ ) = 𝒫 𝑉 ) |
14 |
13
|
difeq1d |
⊢ ( ℎ = 𝐺 → ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) = ( 𝒫 𝑉 ∖ { ∅ } ) ) |
15 |
6 10 14
|
feq123d |
⊢ ( ℎ = 𝐺 → ( ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) ⟶ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) ) |
16 |
|
fvexd |
⊢ ( 𝑔 = ℎ → ( Vtx ‘ 𝑔 ) ∈ V ) |
17 |
|
fveq2 |
⊢ ( 𝑔 = ℎ → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ ℎ ) ) |
18 |
|
fvexd |
⊢ ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) → ( iEdg ‘ 𝑔 ) ∈ V ) |
19 |
|
fveq2 |
⊢ ( 𝑔 = ℎ → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ ℎ ) ) |
20 |
19
|
adantr |
⊢ ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ ℎ ) ) |
21 |
|
simpr |
⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → 𝑒 = ( iEdg ‘ ℎ ) ) |
22 |
21
|
dmeqd |
⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → dom 𝑒 = dom ( iEdg ‘ ℎ ) ) |
23 |
|
simpr |
⊢ ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) → 𝑣 = ( Vtx ‘ ℎ ) ) |
24 |
23
|
pweqd |
⊢ ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) → 𝒫 𝑣 = 𝒫 ( Vtx ‘ ℎ ) ) |
25 |
24
|
difeq1d |
⊢ ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) → ( 𝒫 𝑣 ∖ { ∅ } ) = ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ) |
26 |
25
|
adantr |
⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → ( 𝒫 𝑣 ∖ { ∅ } ) = ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ) |
27 |
21 22 26
|
feq123d |
⊢ ( ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) ∧ 𝑒 = ( iEdg ‘ ℎ ) ) → ( 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) ↔ ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) ⟶ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ) ) |
28 |
18 20 27
|
sbcied2 |
⊢ ( ( 𝑔 = ℎ ∧ 𝑣 = ( Vtx ‘ ℎ ) ) → ( [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) ↔ ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) ⟶ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ) ) |
29 |
16 17 28
|
sbcied2 |
⊢ ( 𝑔 = ℎ → ( [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) ↔ ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) ⟶ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) ) ) |
30 |
29
|
cbvabv |
⊢ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) } = { ℎ ∣ ( iEdg ‘ ℎ ) : dom ( iEdg ‘ ℎ ) ⟶ ( 𝒫 ( Vtx ‘ ℎ ) ∖ { ∅ } ) } |
31 |
15 30
|
elab2g |
⊢ ( 𝐺 ∈ 𝑈 → ( 𝐺 ∈ { 𝑔 ∣ [ ( Vtx ‘ 𝑔 ) / 𝑣 ] [ ( iEdg ‘ 𝑔 ) / 𝑒 ] 𝑒 : dom 𝑒 ⟶ ( 𝒫 𝑣 ∖ { ∅ } ) } ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) ) |
32 |
4 31
|
syl5bb |
⊢ ( 𝐺 ∈ 𝑈 → ( 𝐺 ∈ UHGraph ↔ 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ) ) |