subuhgr

Description: A subgraph of a hypergraph is a hypergraph. (Contributed by AV, 16-Nov-2020) (Proof shortened by AV, 21-Nov-2020)

		Ref	Expression
	Assertion	subuhgr	$⊢ (G \in UHGraph \land S SubGraph G) \to S \in UHGraph$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (S) = Vtx (S)$
2		eqid	$⊢ Vtx (G) = Vtx (G)$
3		eqid	$⊢ iEdg (S) = iEdg (S)$
4		eqid	$⊢ iEdg (G) = iEdg (G)$
5		eqid	$⊢ Edg (S) = Edg (S)$
6	1 2 3 4 5	subgrprop2	$⊢ S SubGraph G \to (Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S))$
7		subgruhgrfun	$⊢ (G \in UHGraph \land S SubGraph G) \to Fun iEdg (S)$
8	7	ancoms	$⊢ (S SubGraph G \land G \in UHGraph) \to Fun iEdg (S)$
9	8	adantl	$⊢ ((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UHGraph)) \to Fun iEdg (S)$
10	9	funfnd	$⊢ ((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UHGraph)) \to iEdg (S) Fn dom iEdg (S)$
11		simplrr	$⊢ (((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UHGraph)) \land x \in dom iEdg (S)) \to G \in UHGraph$
12		simplrl	$⊢ (((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UHGraph)) \land x \in dom iEdg (S)) \to S SubGraph G$
13		simpr	$⊢ (((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UHGraph)) \land x \in dom iEdg (S)) \to x \in dom iEdg (S)$
14	1 3 11 12 13	subgruhgredgd	$⊢ (((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UHGraph)) \land x \in dom iEdg (S)) \to iEdg (S) (x) \in (𝒫 Vtx (S) ∖ \{\emptyset\})$
15	14	ralrimiva	$⊢ ((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UHGraph)) \to \forall x \in dom iEdg (S) iEdg (S) (x) \in (𝒫 Vtx (S) ∖ \{\emptyset\})$
16		fnfvrnss	$⊢ (iEdg (S) Fn dom iEdg (S) \land \forall x \in dom iEdg (S) iEdg (S) (x) \in (𝒫 Vtx (S) ∖ \{\emptyset\})) \to ran iEdg (S) \subseteq 𝒫 Vtx (S) ∖ \{\emptyset\}$
17	10 15 16	syl2anc	$⊢ ((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UHGraph)) \to ran iEdg (S) \subseteq 𝒫 Vtx (S) ∖ \{\emptyset\}$
18		df-f	$⊢ iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\} \leftrightarrow (iEdg (S) Fn dom iEdg (S) \land ran iEdg (S) \subseteq 𝒫 Vtx (S) ∖ \{\emptyset\})$
19	10 17 18	sylanbrc	$⊢ ((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UHGraph)) \to iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\}$
20		subgrv	$⊢ S SubGraph G \to (S \in V \land G \in V)$
21	1 3	isuhgr	$⊢ S \in V \to (S \in UHGraph \leftrightarrow iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\})$
22	21	adantr	$⊢ (S \in V \land G \in V) \to (S \in UHGraph \leftrightarrow iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\})$
23	20 22	syl	$⊢ S SubGraph G \to (S \in UHGraph \leftrightarrow iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\})$
24	23	adantr	$⊢ (S SubGraph G \land G \in UHGraph) \to (S \in UHGraph \leftrightarrow iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\})$
25	24	adantl	$⊢ ((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UHGraph)) \to (S \in UHGraph \leftrightarrow iEdg (S) : dom iEdg (S) ⟶ 𝒫 Vtx (S) ∖ \{\emptyset\})$
26	19 25	mpbird	$⊢ ((Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \land (S SubGraph G \land G \in UHGraph)) \to S \in UHGraph$
27	26	ex	$⊢ (Vtx (S) \subseteq Vtx (G) \land iEdg (S) \subseteq iEdg (G) \land Edg (S) \subseteq 𝒫 Vtx (S)) \to ((S SubGraph G \land G \in UHGraph) \to S \in UHGraph)$
28	6 27	syl	$⊢ S SubGraph G \to ((S SubGraph G \land G \in UHGraph) \to S \in UHGraph)$
29	28	anabsi8	$⊢ (G \in UHGraph \land S SubGraph G) \to S \in UHGraph$

Metamath Proof Explorer

Theorem subuhgr

Proof