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 e. UHGraph -> G SubGraph G )

Proof

Step Hyp Ref Expression
1 ssid 
 |-  ( Vtx ` G ) C_ ( Vtx ` G )
2 ssid 
 |-  ( iEdg ` G ) C_ ( iEdg ` G )
3 1 2 pm3.2i 
 |-  ( ( Vtx ` G ) C_ ( Vtx ` G ) /\ ( iEdg ` G ) C_ ( iEdg ` G ) )
4 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
5 4 uhgrfun 
 |-  ( G e. UHGraph -> Fun ( iEdg ` G ) )
6 id 
 |-  ( G e. UHGraph -> G e. UHGraph )
7 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
8 7 7 4 4 uhgrissubgr 
 |-  ( ( G e. UHGraph /\ Fun ( iEdg ` G ) /\ G e. UHGraph ) -> ( G SubGraph G <-> ( ( Vtx ` G ) C_ ( Vtx ` G ) /\ ( iEdg ` G ) C_ ( iEdg ` G ) ) ) )
9 5 6 8 mpd3an23 
 |-  ( G e. UHGraph -> ( G SubGraph G <-> ( ( Vtx ` G ) C_ ( Vtx ` G ) /\ ( iEdg ` G ) C_ ( iEdg ` G ) ) ) )
10 3 9 mpbiri 
 |-  ( G e. UHGraph -> G SubGraph G )