This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isubgruhgr

Description: An induced subgraph of a hypergraph is a hypergraph. (Contributed by AV, 13-May-2025)

Ref Expression
Hypothesis isubgrvtx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion isubgruhgr ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) ∈ UHGraph )

Proof

Step Hyp Ref Expression
1 isubgrvtx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 eqid ⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
3 1 2 uhgrf ⊢ ( 𝐺 ∈ UHGraph → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
4 3 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
5 dmresss ⊢ dom ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ⊆ dom ( iEdg ‘ 𝐺 )
6 5 a1i ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → dom ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ⊆ dom ( iEdg ‘ 𝐺 ) )
7 imadmres ⊢ ( ( iEdg ‘ 𝐺 ) “ dom ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ) = ( ( iEdg ‘ 𝐺 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } )
8 ffvelcdm ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) )
9 eldifsni ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ≠ ∅ )
10 8 9 syl ⊢ ( ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ≠ ∅ )
11 10 ex ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝐺 ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ≠ ∅ ) )
12 3 11 syl ⊢ ( 𝐺 ∈ UHGraph → ( 𝑦 ∈ dom ( iEdg ‘ 𝐺 ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ≠ ∅ ) )
13 12 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝑦 ∈ dom ( iEdg ‘ 𝐺 ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ≠ ∅ ) )
14 13 imp ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ≠ ∅ )
15 fvexd ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ⊆ 𝑆 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ∈ V )
16 id ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ⊆ 𝑆 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ⊆ 𝑆 )
17 15 16 elpwd ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ⊆ 𝑆 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝒫 𝑆 )
18 14 17 anim12ci ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ⊆ 𝑆 ) → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝒫 𝑆 ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ≠ ∅ ) )
19 eldifsn ⊢ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( 𝒫 𝑆 ∖ { ∅ } ) ↔ ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝒫 𝑆 ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ≠ ∅ ) )
20 18 19 sylibr ⊢ ( ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝐺 ) ) ∧ ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ⊆ 𝑆 ) → ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( 𝒫 𝑆 ∖ { ∅ } ) )
21 20 ex ⊢ ( ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) ∧ 𝑦 ∈ dom ( iEdg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ⊆ 𝑆 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( 𝒫 𝑆 ∖ { ∅ } ) ) )
22 21 ralrimiva ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ∀ 𝑦 ∈ dom ( iEdg ‘ 𝐺 ) ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ⊆ 𝑆 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( 𝒫 𝑆 ∖ { ∅ } ) ) )
23 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) = ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) )
24 23 sseq1d ⊢ ( 𝑥 = 𝑦 → ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 ↔ ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ⊆ 𝑆 ) )
25 24 ralrab ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( 𝒫 𝑆 ∖ { ∅ } ) ↔ ∀ 𝑦 ∈ dom ( iEdg ‘ 𝐺 ) ( ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ⊆ 𝑆 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( 𝒫 𝑆 ∖ { ∅ } ) ) )
26 22 25 sylibr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ∀ 𝑦 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( 𝒫 𝑆 ∖ { ∅ } ) )
27 ffun ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) → Fun ( iEdg ‘ 𝐺 ) )
28 ssrab2 ⊢ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ⊆ dom ( iEdg ‘ 𝐺 )
29 27 28 jctir ⊢ ( ( iEdg ‘ 𝐺 ) : dom ( iEdg ‘ 𝐺 ) ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) → ( Fun ( iEdg ‘ 𝐺 ) ∧ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ⊆ dom ( iEdg ‘ 𝐺 ) ) )
30 3 29 syl ⊢ ( 𝐺 ∈ UHGraph → ( Fun ( iEdg ‘ 𝐺 ) ∧ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ⊆ dom ( iEdg ‘ 𝐺 ) ) )
31 30 adantr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( Fun ( iEdg ‘ 𝐺 ) ∧ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ⊆ dom ( iEdg ‘ 𝐺 ) ) )
32 funimass4 ⊢ ( ( Fun ( iEdg ‘ 𝐺 ) ∧ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ⊆ dom ( iEdg ‘ 𝐺 ) ) → ( ( ( iEdg ‘ 𝐺 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ⊆ ( 𝒫 𝑆 ∖ { ∅ } ) ↔ ∀ 𝑦 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( 𝒫 𝑆 ∖ { ∅ } ) ) )
33 31 32 syl ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( ( ( iEdg ‘ 𝐺 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ⊆ ( 𝒫 𝑆 ∖ { ∅ } ) ↔ ∀ 𝑦 ∈ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ( ( iEdg ‘ 𝐺 ) ‘ 𝑦 ) ∈ ( 𝒫 𝑆 ∖ { ∅ } ) ) )
34 26 33 mpbird ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( ( iEdg ‘ 𝐺 ) “ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ⊆ ( 𝒫 𝑆 ∖ { ∅ } ) )
35 7 34 eqsstrid ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( ( iEdg ‘ 𝐺 ) “ dom ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ) ⊆ ( 𝒫 𝑆 ∖ { ∅ } ) )
36 4 6 35 fssrescdmd ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( ( iEdg ‘ 𝐺 ) ↾ dom ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ) : dom ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ⟶ ( 𝒫 𝑆 ∖ { ∅ } ) )
37 resdmres ⊢ ( ( iEdg ‘ 𝐺 ) ↾ dom ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ) = ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } )
38 37 eqcomi ⊢ ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) = ( ( iEdg ‘ 𝐺 ) ↾ dom ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) )
39 38 feq1i ⊢ ( ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) : dom ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ⟶ ( 𝒫 𝑆 ∖ { ∅ } ) ↔ ( ( iEdg ‘ 𝐺 ) ↾ dom ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ) : dom ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ⟶ ( 𝒫 𝑆 ∖ { ∅ } ) )
40 36 39 sylibr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) : dom ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ⟶ ( 𝒫 𝑆 ∖ { ∅ } ) )
41 1 2 isubgriedg ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) = ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) )
42 41 dmeqd ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → dom ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) = dom ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) )
43 1 isubgrvtx ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( Vtx ‘ ( 𝐺 ISubGr 𝑆 ) ) = 𝑆 )
44 43 pweqd ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → 𝒫 ( Vtx ‘ ( 𝐺 ISubGr 𝑆 ) ) = 𝒫 𝑆 )
45 44 difeq1d ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝒫 ( Vtx ‘ ( 𝐺 ISubGr 𝑆 ) ) ∖ { ∅ } ) = ( 𝒫 𝑆 ∖ { ∅ } ) )
46 41 42 45 feq123d ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) : dom ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) ⟶ ( 𝒫 ( Vtx ‘ ( 𝐺 ISubGr 𝑆 ) ) ∖ { ∅ } ) ↔ ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) : dom ( ( iEdg ‘ 𝐺 ) ↾ { 𝑥 ∈ dom ( iEdg ‘ 𝐺 ) ∣ ( ( iEdg ‘ 𝐺 ) ‘ 𝑥 ) ⊆ 𝑆 } ) ⟶ ( 𝒫 𝑆 ∖ { ∅ } ) ) )
47 40 46 mpbird ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) : dom ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) ⟶ ( 𝒫 ( Vtx ‘ ( 𝐺 ISubGr 𝑆 ) ) ∖ { ∅ } ) )
48 ovexd ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) ∈ V )
49 eqid ⊢ ( Vtx ‘ ( 𝐺 ISubGr 𝑆 ) ) = ( Vtx ‘ ( 𝐺 ISubGr 𝑆 ) )
50 eqid ⊢ ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) = ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) )
51 49 50 isuhgr ⊢ ( ( 𝐺 ISubGr 𝑆 ) ∈ V → ( ( 𝐺 ISubGr 𝑆 ) ∈ UHGraph ↔ ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) : dom ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) ⟶ ( 𝒫 ( Vtx ‘ ( 𝐺 ISubGr 𝑆 ) ) ∖ { ∅ } ) ) )
52 48 51 syl ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( ( 𝐺 ISubGr 𝑆 ) ∈ UHGraph ↔ ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) : dom ( iEdg ‘ ( 𝐺 ISubGr 𝑆 ) ) ⟶ ( 𝒫 ( Vtx ‘ ( 𝐺 ISubGr 𝑆 ) ) ∖ { ∅ } ) ) )
53 47 52 mpbird ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑆 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑆 ) ∈ UHGraph )