Metamath Proof Explorer

Theorem isubgr0uhgr

Description: The subgraph induced by an empty set of vertices of a hypergraph. (Contributed by AV, 13-May-2025)

Ref Expression
Assertion isubgr0uhgr ⊢ G ∈ UHGraph → G ISubGr ∅ = ∅ ∅

Proof

Step Hyp Ref Expression
1 0ss ⊢ ∅ ⊆ Vtx ⁡ G
2 eqid ⊢ Vtx ⁡ G = Vtx ⁡ G
3 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
4 2 3 isisubgr ⊢ G ∈ UHGraph ∧ ∅ ⊆ Vtx ⁡ G → G ISubGr ∅ = ∅ iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ ∅
5 1 4 mpan2 ⊢ G ∈ UHGraph → G ISubGr ∅ = ∅ iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ ∅
6 inrab2 ⊢ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ ∅ ∩ dom ⁡ iEdg ⁡ G = x ∈ dom ⁡ iEdg ⁡ G ∩ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ ∅
7 inidm ⊢ dom ⁡ iEdg ⁡ G ∩ dom ⁡ iEdg ⁡ G = dom ⁡ iEdg ⁡ G
8 7 rabeqi ⊢ x ∈ dom ⁡ iEdg ⁡ G ∩ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ ∅ = x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ ∅
9 ss0b ⊢ iEdg ⁡ G ⁡ x ⊆ ∅ ↔ iEdg ⁡ G ⁡ x = ∅
10 8 9 rabbieq ⊢ x ∈ dom ⁡ iEdg ⁡ G ∩ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ ∅ = x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = ∅
11 6 10 eqtri ⊢ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ ∅ ∩ dom ⁡ iEdg ⁡ G = x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = ∅
12 11 ineqcomi ⊢ dom ⁡ iEdg ⁡ G ∩ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ ∅ = x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = ∅
13 2 3 uhgrf ⊢ G ∈ UHGraph → iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 𝒫 Vtx ⁡ G ∖ ∅
14 ffvelcdm ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 𝒫 Vtx ⁡ G ∖ ∅ ∧ x ∈ dom ⁡ iEdg ⁡ G → iEdg ⁡ G ⁡ x ∈ 𝒫 Vtx ⁡ G ∖ ∅
15 eldifsni ⊢ iEdg ⁡ G ⁡ x ∈ 𝒫 Vtx ⁡ G ∖ ∅ → iEdg ⁡ G ⁡ x ≠ ∅
16 14 15 syl ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 𝒫 Vtx ⁡ G ∖ ∅ ∧ x ∈ dom ⁡ iEdg ⁡ G → iEdg ⁡ G ⁡ x ≠ ∅
17 16 neneqd ⊢ iEdg ⁡ G : dom ⁡ iEdg ⁡ G ⟶ 𝒫 Vtx ⁡ G ∖ ∅ ∧ x ∈ dom ⁡ iEdg ⁡ G → ¬ iEdg ⁡ G ⁡ x = ∅
18 13 17 sylan ⊢ G ∈ UHGraph ∧ x ∈ dom ⁡ iEdg ⁡ G → ¬ iEdg ⁡ G ⁡ x = ∅
19 18 ralrimiva ⊢ G ∈ UHGraph → ∀ x ∈ dom ⁡ iEdg ⁡ G ¬ iEdg ⁡ G ⁡ x = ∅
20 rabeq0 ⊢ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = ∅ = ∅ ↔ ∀ x ∈ dom ⁡ iEdg ⁡ G ¬ iEdg ⁡ G ⁡ x = ∅
21 19 20 sylibr ⊢ G ∈ UHGraph → x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x = ∅ = ∅
22 12 21 eqtrid ⊢ G ∈ UHGraph → dom ⁡ iEdg ⁡ G ∩ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ ∅ = ∅
23 3 uhgrfun ⊢ G ∈ UHGraph → Fun ⁡ iEdg ⁡ G
24 23 funfnd ⊢ G ∈ UHGraph → iEdg ⁡ G Fn dom ⁡ iEdg ⁡ G
25 fnresdisj ⊢ iEdg ⁡ G Fn dom ⁡ iEdg ⁡ G → dom ⁡ iEdg ⁡ G ∩ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ ∅ = ∅ ↔ iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ ∅ = ∅
26 24 25 syl ⊢ G ∈ UHGraph → dom ⁡ iEdg ⁡ G ∩ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ ∅ = ∅ ↔ iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ ∅ = ∅
27 22 26 mpbid ⊢ G ∈ UHGraph → iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ ∅ = ∅
28 27 opeq2d ⊢ G ∈ UHGraph → ∅ iEdg ⁡ G ↾ x ∈ dom ⁡ iEdg ⁡ G | iEdg ⁡ G ⁡ x ⊆ ∅ = ∅ ∅
29 5 28 eqtrd ⊢ G ∈ UHGraph → G ISubGr ∅ = ∅ ∅