Step |
Hyp |
Ref |
Expression |
1 |
|
uhgrfun.e |
|- E = ( iEdg ` G ) |
2 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
3 |
2 1
|
uhgrf |
|- ( G e. UHGraph -> E : dom E --> ( ~P ( Vtx ` G ) \ { (/) } ) ) |
4 |
|
fndm |
|- ( E Fn A -> dom E = A ) |
5 |
4
|
feq2d |
|- ( E Fn A -> ( E : dom E --> ( ~P ( Vtx ` G ) \ { (/) } ) <-> E : A --> ( ~P ( Vtx ` G ) \ { (/) } ) ) ) |
6 |
3 5
|
syl5ibcom |
|- ( G e. UHGraph -> ( E Fn A -> E : A --> ( ~P ( Vtx ` G ) \ { (/) } ) ) ) |
7 |
6
|
imp |
|- ( ( G e. UHGraph /\ E Fn A ) -> E : A --> ( ~P ( Vtx ` G ) \ { (/) } ) ) |
8 |
7
|
ffvelrnda |
|- ( ( ( G e. UHGraph /\ E Fn A ) /\ F e. A ) -> ( E ` F ) e. ( ~P ( Vtx ` G ) \ { (/) } ) ) |
9 |
8
|
3impa |
|- ( ( G e. UHGraph /\ E Fn A /\ F e. A ) -> ( E ` F ) e. ( ~P ( Vtx ` G ) \ { (/) } ) ) |
10 |
|
eldifsni |
|- ( ( E ` F ) e. ( ~P ( Vtx ` G ) \ { (/) } ) -> ( E ` F ) =/= (/) ) |
11 |
9 10
|
syl |
|- ( ( G e. UHGraph /\ E Fn A /\ F e. A ) -> ( E ` F ) =/= (/) ) |