Metamath Proof Explorer

Theorem subuhgr

Description: A subgraph of a hypergraph is a hypergraph. (Contributed by AV, 16-Nov-2020) (Proof shortened by AV, 21-Nov-2020)

Ref Expression
Assertion subuhgr ⊢ G ∈ UHGraph ∧ S SubGraph G → S ∈ UHGraph

Proof

Step Hyp Ref Expression
1 eqid ⊢ Vtx ⁡ S = Vtx ⁡ S
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 eqid ⊢ iEdg ⁡ S = iEdg ⁡ S
4 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
5 eqid ⊢ Edg ⁡ S = Edg ⁡ S
6 1 2 3 4 5 subgrprop2 ⊢ S SubGraph G → Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S
7 subgruhgrfun ⊢ G ∈ UHGraph ∧ S SubGraph G → Fun ⁡ iEdg ⁡ S
8 7 ancoms ⊢ S SubGraph G ∧ G ∈ UHGraph → Fun ⁡ iEdg ⁡ S
9 8 adantl ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UHGraph → Fun ⁡ iEdg ⁡ S
10 9 funfnd ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UHGraph → iEdg ⁡ S Fn dom ⁡ iEdg ⁡ S
11 simplrr ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UHGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → G ∈ UHGraph
12 simplrl ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UHGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → S SubGraph G
13 simpr ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UHGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → x ∈ dom ⁡ iEdg ⁡ S
14 1 3 11 12 13 subgruhgredgd ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UHGraph ∧ x ∈ dom ⁡ iEdg ⁡ S → iEdg ⁡ S ⁡ x ∈ 𝒫 Vtx ⁡ S ∖ ∅
15 14 ralrimiva ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UHGraph → ∀ x ∈ dom ⁡ iEdg ⁡ S iEdg ⁡ S ⁡ x ∈ 𝒫 Vtx ⁡ S ∖ ∅
16 fnfvrnss ⊢ iEdg ⁡ S Fn dom ⁡ iEdg ⁡ S ∧ ∀ x ∈ dom ⁡ iEdg ⁡ S iEdg ⁡ S ⁡ x ∈ 𝒫 Vtx ⁡ S ∖ ∅ → ran ⁡ iEdg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∖ ∅
17 10 15 16 syl2anc ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UHGraph → ran ⁡ iEdg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∖ ∅
18 df-f ⊢ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ 𝒫 Vtx ⁡ S ∖ ∅ ↔ iEdg ⁡ S Fn dom ⁡ iEdg ⁡ S ∧ ran ⁡ iEdg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∖ ∅
19 10 17 18 sylanbrc ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UHGraph → iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ 𝒫 Vtx ⁡ S ∖ ∅
20 subgrv ⊢ S SubGraph G → S ∈ V ∧ G ∈ V
21 1 3 isuhgr ⊢ S ∈ V → S ∈ UHGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ 𝒫 Vtx ⁡ S ∖ ∅
22 21 adantr ⊢ S ∈ V ∧ G ∈ V → S ∈ UHGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ 𝒫 Vtx ⁡ S ∖ ∅
23 20 22 syl ⊢ S SubGraph G → S ∈ UHGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ 𝒫 Vtx ⁡ S ∖ ∅
24 23 adantr ⊢ S SubGraph G ∧ G ∈ UHGraph → S ∈ UHGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ 𝒫 Vtx ⁡ S ∖ ∅
25 24 adantl ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UHGraph → S ∈ UHGraph ↔ iEdg ⁡ S : dom ⁡ iEdg ⁡ S ⟶ 𝒫 Vtx ⁡ S ∖ ∅
26 19 25 mpbird ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S ∧ S SubGraph G ∧ G ∈ UHGraph → S ∈ UHGraph
27 26 ex ⊢ Vtx ⁡ S ⊆ Vtx ⁡ G ∧ iEdg ⁡ S ⊆ iEdg ⁡ G ∧ Edg ⁡ S ⊆ 𝒫 Vtx ⁡ S → S SubGraph G ∧ G ∈ UHGraph → S ∈ UHGraph
28 6 27 syl ⊢ S SubGraph G → S SubGraph G ∧ G ∈ UHGraph → S ∈ UHGraph
29 28 anabsi8 ⊢ G ∈ UHGraph ∧ S SubGraph G → S ∈ UHGraph