This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐺 ↔ ( 𝑉 ⊆ 𝐴 ∧ 𝐼 ⊆ 𝐵 ∧ 𝐸 ⊆ 𝒫 𝑉 ) ) )