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 ( 𝐺 ∈ UHGraph → 𝐺 SubGraph 𝐺 )

Proof

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