Metamath Proof Explorer

Theorem uhgrspan1

Description: The induced subgraph S of a hypergraph G obtained by removing one vertex is actually a subgraph of G . A subgraph is called induced orspanned by a subset of vertices of a graph if it contains all edges of the original graph that join two vertices of the subgraph (see section I.1 in Bollobas p. 2 and section 1.1 in Diestel p. 4). (Contributed by AV, 19-Nov-2020)

Ref Expression
Hypotheses uhgrspan1.v 
|- V = ( Vtx ` G )
uhgrspan1.i 
|- I = ( iEdg ` G )
uhgrspan1.f 
|- F = { i e. dom I | N e/ ( I ` i ) }
uhgrspan1.s 
|- S = <. ( V \ { N } ) , ( I |` F ) >.
Assertion uhgrspan1 
|- ( ( G e. UHGraph /\ N e. V ) -> S SubGraph G )

Proof

Step Hyp Ref Expression
1 uhgrspan1.v 
 |-  V = ( Vtx ` G )
2 uhgrspan1.i 
 |-  I = ( iEdg ` G )
3 uhgrspan1.f 
 |-  F = { i e. dom I | N e/ ( I ` i ) }
4 uhgrspan1.s 
 |-  S = <. ( V \ { N } ) , ( I |` F ) >.
5 difssd 
 |-  ( ( G e. UHGraph /\ N e. V ) -> ( V \ { N } ) C_ V )
6 1 2 3 4 uhgrspan1lem3 
 |-  ( iEdg ` S ) = ( I |` F )
7 resresdm 
 |-  ( ( iEdg ` S ) = ( I |` F ) -> ( iEdg ` S ) = ( I |` dom ( iEdg ` S ) ) )
8 6 7 mp1i 
 |-  ( ( G e. UHGraph /\ N e. V ) -> ( iEdg ` S ) = ( I |` dom ( iEdg ` S ) ) )
9 2 uhgrfun 
 |-  ( G e. UHGraph -> Fun I )
10 fvelima 
 |-  ( ( Fun I /\ c e. ( I " F ) ) -> E. j e. F ( I ` j ) = c )
11 10 ex 
 |-  ( Fun I -> ( c e. ( I " F ) -> E. j e. F ( I ` j ) = c ) )
12 9 11 syl 
 |-  ( G e. UHGraph -> ( c e. ( I " F ) -> E. j e. F ( I ` j ) = c ) )
13 12 adantr 
 |-  ( ( G e. UHGraph /\ N e. V ) -> ( c e. ( I " F ) -> E. j e. F ( I ` j ) = c ) )
14 eqidd 
 |-  ( i = j -> N = N )
15 fveq2 
 |-  ( i = j -> ( I ` i ) = ( I ` j ) )
16 14 15 neleq12d 
 |-  ( i = j -> ( N e/ ( I ` i ) <-> N e/ ( I ` j ) ) )
17 16 3 elrab2 
 |-  ( j e. F <-> ( j e. dom I /\ N e/ ( I ` j ) ) )
18 fvexd 
 |-  ( ( ( G e. UHGraph /\ N e. V ) /\ ( j e. dom I /\ N e/ ( I ` j ) ) ) -> ( I ` j ) e. _V )
19 1 2 uhgrss 
 |-  ( ( G e. UHGraph /\ j e. dom I ) -> ( I ` j ) C_ V )
20 19 ad2ant2r 
 |-  ( ( ( G e. UHGraph /\ N e. V ) /\ ( j e. dom I /\ N e/ ( I ` j ) ) ) -> ( I ` j ) C_ V )
21 simprr 
 |-  ( ( ( G e. UHGraph /\ N e. V ) /\ ( j e. dom I /\ N e/ ( I ` j ) ) ) -> N e/ ( I ` j ) )
22 elpwdifsn 
 |-  ( ( ( I ` j ) e. _V /\ ( I ` j ) C_ V /\ N e/ ( I ` j ) ) -> ( I ` j ) e. ~P ( V \ { N } ) )
23 18 20 21 22 syl3anc 
 |-  ( ( ( G e. UHGraph /\ N e. V ) /\ ( j e. dom I /\ N e/ ( I ` j ) ) ) -> ( I ` j ) e. ~P ( V \ { N } ) )
24 eleq1 
 |-  ( c = ( I ` j ) -> ( c e. ~P ( V \ { N } ) <-> ( I ` j ) e. ~P ( V \ { N } ) ) )
25 24 eqcoms 
 |-  ( ( I ` j ) = c -> ( c e. ~P ( V \ { N } ) <-> ( I ` j ) e. ~P ( V \ { N } ) ) )
26 23 25 syl5ibrcom 
 |-  ( ( ( G e. UHGraph /\ N e. V ) /\ ( j e. dom I /\ N e/ ( I ` j ) ) ) -> ( ( I ` j ) = c -> c e. ~P ( V \ { N } ) ) )
27 26 ex 
 |-  ( ( G e. UHGraph /\ N e. V ) -> ( ( j e. dom I /\ N e/ ( I ` j ) ) -> ( ( I ` j ) = c -> c e. ~P ( V \ { N } ) ) ) )
28 17 27 biimtrid 
 |-  ( ( G e. UHGraph /\ N e. V ) -> ( j e. F -> ( ( I ` j ) = c -> c e. ~P ( V \ { N } ) ) ) )
29 28 rexlimdv 
 |-  ( ( G e. UHGraph /\ N e. V ) -> ( E. j e. F ( I ` j ) = c -> c e. ~P ( V \ { N } ) ) )
30 13 29 syld 
 |-  ( ( G e. UHGraph /\ N e. V ) -> ( c e. ( I " F ) -> c e. ~P ( V \ { N } ) ) )
31 30 ssrdv 
 |-  ( ( G e. UHGraph /\ N e. V ) -> ( I " F ) C_ ~P ( V \ { N } ) )
32 opex 
 |-  <. ( V \ { N } ) , ( I |` F ) >. e. _V
33 4 32 eqeltri 
 |-  S e. _V
34 33 a1i 
 |-  ( N e. V -> S e. _V )
35 1 2 3 4 uhgrspan1lem2 
 |-  ( Vtx ` S ) = ( V \ { N } )
36 35 eqcomi 
 |-  ( V \ { N } ) = ( Vtx ` S )
37 eqid 
 |-  ( iEdg ` S ) = ( iEdg ` S )
38 6 rneqi 
 |-  ran ( iEdg ` S ) = ran ( I |` F )
39 edgval 
 |-  ( Edg ` S ) = ran ( iEdg ` S )
40 df-ima 
 |-  ( I " F ) = ran ( I |` F )
41 38 39 40 3eqtr4ri 
 |-  ( I " F ) = ( Edg ` S )
42 36 1 37 2 41 issubgr 
 |-  ( ( G e. UHGraph /\ S e. _V ) -> ( S SubGraph G <-> ( ( V \ { N } ) C_ V /\ ( iEdg ` S ) = ( I |` dom ( iEdg ` S ) ) /\ ( I " F ) C_ ~P ( V \ { N } ) ) ) )
43 34 42 sylan2 
 |-  ( ( G e. UHGraph /\ N e. V ) -> ( S SubGraph G <-> ( ( V \ { N } ) C_ V /\ ( iEdg ` S ) = ( I |` dom ( iEdg ` S ) ) /\ ( I " F ) C_ ~P ( V \ { N } ) ) ) )
44 5 8 31 43 mpbir3and 
 |-  ( ( G e. UHGraph /\ N e. V ) -> S SubGraph G )