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

Metamath Proof Explorer

Theorem isubgrvtxuhgr

Description: The subgraph induced by the full set of vertices of a hypergraph. (Contributed by AV, 12-May-2025)

Ref Expression
Hypotheses isubgriedg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
isubgriedg.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion isubgrvtxuhgr ( 𝐺 ∈ UHGraph → ( 𝐺 ISubGr 𝑉 ) = ⟨ 𝑉 , 𝐸 ⟩ )

Proof

Step Hyp Ref Expression
1 isubgriedg.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 isubgriedg.e ⊢ 𝐸 = ( iEdg ‘ 𝐺 )
3 ssidd ⊢ ( 𝐺 ∈ UHGraph → 𝑉 ⊆ 𝑉 )
4 1 2 isisubgr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑉 ⊆ 𝑉 ) → ( 𝐺 ISubGr 𝑉 ) = ⟨ 𝑉 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } ) ⟩ )
5 3 4 mpdan ⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 ISubGr 𝑉 ) = ⟨ 𝑉 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } ) ⟩ )
6 2 uhgrfun ⊢ ( 𝐺 ∈ UHGraph → Fun 𝐸 )
7 funrel ⊢ ( Fun 𝐸 → Rel 𝐸 )
8 6 7 syl ⊢ ( 𝐺 ∈ UHGraph → Rel 𝐸 )
9 1 2 uhgrf ⊢ ( 𝐺 ∈ UHGraph → 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) )
10 ffvelcdm ⊢ ( ( 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ 𝑥 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) )
11 eldifi ⊢ ( ( 𝐸 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → ( 𝐸 ‘ 𝑥 ) ∈ 𝒫 𝑉 )
12 11 elpwid ⊢ ( ( 𝐸 ‘ 𝑥 ) ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 )
13 10 12 syl ⊢ ( ( 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ 𝑥 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 )
14 13 rabeqcda ⊢ ( 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) → { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } = dom 𝐸 )
15 14 eqimsscd ⊢ ( 𝐸 : dom 𝐸 ⟶ ( 𝒫 𝑉 ∖ { ∅ } ) → dom 𝐸 ⊆ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } )
16 9 15 syl ⊢ ( 𝐺 ∈ UHGraph → dom 𝐸 ⊆ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } )
17 relssres ⊢ ( ( Rel 𝐸 ∧ dom 𝐸 ⊆ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } ) → ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } ) = 𝐸 )
18 8 16 17 syl2anc ⊢ ( 𝐺 ∈ UHGraph → ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } ) = 𝐸 )
19 18 opeq2d ⊢ ( 𝐺 ∈ UHGraph → ⟨ 𝑉 , ( 𝐸 ↾ { 𝑥 ∈ dom 𝐸 ∣ ( 𝐸 ‘ 𝑥 ) ⊆ 𝑉 } ) ⟩ = ⟨ 𝑉 , 𝐸 ⟩ )
20 5 19 eqtrd ⊢ ( 𝐺 ∈ UHGraph → ( 𝐺 ISubGr 𝑉 ) = ⟨ 𝑉 , 𝐸 ⟩ )