Theorem isisubgr

Description: The subgraph induced by a subset of vertices. (Contributed by AV, 12-May-2025)

	Ref	Expression
Hypotheses	isisubgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	isisubgr.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion	isisubgr	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) = ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		isisubgr.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		isisubgr.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3		elex	⊢ ( 𝐺 ∈ 𝑊 → 𝐺 ∈ V )
4	3	adantr	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → 𝐺 ∈ V )
5	1	fvexi	⊢ 𝑉 ∈ V
6	5	a1i	⊢ ( 𝑆 ⊆ 𝑉 → 𝑉 ∈ V )
7		id	⊢ ( 𝑆 ⊆ 𝑉 → 𝑆 ⊆ 𝑉 )
8	6 7	sselpwd	⊢ ( 𝑆 ⊆ 𝑉 → 𝑆 ∈ 𝒫 𝑉 )
9	8	adantl	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → 𝑆 ∈ 𝒫 𝑉 )
10		opex	⊢ ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ ∈ V
11	10	a1i	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ ∈ V )
12		simpr	⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑆 ) → 𝑣 = 𝑆 )
13		fvexd	⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑆 ) → ( iEdg ‘ 𝑔 ) ∈ V )
14		fveq2	⊢ ( 𝑔 = 𝐺 → ( iEdg ‘ 𝑔 ) = ( iEdg ‘ 𝐺 ) )
15	14 2	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( iEdg ‘ 𝑔 ) = 𝐸 )
16	15	eqeq2d	⊢ ( 𝑔 = 𝐺 → ( 𝑒 = ( iEdg ‘ 𝑔 ) ↔ 𝑒 = 𝐸 ) )
17	16	adantr	⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑆 ) → ( 𝑒 = ( iEdg ‘ 𝑔 ) ↔ 𝑒 = 𝐸 ) )
18		simpr	⊢ ( ( 𝑣 = 𝑆 ∧ 𝑒 = 𝐸 ) → 𝑒 = 𝐸 )
19		dmeq	⊢ ( 𝑒 = 𝐸 → dom 𝑒 = dom 𝐸 )
20	19	adantl	⊢ ( ( 𝑣 = 𝑆 ∧ 𝑒 = 𝐸 ) → dom 𝑒 = dom 𝐸 )
21		fveq1	⊢ ( 𝑒 = 𝐸 → ( 𝑒 ‘ 𝑥 ) = ( 𝐸 ‘ 𝑥 ) )
22	21	adantl	⊢ ( ( 𝑣 = 𝑆 ∧ 𝑒 = 𝐸 ) → ( 𝑒 ‘ 𝑥 ) = ( 𝐸 ‘ 𝑥 ) )
23		simpl	⊢ ( ( 𝑣 = 𝑆 ∧ 𝑒 = 𝐸 ) → 𝑣 = 𝑆 )
24	22 23	sseq12d	⊢ ( ( 𝑣 = 𝑆 ∧ 𝑒 = 𝐸 ) → ( ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 ↔ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 ) )
25	20 24	rabeqbidv	⊢ ( ( 𝑣 = 𝑆 ∧ 𝑒 = 𝐸 ) → { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } = { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } )
26	18 25	reseq12d	⊢ ( ( 𝑣 = 𝑆 ∧ 𝑒 = 𝐸 ) → ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) )
27	26	ex	⊢ ( 𝑣 = 𝑆 → ( 𝑒 = 𝐸 → ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ) )
28	27	adantl	⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑆 ) → ( 𝑒 = 𝐸 → ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ) )
29	17 28	sylbid	⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑆 ) → ( 𝑒 = ( iEdg ‘ 𝑔 ) → ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ) )
30	29	imp	⊢ ( ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑆 ) ∧ 𝑒 = ( iEdg ‘ 𝑔 ) ) → ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) )
31	13 30	csbied	⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑆 ) → ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) )
32	12 31	opeq12d	⊢ ( ( 𝑔 = 𝐺 ∧ 𝑣 = 𝑆 ) → ⟨ 𝑣 , ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) ⟩ = ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ )
33		fveq2	⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = ( Vtx ‘ 𝐺 ) )
34	33 1	eqtr4di	⊢ ( 𝑔 = 𝐺 → ( Vtx ‘ 𝑔 ) = 𝑉 )
35	34	pweqd	⊢ ( 𝑔 = 𝐺 → 𝒫 ( Vtx ‘ 𝑔 ) = 𝒫 𝑉 )
36		df-isubgr	⊢ ISubGr = ( 𝑔 ∈ V , 𝑣 ∈ 𝒫 ( Vtx ‘ 𝑔 ) ↦ ⟨ 𝑣 , ⦋ ( iEdg ‘ 𝑔 ) / 𝑒 ⦌ ( 𝑒 ↾ { 𝑥 ∈ dom 𝑒 ∣ ( 𝑒 ‘ 𝑥 ) ⊆ 𝑣 } ) ⟩ )
37	32 35 36	ovmpox	⊢ ( ( 𝐺 ∈ V ∧ 𝑆 ∈ 𝒫 𝑉 ∧ ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ ∈ V ) → ( 𝐺 ISubGr 𝑆 ) = ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ )
38	4 9 11 37	syl3anc	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) = ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ )