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 ⊢ 𝐸 = ( 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 𝐴 ∧ 𝐹 ∈ 𝐴 ) → ( 𝐸 ‘ 𝐹 ) ≠ ∅ )