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 )