This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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