Metamath Proof Explorer

Theorem vtxduhgr0nedg

Description: If a vertex in a hypergraph has degree 0, the vertex is not adjacent to another vertex via an edge. (Contributed by Alexander van der Vekens, 8-Dec-2017) (Revised by AV, 15-Dec-2020) (Proof shortened by AV, 24-Dec-2020)

Ref Expression
Hypotheses vtxdushgrfvedg.v ⊢ V = Vtx ⁡ G
vtxdushgrfvedg.e ⊢ E = Edg ⁡ G
vtxdushgrfvedg.d ⊢ D = VtxDeg ⁡ G
Assertion vtxduhgr0nedg ⊢ G ∈ UHGraph ∧ U ∈ V ∧ D ⁡ U = 0 → ¬ ∃ v ∈ V U v ∈ E

Proof

Step Hyp Ref Expression
1 vtxdushgrfvedg.v ⊢ V = Vtx ⁡ G
2 vtxdushgrfvedg.e ⊢ E = Edg ⁡ G
3 vtxdushgrfvedg.d ⊢ D = VtxDeg ⁡ G
4 eqid ⊢ iEdg ⁡ G = iEdg ⁡ G
5 1 4 3 vtxd0nedgb ⊢ U ∈ V → D ⁡ U = 0 ↔ ¬ ∃ i ∈ dom ⁡ iEdg ⁡ G U ∈ iEdg ⁡ G ⁡ i
6 5 adantl ⊢ G ∈ UHGraph ∧ U ∈ V → D ⁡ U = 0 ↔ ¬ ∃ i ∈ dom ⁡ iEdg ⁡ G U ∈ iEdg ⁡ G ⁡ i
7 2 eleq2i ⊢ U v ∈ E ↔ U v ∈ Edg ⁡ G
8 4 uhgredgiedgb ⊢ G ∈ UHGraph → U v ∈ Edg ⁡ G ↔ ∃ i ∈ dom ⁡ iEdg ⁡ G U v = iEdg ⁡ G ⁡ i
9 7 8 syl5bb ⊢ G ∈ UHGraph → U v ∈ E ↔ ∃ i ∈ dom ⁡ iEdg ⁡ G U v = iEdg ⁡ G ⁡ i
10 9 adantr ⊢ G ∈ UHGraph ∧ U ∈ V → U v ∈ E ↔ ∃ i ∈ dom ⁡ iEdg ⁡ G U v = iEdg ⁡ G ⁡ i
11 prid1g ⊢ U ∈ V → U ∈ U v
12 eleq2 ⊢ U v = iEdg ⁡ G ⁡ i → U ∈ U v ↔ U ∈ iEdg ⁡ G ⁡ i
13 11 12 syl5ibcom ⊢ U ∈ V → U v = iEdg ⁡ G ⁡ i → U ∈ iEdg ⁡ G ⁡ i
14 13 adantl ⊢ G ∈ UHGraph ∧ U ∈ V → U v = iEdg ⁡ G ⁡ i → U ∈ iEdg ⁡ G ⁡ i
15 14 reximdv ⊢ G ∈ UHGraph ∧ U ∈ V → ∃ i ∈ dom ⁡ iEdg ⁡ G U v = iEdg ⁡ G ⁡ i → ∃ i ∈ dom ⁡ iEdg ⁡ G U ∈ iEdg ⁡ G ⁡ i
16 10 15 sylbid ⊢ G ∈ UHGraph ∧ U ∈ V → U v ∈ E → ∃ i ∈ dom ⁡ iEdg ⁡ G U ∈ iEdg ⁡ G ⁡ i
17 16 rexlimdvw ⊢ G ∈ UHGraph ∧ U ∈ V → ∃ v ∈ V U v ∈ E → ∃ i ∈ dom ⁡ iEdg ⁡ G U ∈ iEdg ⁡ G ⁡ i
18 17 con3d ⊢ G ∈ UHGraph ∧ U ∈ V → ¬ ∃ i ∈ dom ⁡ iEdg ⁡ G U ∈ iEdg ⁡ G ⁡ i → ¬ ∃ v ∈ V U v ∈ E
19 6 18 sylbid ⊢ G ∈ UHGraph ∧ U ∈ V → D ⁡ U = 0 → ¬ ∃ v ∈ V U v ∈ E
20 19 3impia ⊢ G ∈ UHGraph ∧ U ∈ V ∧ D ⁡ U = 0 → ¬ ∃ v ∈ V U v ∈ E