Metamath Proof Explorer

Theorem uhgrspanop

Description: A spanning subgraph of a hypergraph represented by an ordered pair is a hypergraph. (Contributed by Alexander van der Vekens, 27-Dec-2017) (Revised by AV, 11-Oct-2020)

		Ref	Expression
	Hypotheses	uhgrspanop.v	$⊢ V = Vtx (G)$
		uhgrspanop.e	$⊢ E = iEdg (G)$
	Assertion	uhgrspanop	$⊢ G \in UHGraph \to ⟨V, {E ↾}_{A}⟩ \in UHGraph$

Proof

Step	Hyp	Ref	Expression
1		uhgrspanop.v	$⊢ V = Vtx (G)$
2		uhgrspanop.e	$⊢ E = iEdg (G)$
3		opex	$⊢ ⟨V, {E ↾}_{A}⟩ \in V$
4	3	a1i	$⊢ G \in UHGraph \to ⟨V, {E ↾}_{A}⟩ \in V$
5	1	fvexi	$⊢ V \in V$
6	2	fvexi	$⊢ E \in V$
7	6	resex	$⊢ {E ↾}_{A} \in V$
8	5 7	opvtxfvi	$⊢ Vtx (⟨V, {E ↾}_{A}⟩) = V$
9	8	a1i	$⊢ G \in UHGraph \to Vtx (⟨V, {E ↾}_{A}⟩) = V$
10	5 7	opiedgfvi	$⊢ iEdg (⟨V, {E ↾}_{A}⟩) = {E ↾}_{A}$
11	10	a1i	$⊢ G \in UHGraph \to iEdg (⟨V, {E ↾}_{A}⟩) = {E ↾}_{A}$
12		id	$⊢ G \in UHGraph \to G \in UHGraph$
13	1 2 4 9 11 12	uhgrspan	$⊢ G \in UHGraph \to ⟨V, {E ↾}_{A}⟩ \in UHGraph$