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 𝐺 )