Metamath Proof Explorer

Theorem uhgrsubgrself

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

Ref Expression
Assertion uhgrsubgrself ⊢G∈UHGraph→GSubGraphG

Proof

Step Hyp Ref Expression
1 ssid ⊢Vtx⁡G⊆Vtx⁡G
2 ssid ⊢iEdg⁡G⊆iEdg⁡G
3 1 2 pm3.2i ⊢Vtx⁡G⊆Vtx⁡G∧iEdg⁡G⊆iEdg⁡G
4 eqid ⊢iEdg⁡G=iEdg⁡G
5 4 uhgrfun ⊢G∈UHGraph→Fun⁡iEdg⁡G
6 id ⊢G∈UHGraph→G∈UHGraph
7 eqid ⊢Vtx⁡G=Vtx⁡G
8 7 7 4 4 uhgrissubgr ⊢G∈UHGraph∧Fun⁡iEdg⁡G∧G∈UHGraph→GSubGraphG↔Vtx⁡G⊆Vtx⁡G∧iEdg⁡G⊆iEdg⁡G
9 5 6 8 mpd3an23 ⊢G∈UHGraph→GSubGraphG↔Vtx⁡G⊆Vtx⁡G∧iEdg⁡G⊆iEdg⁡G
10 3 9 mpbiri ⊢G∈UHGraph→GSubGraphG