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 → G SubGraph G

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 → G SubGraph G ↔ Vtx ⁡ G ⊆ Vtx ⁡ G ∧ iEdg ⁡ G ⊆ iEdg ⁡ G
9 5 6 8 mpd3an23 ⊢ G ∈ UHGraph → G SubGraph G ↔ Vtx ⁡ G ⊆ Vtx ⁡ G ∧ iEdg ⁡ G ⊆ iEdg ⁡ G
10 3 9 mpbiri ⊢ G ∈ UHGraph → G SubGraph G