Theorem issubgr2

Description: The property of a set to be a subgraph of a set whose edge function is actually a function. (Contributed by AV, 20-Nov-2020)

	Ref	Expression
Hypotheses	issubgr.v	⊢ 𝑉 = ( Vtx ‘ 𝑆 )
	issubgr.a	⊢ 𝐴 = ( Vtx ‘ 𝐺 )
	issubgr.i	⊢ 𝐼 = ( iEdg ‘ 𝑆 )
	issubgr.b	⊢ 𝐵 = ( iEdg ‘ 𝐺 )
	issubgr.e	⊢ 𝐸 = ( Edg ‘ 𝑆 )
Assertion	issubgr2	⊢ ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ 𝑈 ) → ( 𝑆 SubGraph 𝐺 ↔ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ∧ 𝐸 ⊆ 𝒫 𝑉 ) ) )

Proof

Step	Hyp	Ref	Expression
1		issubgr.v	⊢ 𝑉 = ( Vtx ‘ 𝑆 )
2		issubgr.a	⊢ 𝐴 = ( Vtx ‘ 𝐺 )
3		issubgr.i	⊢ 𝐼 = ( iEdg ‘ 𝑆 )
4		issubgr.b	⊢ 𝐵 = ( iEdg ‘ 𝐺 )
5		issubgr.e	⊢ 𝐸 = ( Edg ‘ 𝑆 )
6	1 2 3 4 5	issubgr	⊢ ( ( 𝐺 ∈ 𝑊 ∧ 𝑆 ∈ 𝑈 ) → ( 𝑆 SubGraph 𝐺 ↔ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) ) )
7	6	3adant2	⊢ ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ 𝑈 ) → ( 𝑆 SubGraph 𝐺 ↔ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) ) )
8		resss	⊢ ( 𝐵 ↾ dom 𝐼 ) ⊆ 𝐵
9		sseq1	⊢ ( 𝐼 = ( 𝐵 ↾ dom 𝐼 ) → ( 𝐼 ⊆ 𝐵 ↔ ( 𝐵 ↾ dom 𝐼 ) ⊆ 𝐵 ) )
10	8 9	mpbiri	⊢ ( 𝐼 = ( 𝐵 ↾ dom 𝐼 ) → 𝐼 ⊆ 𝐵 )
11		funssres	⊢ ( ( Fun 𝐵 ∧ 𝐼 ⊆ 𝐵 ) → ( 𝐵 ↾ dom 𝐼 ) = 𝐼 )
12	11	eqcomd	⊢ ( ( Fun 𝐵 ∧ 𝐼 ⊆ 𝐵 ) → 𝐼 = ( 𝐵 ↾ dom 𝐼 ) )
13	12	ex	⊢ ( Fun 𝐵 → ( 𝐼 ⊆ 𝐵 → 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ) )
14	13	3ad2ant2	⊢ ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ 𝑈 ) → ( 𝐼 ⊆ 𝐵 → 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ) )
15	10 14	impbid2	⊢ ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ 𝑈 ) → ( 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ↔ 𝐼 ⊆ 𝐵 ) )
16	15	3anbi2d	⊢ ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ 𝑈 ) → ( ( 𝑉 ⊆ 𝐴 ∧ 𝐼 = ( 𝐵 ↾ dom 𝐼 ) ∧ 𝐸 ⊆ 𝒫 𝑉 ) ↔ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ∧ 𝐸 ⊆ 𝒫 𝑉 ) ) )
17	7 16	bitrd	⊢ ( ( 𝐺 ∈ 𝑊 ∧ Fun 𝐵 ∧ 𝑆 ∈ 𝑈 ) → ( 𝑆 SubGraph 𝐺 ↔ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ∧ 𝐸 ⊆ 𝒫 𝑉 ) ) )