Metamath Proof Explorer


Theorem uhgrn0

Description: An edge is a nonempty subset of vertices. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 15-Dec-2020)

Ref Expression
Hypothesis uhgrfun.e
|- E = ( iEdg ` G )
Assertion uhgrn0
|- ( ( G e. UHGraph /\ E Fn A /\ F e. A ) -> ( E ` F ) =/= (/) )

Proof

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 ) =/= (/) )