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 → S SubGraph G ↔ 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 = s g | Vtx ⁡ s ⊆ Vtx ⁡ g ∧ iEdg ⁡ s = iEdg ⁡ g ↾ dom ⁡ iEdg ⁡ s ∧ Edg ⁡ s ⊆ 𝒫 Vtx ⁡ s
25 23 24 brabga ⊢ S ∈ U ∧ G ∈ W → S SubGraph G ↔ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S = iEdg ⁡ G ↾ dom ⁡ iEdg ⁡ S ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S
26 25 ancoms ⊢ G ∈ W ∧ S ∈ U → S SubGraph G ↔ 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 → S SubGraph G ↔ V ⊆ A ∧ I = B ↾ dom ⁡ I ∧ E ⊆ 𝒫 V