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	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion	uhgrn0	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ( 𝐸 ‘ 𝐹 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		uhgrfun.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
2		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
3	2 1	uhgrf	⊢ ( 𝐺 ∈ UHGraph → 𝐸 : dom 𝐸 ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
4		fndm	⊢ ( 𝐸 Fn 𝐴 → dom 𝐸 = 𝐴 )
5	4	feq2d	⊢ ( 𝐸 Fn 𝐴 → ( 𝐸 : dom 𝐸 ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ↔ 𝐸 : 𝐴 ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) )
6	3 5	syl5ibcom	⊢ ( 𝐺 ∈ UHGraph → ( 𝐸 Fn 𝐴 → 𝐸 : 𝐴 ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ) )
7	6	imp	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐸 Fn 𝐴 ) → 𝐸 : 𝐴 ⟶ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
8	7	ffvelcdmda	⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝐸 Fn 𝐴 ) ∧ 𝐹 ∈ 𝐴 ) → ( 𝐸 ‘ 𝐹 ) ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
9	8	3impa	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ( 𝐸 ‘ 𝐹 ) ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
10		eldifsni	⊢ ( ( 𝐸 ‘ 𝐹 ) ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) → ( 𝐸 ‘ 𝐹 ) ≠ ∅ )
11	9 10	syl	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐸 Fn 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ( 𝐸 ‘ 𝐹 ) ≠ ∅ )