Metamath Proof Explorer

Theorem uhgrspansubgr

Description: A spanning subgraph S of a hypergraph G is actually a subgraph of G . A subgraph S of a graph G which has the same vertices as G and is obtained by removing some edges of G is called aspanning subgraph (see section I.1 in Bollobas p. 2 and section 1.1 in Diestel p. 4). Formally, the edges are "removed" by restricting the edge function of the original graph by an arbitrary class (which actually needs not to be a subset of the domain of the edge function). (Contributed by AV, 18-Nov-2020) (Proof shortened by AV, 21-Nov-2020)

Ref Expression
Hypotheses uhgrspan.v ⊢ V = Vtx ⁡ G
uhgrspan.e ⊢ E = iEdg ⁡ G
uhgrspan.s ⊢ φ → S ∈ W
uhgrspan.q ⊢ φ → Vtx ⁡ S = V
uhgrspan.r ⊢ φ → iEdg ⁡ S = E ↾ A
uhgrspan.g ⊢ φ → G ∈ UHGraph
Assertion uhgrspansubgr ⊢ φ → S SubGraph G

Proof

Step Hyp Ref Expression
1 uhgrspan.v ⊢ V = Vtx ⁡ G
2 uhgrspan.e ⊢ E = iEdg ⁡ G
3 uhgrspan.s ⊢ φ → S ∈ W
4 uhgrspan.q ⊢ φ → Vtx ⁡ S = V
5 uhgrspan.r ⊢ φ → iEdg ⁡ S = E ↾ A
6 uhgrspan.g ⊢ φ → G ∈ UHGraph
7 ssid ⊢ Vtx ⁡ S ⊆ Vtx ⁡ S
8 7 4 sseqtrid ⊢ φ → Vtx ⁡ S ⊆ V
9 resss ⊢ E ↾ A ⊆ E
10 5 9 eqsstrdi ⊢ φ → iEdg ⁡ S ⊆ E
11 1 2 3 4 5 6 uhgrspansubgrlem ⊢ φ → Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S
12 2 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ E
13 6 12 syl ⊢ φ → Fun ⁡ E
14 eqid ⊢ Vtx ⁡ S = Vtx ⁡ S
15 eqid ⊢ iEdg ⁡ S = iEdg ⁡ S
16 eqid ⊢ Edg ⁡ S = Edg ⁡ S
17 14 1 15 2 16 issubgr2 ⊢ G ∈ UHGraph ∧ Fun ⁡ E ∧ S ∈ W → S SubGraph G ↔ Vtx ⁡ S ⊆ V ∧ iEdg ⁡ S ⊆ E ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S
18 6 13 3 17 syl3anc ⊢ φ → S SubGraph G ↔ Vtx ⁡ S ⊆ V ∧ iEdg ⁡ S ⊆ E ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S
19 8 10 11 18 mpbir3and ⊢ φ → S SubGraph G