Theorem isubgriedg

Description: The edges of an induced subgraph. (Contributed by AV, 12-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		isubgriedg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		isubgriedg.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3	1 2	isisubgr	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) = ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ )
4	3	fveq2d	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) = ( iEdg ‘ ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ ) )
5	1	fvexi	⊢ 𝑉 ∈ V
6	5	ssex	⊢ ( 𝑆 ⊆ 𝑉 → 𝑆 ∈ V )
7	2	fvexi	⊢ 𝐸 ∈ V
8	7	a1i	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → 𝐸 ∈ V )
9	8	resexd	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ∈ V )
10		opiedgfv	⊢ ( ( 𝑆 ∈ V ∧ ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ∈ V ) → ( iEdg ‘ ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) )
11	6 9 10	syl2an2	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ ⟨ 𝑆 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) ⟩ ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) )
12	4 11	eqtrd	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) = ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑆 } ) )