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 ⊢ V = Vtx ⁡ G
isubgriedg.e ⊢ E = iEdg ⁡ G
Assertion isubgrvtxuhgr ⊢ G ∈ UHGraph → G ISubGr V = V E

Proof

Step Hyp Ref Expression
1 isubgriedg.v ⊢ V = Vtx ⁡ G
2 isubgriedg.e ⊢ E = iEdg ⁡ G
3 ssidd ⊢ G ∈ UHGraph → V ⊆ V
4 1 2 isisubgr ⊢ G ∈ UHGraph ∧ V ⊆ V → G ISubGr V = V E ↾ x ∈ dom ⁡ E | E ⁡ x ⊆ V
5 3 4 mpdan ⊢ G ∈ UHGraph → G ISubGr V = V E ↾ x ∈ dom ⁡ E | E ⁡ x ⊆ V
6 2 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ E
7 funrel ⊢ Fun ⁡ E → Rel ⁡ E
8 6 7 syl ⊢ G ∈ UHGraph → Rel ⁡ E
9 1 2 uhgrf ⊢ G ∈ UHGraph → E : dom ⁡ E ⟶ 𝒫 V ∖ ∅
10 ffvelcdm ⊢ E : dom ⁡ E ⟶ 𝒫 V ∖ ∅ ∧ x ∈ dom ⁡ E → E ⁡ x ∈ 𝒫 V ∖ ∅
11 eldifi ⊢ E ⁡ x ∈ 𝒫 V ∖ ∅ → E ⁡ x ∈ 𝒫 V
12 11 elpwid ⊢ E ⁡ x ∈ 𝒫 V ∖ ∅ → E ⁡ x ⊆ V
13 10 12 syl ⊢ E : dom ⁡ E ⟶ 𝒫 V ∖ ∅ ∧ x ∈ dom ⁡ E → E ⁡ x ⊆ V
14 13 rabeqcda ⊢ E : dom ⁡ E ⟶ 𝒫 V ∖ ∅ → x ∈ dom ⁡ E | E ⁡ x ⊆ V = dom ⁡ E
15 14 eqimsscd ⊢ E : dom ⁡ E ⟶ 𝒫 V ∖ ∅ → dom ⁡ E ⊆ x ∈ dom ⁡ E | E ⁡ x ⊆ V
16 9 15 syl ⊢ G ∈ UHGraph → dom ⁡ E ⊆ x ∈ dom ⁡ E | E ⁡ x ⊆ V
17 relssres ⊢ Rel ⁡ E ∧ dom ⁡ E ⊆ x ∈ dom ⁡ E | E ⁡ x ⊆ V → E ↾ x ∈ dom ⁡ E | E ⁡ x ⊆ V = E
18 8 16 17 syl2anc ⊢ G ∈ UHGraph → E ↾ x ∈ dom ⁡ E | E ⁡ x ⊆ V = E
19 18 opeq2d ⊢ G ∈ UHGraph → V E ↾ x ∈ dom ⁡ E | E ⁡ x ⊆ V = V E
20 5 19 eqtrd ⊢ G ∈ UHGraph → G ISubGr V = V E