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 ⊢ V = Vtx ⁡ G
Assertion isubgrsubgr ⊢ G ∈ UHGraph ∧ S ⊆ V → G ISubGr S SubGraph G

Proof

Step Hyp Ref Expression
1 isubgrvtx.v ⊢ V = Vtx ⁡ G
2 1 isubgrvtx ⊢ G ∈ UHGraph ∧ S ⊆ V → Vtx ⁡ G ISubGr S = S
3 simpr ⊢ G ∈ UHGraph ∧ S ⊆ V → S ⊆ V
4 2 3 eqsstrd ⊢ G ∈ UHGraph ∧ S ⊆ V → Vtx ⁡ G ISubGr S ⊆ V
5 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
6 1 5 isubgriedg ⊢ G ∈ UHGraph ∧ S ⊆ V → iEdg ⁡ G ISubGr S = iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ S
7 resss ⊢ iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ S ⊆ iEdg ⁡ G
8 6 7 eqsstrdi ⊢ G ∈ UHGraph ∧ S ⊆ V → iEdg ⁡ G ISubGr S ⊆ iEdg ⁡ G
9 simpl ⊢ G ∈ UHGraph ∧ S ⊆ V → G ∈ UHGraph
10 5 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ iEdg ⁡ G
11 10 adantr ⊢ G ∈ UHGraph ∧ S ⊆ V → Fun ⁡ iEdg ⁡ G
12 1 isubgruhgr ⊢ G ∈ UHGraph ∧ S ⊆ V → G ISubGr S ∈ UHGraph
13 eqid ⊢ Vtx ⁡ G ISubGr S = Vtx ⁡ G ISubGr S
14 eqid ⊢ iEdg ⁡ G ISubGr S = iEdg ⁡ G ISubGr S
15 13 1 14 5 uhgrissubgr ⊢ G ∈ UHGraph ∧ Fun ⁡ iEdg ⁡ G ∧ G ISubGr S ∈ UHGraph → G ISubGr S SubGraph G ↔ Vtx ⁡ G ISubGr S ⊆ V ∧ iEdg ⁡ G ISubGr S ⊆ iEdg ⁡ G
16 9 11 12 15 syl3anc ⊢ G ∈ UHGraph ∧ S ⊆ V → G ISubGr S SubGraph G ↔ Vtx ⁡ G ISubGr S ⊆ V ∧ iEdg ⁡ G ISubGr S ⊆ iEdg ⁡ G
17 4 8 16 mpbir2and ⊢ G ∈ UHGraph ∧ S ⊆ V → G ISubGr S SubGraph G