Metamath Proof Explorer

Theorem uhgrissubgr

Description: The property of a hypergraph to be a subgraph. (Contributed by AV, 19-Nov-2020)

Ref Expression
Hypotheses uhgrissubgr.v ⊢ V = Vtx ⁡ S
uhgrissubgr.a ⊢ A = Vtx ⁡ G
uhgrissubgr.i ⊢ I = iEdg ⁡ S
uhgrissubgr.b ⊢ B = iEdg ⁡ G
Assertion uhgrissubgr ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ UHGraph → S SubGraph G ↔ V ⊆ A ∧ I ⊆ B

Proof

Step Hyp Ref Expression
1 uhgrissubgr.v ⊢ V = Vtx ⁡ S
2 uhgrissubgr.a ⊢ A = Vtx ⁡ G
3 uhgrissubgr.i ⊢ I = iEdg ⁡ S
4 uhgrissubgr.b ⊢ B = iEdg ⁡ G
5 eqid ⊢ Edg ⁡ S = Edg ⁡ S
6 1 2 3 4 5 subgrprop2 ⊢ S SubGraph G → V ⊆ A ∧ I ⊆ B ∧ Edg ⁡ S ⊆ 𝒫 V
7 3simpa ⊢ V ⊆ A ∧ I ⊆ B ∧ Edg ⁡ S ⊆ 𝒫 V → V ⊆ A ∧ I ⊆ B
8 6 7 syl ⊢ S SubGraph G → V ⊆ A ∧ I ⊆ B
9 simprl ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ UHGraph ∧ V ⊆ A ∧ I ⊆ B → V ⊆ A
10 simp2 ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ UHGraph → Fun ⁡ B
11 simpr ⊢ V ⊆ A ∧ I ⊆ B → I ⊆ B
12 funssres ⊢ Fun ⁡ B ∧ I ⊆ B → B ↾ dom ⁡ I = I
13 10 11 12 syl2an ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ UHGraph ∧ V ⊆ A ∧ I ⊆ B → B ↾ dom ⁡ I = I
14 13 eqcomd ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ UHGraph ∧ V ⊆ A ∧ I ⊆ B → I = B ↾ dom ⁡ I
15 edguhgr ⊢ S ∈ UHGraph ∧ e ∈ Edg ⁡ S → e ∈ 𝒫 Vtx ⁡ S
16 15 ex ⊢ S ∈ UHGraph → e ∈ Edg ⁡ S → e ∈ 𝒫 Vtx ⁡ S
17 1 pweqi ⊢ 𝒫 V = 𝒫 Vtx ⁡ S
18 17 eleq2i ⊢ e ∈ 𝒫 V ↔ e ∈ 𝒫 Vtx ⁡ S
19 16 18 syl6ibr ⊢ S ∈ UHGraph → e ∈ Edg ⁡ S → e ∈ 𝒫 V
20 19 ssrdv ⊢ S ∈ UHGraph → Edg ⁡ S ⊆ 𝒫 V
21 20 3ad2ant3 ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ UHGraph → Edg ⁡ S ⊆ 𝒫 V
22 21 adantr ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ UHGraph ∧ V ⊆ A ∧ I ⊆ B → Edg ⁡ S ⊆ 𝒫 V
23 1 2 3 4 5 issubgr ⊢ G ∈ W ∧ S ∈ UHGraph → S SubGraph G ↔ V ⊆ A ∧ I = B ↾ dom ⁡ I ∧ Edg ⁡ S ⊆ 𝒫 V
24 23 3adant2 ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ UHGraph → S SubGraph G ↔ V ⊆ A ∧ I = B ↾ dom ⁡ I ∧ Edg ⁡ S ⊆ 𝒫 V
25 24 adantr ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ UHGraph ∧ V ⊆ A ∧ I ⊆ B → S SubGraph G ↔ V ⊆ A ∧ I = B ↾ dom ⁡ I ∧ Edg ⁡ S ⊆ 𝒫 V
26 9 14 22 25 mpbir3and ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ UHGraph ∧ V ⊆ A ∧ I ⊆ B → S SubGraph G
27 26 ex ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ UHGraph → V ⊆ A ∧ I ⊆ B → S SubGraph G
28 8 27 impbid2 ⊢ G ∈ W ∧ Fun ⁡ B ∧ S ∈ UHGraph → S SubGraph G ↔ V ⊆ A ∧ I ⊆ B