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 ( ( 𝐺 ∈ UHGraph ∧ 𝑆 SubGraph 𝐺 ) → 𝑆 ∈ UHGraph )

Proof

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