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

Metamath Proof Explorer

Theorem isubgrsubgr

Description: An induced subgraph of a hypergraph is a subgraph of the hypergraph. (Contributed by AV, 14-May-2025)

Ref Expression
Hypothesis isubgrvtx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion isubgrsubgr ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) SubGraph 𝐺 )

Proof

Step Hyp Ref Expression
1 isubgrvtx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 1 isubgrvtx ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( Vtx ‘ ( 𝐺 ISubGr 𝑆 ) ) = 𝑆 )
3 simpr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ⊆ 𝑉 )
4 2 3 eqsstrd ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( Vtx ‘ ( 𝐺 ISubGr 𝑆 ) ) ⊆ 𝑉 )
5 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
6 1 5 isubgriedg ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) = ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) )
7 resss ⊢ ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ⊆ ( iEdg ‘ 𝐺 )
8 6 7 eqsstrdi ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) ⊆ ( iEdg ‘ 𝐺 ) )
9 simpl ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → 𝐺 ∈ UHGraph )
10 5 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun ( iEdg ‘ 𝐺 ) )
11 10 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → Fun ( iEdg ‘ 𝐺 ) )
12 1 isubgruhgr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) ∈ UHGraph )
13 eqid ⊢ ( Vtx ‘ ( 𝐺 ISubGr 𝑆 ) ) = ( Vtx ‘ ( 𝐺 ISubGr 𝑆 ) )
14 eqid ⊢ ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) = ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) )
15 13 1 14 5 uhgrissubgr ⊢ ( ( 𝐺 ∈ UHGraph ∧ Fun ( iEdg ‘ 𝐺 ) ∧ ( 𝐺 ISubGr 𝑆 ) ∈ UHGraph ) → ( ( 𝐺 ISubGr 𝑆 ) SubGraph 𝐺 ↔ ( ( Vtx ‘ ( 𝐺 ISubGr 𝑆 ) ) ⊆ 𝑉 ∧ ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) ⊆ ( iEdg ‘ 𝐺 ) ) ) )
16 9 11 12 15 syl3anc ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( ( 𝐺 ISubGr 𝑆 ) SubGraph 𝐺 ↔ ( ( Vtx ‘ ( 𝐺 ISubGr 𝑆 ) ) ⊆ 𝑉 ∧ ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) ⊆ ( iEdg ‘ 𝐺 ) ) ) )
17 4 8 16 mpbir2and ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) SubGraph 𝐺 )