# 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 𝑉 = ( Vtx ‘ 𝐺 )
uhgrspan1.i 𝐼 = ( iEdg ‘ 𝐺 )
uhgrspan1.f 𝐹 = { 𝑖 ∈ dom 𝐼𝑁 ∉ ( 𝐼𝑖 ) }
uhgrspan1.s 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( 𝐼𝐹 ) ⟩
Assertion uhgrspan1 ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑉 ) → 𝑆 SubGraph 𝐺 )

### Proof

Step Hyp Ref Expression
1 uhgrspan1.v 𝑉 = ( Vtx ‘ 𝐺 )
2 uhgrspan1.i 𝐼 = ( iEdg ‘ 𝐺 )
3 uhgrspan1.f 𝐹 = { 𝑖 ∈ dom 𝐼𝑁 ∉ ( 𝐼𝑖 ) }
4 uhgrspan1.s 𝑆 = ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( 𝐼𝐹 ) ⟩
5 difssd ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑉 ) → ( 𝑉 ∖ { 𝑁 } ) ⊆ 𝑉 )
6 1 2 3 4 uhgrspan1lem3 ( iEdg ‘ 𝑆 ) = ( 𝐼𝐹 )
7 resresdm ( ( iEdg ‘ 𝑆 ) = ( 𝐼𝐹 ) → ( iEdg ‘ 𝑆 ) = ( 𝐼 ↾ dom ( iEdg ‘ 𝑆 ) ) )
8 6 7 mp1i ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑉 ) → ( iEdg ‘ 𝑆 ) = ( 𝐼 ↾ dom ( iEdg ‘ 𝑆 ) ) )
9 2 uhgrfun ( 𝐺 ∈ UHGraph → Fun 𝐼 )
10 fvelima ( ( Fun 𝐼𝑐 ∈ ( 𝐼𝐹 ) ) → ∃ 𝑗𝐹 ( 𝐼𝑗 ) = 𝑐 )
11 10 ex ( Fun 𝐼 → ( 𝑐 ∈ ( 𝐼𝐹 ) → ∃ 𝑗𝐹 ( 𝐼𝑗 ) = 𝑐 ) )
12 9 11 syl ( 𝐺 ∈ UHGraph → ( 𝑐 ∈ ( 𝐼𝐹 ) → ∃ 𝑗𝐹 ( 𝐼𝑗 ) = 𝑐 ) )
13 12 adantr ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑉 ) → ( 𝑐 ∈ ( 𝐼𝐹 ) → ∃ 𝑗𝐹 ( 𝐼𝑗 ) = 𝑐 ) )
14 eqidd ( 𝑖 = 𝑗𝑁 = 𝑁 )
15 fveq2 ( 𝑖 = 𝑗 → ( 𝐼𝑖 ) = ( 𝐼𝑗 ) )
16 14 15 neleq12d ( 𝑖 = 𝑗 → ( 𝑁 ∉ ( 𝐼𝑖 ) ↔ 𝑁 ∉ ( 𝐼𝑗 ) ) )
17 16 3 elrab2 ( 𝑗𝐹 ↔ ( 𝑗 ∈ dom 𝐼𝑁 ∉ ( 𝐼𝑗 ) ) )
18 fvexd ( ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑉 ) ∧ ( 𝑗 ∈ dom 𝐼𝑁 ∉ ( 𝐼𝑗 ) ) ) → ( 𝐼𝑗 ) ∈ V )
19 1 2 uhgrss ( ( 𝐺 ∈ UHGraph ∧ 𝑗 ∈ dom 𝐼 ) → ( 𝐼𝑗 ) ⊆ 𝑉 )
20 19 ad2ant2r ( ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑉 ) ∧ ( 𝑗 ∈ dom 𝐼𝑁 ∉ ( 𝐼𝑗 ) ) ) → ( 𝐼𝑗 ) ⊆ 𝑉 )
21 simprr ( ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑉 ) ∧ ( 𝑗 ∈ dom 𝐼𝑁 ∉ ( 𝐼𝑗 ) ) ) → 𝑁 ∉ ( 𝐼𝑗 ) )
22 elpwdifsn ( ( ( 𝐼𝑗 ) ∈ V ∧ ( 𝐼𝑗 ) ⊆ 𝑉𝑁 ∉ ( 𝐼𝑗 ) ) → ( 𝐼𝑗 ) ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) )
23 18 20 21 22 syl3anc ( ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑉 ) ∧ ( 𝑗 ∈ dom 𝐼𝑁 ∉ ( 𝐼𝑗 ) ) ) → ( 𝐼𝑗 ) ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) )
24 eleq1 ( 𝑐 = ( 𝐼𝑗 ) → ( 𝑐 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ↔ ( 𝐼𝑗 ) ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ) )
25 24 eqcoms ( ( 𝐼𝑗 ) = 𝑐 → ( 𝑐 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ↔ ( 𝐼𝑗 ) ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ) )
26 23 25 syl5ibrcom ( ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑉 ) ∧ ( 𝑗 ∈ dom 𝐼𝑁 ∉ ( 𝐼𝑗 ) ) ) → ( ( 𝐼𝑗 ) = 𝑐𝑐 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ) )
27 26 ex ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑉 ) → ( ( 𝑗 ∈ dom 𝐼𝑁 ∉ ( 𝐼𝑗 ) ) → ( ( 𝐼𝑗 ) = 𝑐𝑐 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ) ) )
28 17 27 syl5bi ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑉 ) → ( 𝑗𝐹 → ( ( 𝐼𝑗 ) = 𝑐𝑐 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ) ) )
29 28 rexlimdv ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑉 ) → ( ∃ 𝑗𝐹 ( 𝐼𝑗 ) = 𝑐𝑐 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ) )
30 13 29 syld ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑉 ) → ( 𝑐 ∈ ( 𝐼𝐹 ) → 𝑐 ∈ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ) )
31 30 ssrdv ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑉 ) → ( 𝐼𝐹 ) ⊆ 𝒫 ( 𝑉 ∖ { 𝑁 } ) )
32 opex ⟨ ( 𝑉 ∖ { 𝑁 } ) , ( 𝐼𝐹 ) ⟩ ∈ V
33 4 32 eqeltri 𝑆 ∈ V
34 33 a1i ( 𝑁𝑉𝑆 ∈ V )
35 1 2 3 4 uhgrspan1lem2 ( Vtx ‘ 𝑆 ) = ( 𝑉 ∖ { 𝑁 } )
36 35 eqcomi ( 𝑉 ∖ { 𝑁 } ) = ( Vtx ‘ 𝑆 )
37 eqid ( iEdg ‘ 𝑆 ) = ( iEdg ‘ 𝑆 )
38 6 rneqi ran ( iEdg ‘ 𝑆 ) = ran ( 𝐼𝐹 )
39 edgval ( Edg ‘ 𝑆 ) = ran ( iEdg ‘ 𝑆 )
40 df-ima ( 𝐼𝐹 ) = ran ( 𝐼𝐹 )
41 38 39 40 3eqtr4ri ( 𝐼𝐹 ) = ( Edg ‘ 𝑆 )
42 36 1 37 2 41 issubgr ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ∈ V ) → ( 𝑆 SubGraph 𝐺 ↔ ( ( 𝑉 ∖ { 𝑁 } ) ⊆ 𝑉 ∧ ( iEdg ‘ 𝑆 ) = ( 𝐼 ↾ dom ( iEdg ‘ 𝑆 ) ) ∧ ( 𝐼𝐹 ) ⊆ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ) ) )
43 34 42 sylan2 ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑉 ) → ( 𝑆 SubGraph 𝐺 ↔ ( ( 𝑉 ∖ { 𝑁 } ) ⊆ 𝑉 ∧ ( iEdg ‘ 𝑆 ) = ( 𝐼 ↾ dom ( iEdg ‘ 𝑆 ) ) ∧ ( 𝐼𝐹 ) ⊆ 𝒫 ( 𝑉 ∖ { 𝑁 } ) ) ) )
44 5 8 31 43 mpbir3and ( ( 𝐺 ∈ UHGraph ∧ 𝑁𝑉 ) → 𝑆 SubGraph 𝐺 )