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 𝐺 )