Metamath Proof Explorer

Theorem 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 e. W /\ Fun B /\ S e. UHGraph ) -> ( S SubGraph G <-> ( V C_ A /\ I C_ 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 -> ( V C_ A /\ I C_ B /\ ( Edg ` S ) C_ ~P V ) )
7 3simpa 
 |-  ( ( V C_ A /\ I C_ B /\ ( Edg ` S ) C_ ~P V ) -> ( V C_ A /\ I C_ B ) )
8 6 7 syl 
 |-  ( S SubGraph G -> ( V C_ A /\ I C_ B ) )
9 simprl 
 |-  ( ( ( G e. W /\ Fun B /\ S e. UHGraph ) /\ ( V C_ A /\ I C_ B ) ) -> V C_ A )
10 simp2 
 |-  ( ( G e. W /\ Fun B /\ S e. UHGraph ) -> Fun B )
11 simpr 
 |-  ( ( V C_ A /\ I C_ B ) -> I C_ B )
12 funssres 
 |-  ( ( Fun B /\ I C_ B ) -> ( B |` dom I ) = I )
13 10 11 12 syl2an 
 |-  ( ( ( G e. W /\ Fun B /\ S e. UHGraph ) /\ ( V C_ A /\ I C_ B ) ) -> ( B |` dom I ) = I )
14 13 eqcomd 
 |-  ( ( ( G e. W /\ Fun B /\ S e. UHGraph ) /\ ( V C_ A /\ I C_ B ) ) -> I = ( B |` dom I ) )
15 edguhgr 
 |-  ( ( S e. UHGraph /\ e e. ( Edg ` S ) ) -> e e. ~P ( Vtx ` S ) )
16 15 ex 
 |-  ( S e. UHGraph -> ( e e. ( Edg ` S ) -> e e. ~P ( Vtx ` S ) ) )
17 1 pweqi 
 |-  ~P V = ~P ( Vtx ` S )
18 17 eleq2i 
 |-  ( e e. ~P V <-> e e. ~P ( Vtx ` S ) )
19 16 18 imbitrrdi 
 |-  ( S e. UHGraph -> ( e e. ( Edg ` S ) -> e e. ~P V ) )
20 19 ssrdv 
 |-  ( S e. UHGraph -> ( Edg ` S ) C_ ~P V )
21 20 3ad2ant3 
 |-  ( ( G e. W /\ Fun B /\ S e. UHGraph ) -> ( Edg ` S ) C_ ~P V )
22 21 adantr 
 |-  ( ( ( G e. W /\ Fun B /\ S e. UHGraph ) /\ ( V C_ A /\ I C_ B ) ) -> ( Edg ` S ) C_ ~P V )
23 1 2 3 4 5 issubgr 
 |-  ( ( G e. W /\ S e. UHGraph ) -> ( S SubGraph G <-> ( V C_ A /\ I = ( B |` dom I ) /\ ( Edg ` S ) C_ ~P V ) ) )
24 23 3adant2 
 |-  ( ( G e. W /\ Fun B /\ S e. UHGraph ) -> ( S SubGraph G <-> ( V C_ A /\ I = ( B |` dom I ) /\ ( Edg ` S ) C_ ~P V ) ) )
25 24 adantr 
 |-  ( ( ( G e. W /\ Fun B /\ S e. UHGraph ) /\ ( V C_ A /\ I C_ B ) ) -> ( S SubGraph G <-> ( V C_ A /\ I = ( B |` dom I ) /\ ( Edg ` S ) C_ ~P V ) ) )
26 9 14 22 25 mpbir3and 
 |-  ( ( ( G e. W /\ Fun B /\ S e. UHGraph ) /\ ( V C_ A /\ I C_ B ) ) -> S SubGraph G )
27 26 ex 
 |-  ( ( G e. W /\ Fun B /\ S e. UHGraph ) -> ( ( V C_ A /\ I C_ B ) -> S SubGraph G ) )
28 8 27 impbid2 
 |-  ( ( G e. W /\ Fun B /\ S e. UHGraph ) -> ( S SubGraph G <-> ( V C_ A /\ I C_ B ) ) )