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 ⊢ V = Vtx ⁡ S
issubgr.a ⊢ A = Vtx ⁡ G
issubgr.i ⊢ I = iEdg ⁡ S
issubgr.b ⊢ B = iEdg ⁡ G
issubgr.e ⊢ E = Edg ⁡ S
Assertion issubgr2 ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ U → S SubGraph G ↔ V ⊆ A ∧ I ⊆ B ∧ E ⊆ 𝒫 V

Proof

Step Hyp Ref Expression
1 issubgr.v ⊢ V = Vtx ⁡ S
2 issubgr.a ⊢ A = Vtx ⁡ G
3 issubgr.i ⊢ I = iEdg ⁡ S
4 issubgr.b ⊢ B = iEdg ⁡ G
5 issubgr.e ⊢ E = Edg ⁡ S
6 1 2 3 4 5 issubgr ⊢ G ∈ W ∧ S ∈ U → S SubGraph G ↔ V ⊆ A ∧ I = B ↾ dom ⁡ I ∧ E ⊆ 𝒫 V
7 6 3adant2 ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ U → S SubGraph G ↔ V ⊆ A ∧ I = B ↾ dom ⁡ I ∧ E ⊆ 𝒫 V
8 resss ⊢ B ↾ dom ⁡ I ⊆ B
9 sseq1 ⊢ I = B ↾ dom ⁡ I → I ⊆ B ↔ B ↾ dom ⁡ I ⊆ B
10 8 9 mpbiri ⊢ I = B ↾ dom ⁡ I → I ⊆ B
11 funssres ⊢ Fun ⁡ B ∧ I ⊆ B → B ↾ dom ⁡ I = I
12 11 eqcomd ⊢ Fun ⁡ B ∧ I ⊆ B → I = B ↾ dom ⁡ I
13 12 ex ⊢ Fun ⁡ B → I ⊆ B → I = B ↾ dom ⁡ I
14 13 3ad2ant2 ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ U → I ⊆ B → I = B ↾ dom ⁡ I
15 10 14 impbid2 ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ U → I = B ↾ dom ⁡ I ↔ I ⊆ B
16 15 3anbi2d ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ U → V ⊆ A ∧ I = B ↾ dom ⁡ I ∧ E ⊆ 𝒫 V ↔ V ⊆ A ∧ I ⊆ B ∧ E ⊆ 𝒫 V
17 7 16 bitrd ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ U → S SubGraph G ↔ V ⊆ A ∧ I ⊆ B ∧ E ⊆ 𝒫 V