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

Metamath Proof Explorer

Theorem uhgrissubgr

Description: The property of a hypergraph to be a subgraph. (Contributed by AV, 19-Nov-2020)

Ref Expression
Hypotheses uhgrissubgr.v ⊢ 𝑉 = ( Vtx ‘ 𝑆 )
uhgrissubgr.a ⊢ 𝐴 = ( Vtx ‘ 𝐺 )
uhgrissubgr.i ⊢ 𝐼 = ( iEdg ‘ 𝑆 )
uhgrissubgr.b ⊢ 𝐵 = ( iEdg ‘ 𝐺 )
Assertion uhgrissubgr ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph ) → ( 𝑆 SubGraph 𝐺 ↔ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 uhgrissubgr.v ⊢ 𝑉 = ( Vtx ‘ 𝑆 )
2 uhgrissubgr.a ⊢ 𝐴 = ( Vtx ‘ 𝐺 )
3 uhgrissubgr.i ⊢ 𝐼 = ( iEdg ‘ 𝑆 )
4 uhgrissubgr.b ⊢ 𝐵 = ( iEdg ‘ 𝐺 )
5 eqid ⊢ ( Edg ‘ 𝑆 ) = ( Edg ‘ 𝑆 )
6 1 2 3 4 5 subgrprop2 ⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) )
7 3simpa ⊢ ( ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ) )
8 6 7 syl ⊢ ( 𝑆 SubGraph 𝐺 → ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ) )
9 simprl ⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph ) ∧ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ) ) → 𝑉 ⊆ 𝐴 )
10 simp2 ⊢ ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph ) → Fun 𝐵 )
11 simpr ⊢ ( ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ) → 𝐼 ⊆ 𝐵 )
12 funssres ⊢ ( ( Fun 𝐵 ∧ 𝐼 ⊆ 𝐵 ) → ( 𝐵 ↾ dom 𝐼 ) = 𝐼 )
13 10 11 12 syl2an ⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph ) ∧ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ) ) → ( 𝐵 ↾ dom 𝐼 ) = 𝐼 )
14 13 eqcomd ⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph ) ∧ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ) ) → 𝐼 = ( 𝐵 ↾ dom 𝐼 ) )
15 edguhgr ⊢ ( ( 𝑆 ∈ UHGraph ∧ 𝑒 ∈ ( Edg ‘ 𝑆 ) ) → 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) )
16 15 ex ⊢ ( 𝑆 ∈ UHGraph → ( 𝑒 ∈ ( Edg ‘ 𝑆 ) → 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) ) )
17 1 pweqi ⊢ 𝒫 𝑉 = 𝒫 ( Vtx ‘ 𝑆 )
18 17 eleq2i ⊢ ( 𝑒 ∈ 𝒫 𝑉 ↔ 𝑒 ∈ 𝒫 ( Vtx ‘ 𝑆 ) )
19 16 18 imbitrrdi ⊢ ( 𝑆 ∈ UHGraph → ( 𝑒 ∈ ( Edg ‘ 𝑆 ) → 𝑒 ∈ 𝒫 𝑉 ) )
20 19 ssrdv ⊢ ( 𝑆 ∈ UHGraph → ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 )
21 20 3ad2ant3 ⊢ ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph ) → ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 )
22 21 adantr ⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph ) ∧ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ) ) → ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 )
23 1 2 3 4 5 issubgr ⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ UHGraph ) → ( 𝑆 SubGraph 𝐺 ↔ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) )
24 23 3adant2 ⊢ ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph ) → ( 𝑆 SubGraph 𝐺 ↔ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) )
25 24 adantr ⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph ) ∧ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ) ) → ( 𝑆 SubGraph 𝐺 ↔ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ ( Edg ‘ 𝑆 ) ⊆ 𝒫 𝑉 ) ) )
26 9 14 22 25 mpbir3and ⊢ ( ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph ) ∧ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ) ) → 𝑆 SubGraph 𝐺 )
27 26 ex ⊢ ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph ) → ( ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ) → 𝑆 SubGraph 𝐺 ) )
28 8 27 impbid2 ⊢ ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ UHGraph ) → ( 𝑆 SubGraph 𝐺 ↔ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ) ) )