Metamath Proof Explorer

Theorem subgruhgredgd

Description: An edge of a subgraph of a hypergraph is a nonempty subset of its vertices. (Contributed by AV, 17-Nov-2020) (Revised by AV, 21-Nov-2020)

Ref Expression
Hypotheses subgruhgredgd.v ⊢ 𝑉 = ( Vtx ‘ 𝑆 )
subgruhgredgd.i ⊢ 𝐼 = ( iEdg ‘ 𝑆 )
subgruhgredgd.g ⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
subgruhgredgd.s ⊢ ( 𝜑 → 𝑆 SubGraph 𝐺 )
subgruhgredgd.x ⊢ ( 𝜑 → 𝑋 ∈ dom 𝐼 )
Assertion subgruhgredgd ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) )

Proof

Step Hyp Ref Expression
1 subgruhgredgd.v ⊢ 𝑉 = ( Vtx ‘ 𝑆 )
2 subgruhgredgd.i ⊢ 𝐼 = ( iEdg ‘ 𝑆 )
3 subgruhgredgd.g ⊢ ( 𝜑 → 𝐺 ∈ UHGraph )
4 subgruhgredgd.s ⊢ ( 𝜑 → 𝑆 SubGraph 𝐺 )
5 subgruhgredgd.x ⊢ ( 𝜑 → 𝑋 ∈ dom 𝐼 )
6 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
7 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
8 eqid ⊢ ( Edg ‘ 𝑆 ) = ( Edg ‘ 𝑆 )
9 1 6 2 7 8 subgrprop2 ⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) )
10 4 9 syl ⊢ ( 𝜑 → ( 𝑉 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) )
11 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑉 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) → ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 )
12 subgruhgrfun ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺 ) → Fun ( iEdg ‘ 𝑆 ) )
13 3 4 12 syl2anc ⊢ ( 𝜑 → Fun ( iEdg ‘ 𝑆 ) )
14 2 dmeqi ⊢ dom 𝐼 = dom ( iEdg ‘ 𝑆 )
15 5 14 eleqtrdi ⊢ ( 𝜑 → 𝑋 ∈ dom ( iEdg ‘ 𝑆 ) )
16 13 15 jca ⊢ ( 𝜑 → ( Fun ( iEdg ‘ 𝑆 ) ∧ 𝑋 ∈ dom ( iEdg ‘ 𝑆 ) ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ ( 𝑉 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) → ( Fun ( iEdg ‘ 𝑆 ) ∧ 𝑋 ∈ dom ( iEdg ‘ 𝑆 ) ) )
18 2 fveq1i ⊢ ( 𝐼 ‘ 𝑋 ) = ( ( iEdg ‘ 𝑆 ) ‘ 𝑋 )
19 fvelrn ⊢ ( ( Fun ( iEdg ‘ 𝑆 ) ∧ 𝑋 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( ( iEdg ‘ 𝑆 ) ‘ 𝑋 ) ∈ ran ( iEdg ‘ 𝑆 ) )
20 18 19 eqeltrid ⊢ ( ( Fun ( iEdg ‘ 𝑆 ) ∧ 𝑋 ∈ dom ( iEdg ‘ 𝑆 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ ran ( iEdg ‘ 𝑆 ) )
21 17 20 syl ⊢ ( ( 𝜑 ∧ ( 𝑉 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ ran ( iEdg ‘ 𝑆 ) )
22 edgval ⊢ ( Edg ‘ 𝑆 ) = ran ( iEdg ‘ 𝑆 )
23 21 22 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑉 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ ( Edg ‘ 𝑆 ) )
24 11 23 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑉 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ 𝒫 𝑉 )
25 7 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun ( iEdg ‘ 𝐺 ) )
26 3 25 syl ⊢ ( 𝜑 → Fun ( iEdg ‘ 𝐺 ) )
27 26 adantr ⊢ ( ( 𝜑 ∧ ( 𝑉 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) → Fun ( iEdg ‘ 𝐺 ) )
28 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑉 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) → 𝐼 ⊆ ( iEdg ‘ 𝐺 ) )
29 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑉 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) → 𝑋 ∈ dom 𝐼 )
30 funssfv ⊢ ( ( Fun ( iEdg ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑋 ) = ( 𝐼 ‘ 𝑋 ) )
31 30 eqcomd ⊢ ( ( Fun ( iEdg ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ 𝑋 ∈ dom 𝐼 ) → ( 𝐼 ‘ 𝑋 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑋 ) )
32 27 28 29 31 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑉 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) → ( 𝐼 ‘ 𝑋 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑋 ) )
33 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑉 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) → 𝐺 ∈ UHGraph )
34 26 funfnd ⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) )
35 34 adantr ⊢ ( ( 𝜑 ∧ ( 𝑉 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) → ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) )
36 subgreldmiedg ⊢ ( ( 𝑆 SubGraph 𝐺 ∧ 𝑋 ∈ dom ( iEdg ‘ 𝑆 ) ) → 𝑋 ∈ dom ( iEdg ‘ 𝐺 ) )
37 4 15 36 syl2anc ⊢ ( 𝜑 → 𝑋 ∈ dom ( iEdg ‘ 𝐺 ) )
38 37 adantr ⊢ ( ( 𝜑 ∧ ( 𝑉 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) → 𝑋 ∈ dom ( iEdg ‘ 𝐺 ) )
39 7 uhgrn0 ⊢ ( ( 𝐺 ∈ UHGraph ∧ ( iEdg ‘ 𝐺 ) Fn dom ( iEdg ‘ 𝐺 ) ∧ 𝑋 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑋 ) ≠ ∅ )
40 33 35 38 39 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑉 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑋 ) ≠ ∅ )
41 32 40 eqnetrd ⊢ ( ( 𝜑 ∧ ( 𝑉 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) → ( 𝐼 ‘ 𝑋 ) ≠ ∅ )
42 eldifsn ⊢ ( ( 𝐼 ‘ 𝑋 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ↔ ( ( 𝐼 ‘ 𝑋 ) ∈ 𝒫 𝑉 ∧ ( 𝐼 ‘ 𝑋 ) ≠ ∅ ) )
43 24 41 42 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑉 ⊆ ( Vtx ‘ 𝐺 ) ∧ 𝐼 ⊆ ( iEdg ‘ 𝐺 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) → ( 𝐼 ‘ 𝑋 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) )
44 10 43 mpdan ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑋 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) )