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