Metamath Proof Explorer

Theorem issubgr

Description: The property of a set to be a subgraph of another set. (Contributed by AV, 16-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 issubgr ⊢G∈W∧S∈U→SSubGraphG↔V⊆A∧I=B↾dom⁡I∧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 fveq2 ⊢s=S→Vtx⁡s=Vtx⁡S
7 6 adantr ⊢s=S∧g=G→Vtx⁡s=Vtx⁡S
8 fveq2 ⊢g=G→Vtx⁡g=Vtx⁡G
9 8 adantl ⊢s=S∧g=G→Vtx⁡g=Vtx⁡G
10 7 9 sseq12d ⊢s=S∧g=G→Vtx⁡s⊆Vtx⁡g↔Vtx⁡S⊆Vtx⁡G
11 fveq2 ⊢s=S→iEdg⁡s=iEdg⁡S
12 11 adantr ⊢s=S∧g=G→iEdg⁡s=iEdg⁡S
13 fveq2 ⊢g=G→iEdg⁡g=iEdg⁡G
14 13 adantl ⊢s=S∧g=G→iEdg⁡g=iEdg⁡G
15 11 dmeqd ⊢s=S→dom⁡iEdg⁡s=dom⁡iEdg⁡S
16 15 adantr ⊢s=S∧g=G→dom⁡iEdg⁡s=dom⁡iEdg⁡S
17 14 16 reseq12d ⊢s=S∧g=G→iEdg⁡g↾dom⁡iEdg⁡s=iEdg⁡G↾dom⁡iEdg⁡S
18 12 17 eqeq12d ⊢s=S∧g=G→iEdg⁡s=iEdg⁡g↾dom⁡iEdg⁡s↔iEdg⁡S=iEdg⁡G↾dom⁡iEdg⁡S
19 fveq2 ⊢s=S→Edg⁡s=Edg⁡S
20 6 pweqd ⊢s=S→𝒫Vtx⁡s=𝒫Vtx⁡S
21 19 20 sseq12d ⊢s=S→Edg⁡s⊆𝒫Vtx⁡s↔Edg⁡S⊆𝒫Vtx⁡S
22 21 adantr ⊢s=S∧g=G→Edg⁡s⊆𝒫Vtx⁡s↔Edg⁡S⊆𝒫Vtx⁡S
23 10 18 22 3anbi123d ⊢s=S∧g=G→Vtx⁡s⊆Vtx⁡g∧iEdg⁡s=iEdg⁡g↾dom⁡iEdg⁡s∧Edg⁡s⊆𝒫Vtx⁡s↔Vtx⁡S⊆Vtx⁡G∧iEdg⁡S=iEdg⁡G↾dom⁡iEdg⁡S∧Edg⁡S⊆𝒫Vtx⁡S
24 df-subgr ⊢SubGraph=sg|Vtx⁡s⊆Vtx⁡g∧iEdg⁡s=iEdg⁡g↾dom⁡iEdg⁡s∧Edg⁡s⊆𝒫Vtx⁡s
25 23 24 brabga ⊢S∈U∧G∈W→SSubGraphG↔Vtx⁡S⊆Vtx⁡G∧iEdg⁡S=iEdg⁡G↾dom⁡iEdg⁡S∧Edg⁡S⊆𝒫Vtx⁡S
26 25 ancoms ⊢G∈W∧S∈U→SSubGraphG↔Vtx⁡S⊆Vtx⁡G∧iEdg⁡S=iEdg⁡G↾dom⁡iEdg⁡S∧Edg⁡S⊆𝒫Vtx⁡S
27 1 2 sseq12i ⊢V⊆A↔Vtx⁡S⊆Vtx⁡G
28 3 dmeqi ⊢dom⁡I=dom⁡iEdg⁡S
29 4 28 reseq12i ⊢B↾dom⁡I=iEdg⁡G↾dom⁡iEdg⁡S
30 3 29 eqeq12i ⊢I=B↾dom⁡I↔iEdg⁡S=iEdg⁡G↾dom⁡iEdg⁡S
31 1 pweqi ⊢𝒫V=𝒫Vtx⁡S
32 5 31 sseq12i ⊢E⊆𝒫V↔Edg⁡S⊆𝒫Vtx⁡S
33 27 30 32 3anbi123i ⊢V⊆A∧I=B↾dom⁡I∧E⊆𝒫V↔Vtx⁡S⊆Vtx⁡G∧iEdg⁡S=iEdg⁡G↾dom⁡iEdg⁡S∧Edg⁡S⊆𝒫Vtx⁡S
34 26 33 bitr4di ⊢G∈W∧S∈U→SSubGraphG↔V⊆A∧I=B↾dom⁡I∧E⊆𝒫V