uhgrissubgr

Description: The property of a hypergraph to be a subgraph. (Contributed by AV, 19-Nov-2020)

	Ref	Expression
Hypotheses	uhgrissubgr.v	$⊢ V = Vtx (S)$
	uhgrissubgr.a	$⊢ A = Vtx (G)$
	uhgrissubgr.i	$⊢ I = iEdg (S)$
	uhgrissubgr.b	$⊢ B = iEdg (G)$
Assertion	uhgrissubgr	$⊢ (G \in W \land Fun B \land S \in UHGraph) \to (S SubGraph G \leftrightarrow (V \subseteq A \land I \subseteq B))$

Proof

Step	Hyp	Ref	Expression
1		uhgrissubgr.v	$⊢ V = Vtx (S)$
2		uhgrissubgr.a	$⊢ A = Vtx (G)$
3		uhgrissubgr.i	$⊢ I = iEdg (S)$
4		uhgrissubgr.b	$⊢ B = iEdg (G)$
5		eqid	$⊢ Edg (S) = Edg (S)$
6	1 2 3 4 5	subgrprop2	$⊢ S SubGraph G \to (V \subseteq A \land I \subseteq B \land Edg (S) \subseteq 𝒫 V)$
7		3simpa	$⊢ (V \subseteq A \land I \subseteq B \land Edg (S) \subseteq 𝒫 V) \to (V \subseteq A \land I \subseteq B)$
8	6 7	syl	$⊢ S SubGraph G \to (V \subseteq A \land I \subseteq B)$
9		simprl	$⊢ ((G \in W \land Fun B \land S \in UHGraph) \land (V \subseteq A \land I \subseteq B)) \to V \subseteq A$
10		simp2	$⊢ (G \in W \land Fun B \land S \in UHGraph) \to Fun B$
11		simpr	$⊢ (V \subseteq A \land I \subseteq B) \to I \subseteq B$
12		funssres	$⊢ (Fun B \land I \subseteq B) \to {B ↾}_{dom I} = I$
13	10 11 12	syl2an	$⊢ ((G \in W \land Fun B \land S \in UHGraph) \land (V \subseteq A \land I \subseteq B)) \to {B ↾}_{dom I} = I$
14	13	eqcomd	$⊢ ((G \in W \land Fun B \land S \in UHGraph) \land (V \subseteq A \land I \subseteq B)) \to I = {B ↾}_{dom I}$
15		edguhgr	$⊢ (S \in UHGraph \land e \in Edg (S)) \to e \in 𝒫 Vtx (S)$
16	15	ex	$⊢ S \in UHGraph \to (e \in Edg (S) \to e \in 𝒫 Vtx (S))$
17	1	pweqi	$⊢ 𝒫 V = 𝒫 Vtx (S)$
18	17	eleq2i	$⊢ e \in 𝒫 V \leftrightarrow e \in 𝒫 Vtx (S)$
19	16 18	imbitrrdi	$⊢ S \in UHGraph \to (e \in Edg (S) \to e \in 𝒫 V)$
20	19	ssrdv	$⊢ S \in UHGraph \to Edg (S) \subseteq 𝒫 V$
21	20	3ad2ant3	$⊢ (G \in W \land Fun B \land S \in UHGraph) \to Edg (S) \subseteq 𝒫 V$
22	21	adantr	$⊢ ((G \in W \land Fun B \land S \in UHGraph) \land (V \subseteq A \land I \subseteq B)) \to Edg (S) \subseteq 𝒫 V$
23	1 2 3 4 5	issubgr	$⊢ (G \in W \land S \in UHGraph) \to (S SubGraph G \leftrightarrow (V \subseteq A \land I = {B ↾}_{dom I} \land Edg (S) \subseteq 𝒫 V))$
24	23	3adant2	$⊢ (G \in W \land Fun B \land S \in UHGraph) \to (S SubGraph G \leftrightarrow (V \subseteq A \land I = {B ↾}_{dom I} \land Edg (S) \subseteq 𝒫 V))$
25	24	adantr	$⊢ ((G \in W \land Fun B \land S \in UHGraph) \land (V \subseteq A \land I \subseteq B)) \to (S SubGraph G \leftrightarrow (V \subseteq A \land I = {B ↾}_{dom I} \land Edg (S) \subseteq 𝒫 V))$
26	9 14 22 25	mpbir3and	$⊢ ((G \in W \land Fun B \land S \in UHGraph) \land (V \subseteq A \land I \subseteq B)) \to S SubGraph G$
27	26	ex	$⊢ (G \in W \land Fun B \land S \in UHGraph) \to ((V \subseteq A \land I \subseteq B) \to S SubGraph G)$
28	8 27	impbid2	$⊢ (G \in W \land Fun B \land S \in UHGraph) \to (S SubGraph G \leftrightarrow (V \subseteq A \land I \subseteq B))$

Metamath Proof Explorer

Theorem uhgrissubgr

Proof