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

Metamath Proof Explorer

Theorem uhgrvd00

Description: If every vertex in a hypergraph has degree 0, there is no edge in the graph. (Contributed by Alexander van der Vekens, 12-Jul-2018) (Revised by AV, 24-Dec-2020)

Ref Expression
Hypotheses vtxdusgradjvtx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
vtxdusgradjvtx.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion uhgrvd00 ( 𝐺 ∈ UHGraph → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 → 𝐸 = ∅ ) )

Proof

Step Hyp Ref Expression
1 vtxdusgradjvtx.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 vtxdusgradjvtx.e ⊢ 𝐸 = ( Edg ‘ 𝐺 )
3 eqid ⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
4 1 2 3 vtxduhgr0edgnel ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑣 ∈ 𝑉 ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 ↔ ¬ ∃ 𝑒 ∈ 𝐸 𝑣 ∈ 𝑒 ) )
5 ralnex ⊢ ( ∀ 𝑒 ∈ 𝐸 ¬ 𝑣 ∈ 𝑒 ↔ ¬ ∃ 𝑒 ∈ 𝐸 𝑣 ∈ 𝑒 )
6 4 5 bitr4di ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑣 ∈ 𝑉 ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 ↔ ∀ 𝑒 ∈ 𝐸 ¬ 𝑣 ∈ 𝑒 ) )
7 6 ralbidva ⊢ ( 𝐺 ∈ UHGraph → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 ↔ ∀ 𝑣 ∈ 𝑉 ∀ 𝑒 ∈ 𝐸 ¬ 𝑣 ∈ 𝑒 ) )
8 ralcom ⊢ ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑒 ∈ 𝐸 ¬ 𝑣 ∈ 𝑒 ↔ ∀ 𝑒 ∈ 𝐸 ∀ 𝑣 ∈ 𝑉 ¬ 𝑣 ∈ 𝑒 )
9 ralnex2 ⊢ ( ∀ 𝑒 ∈ 𝐸 ∀ 𝑣 ∈ 𝑉 ¬ 𝑣 ∈ 𝑒 ↔ ¬ ∃ 𝑒 ∈ 𝐸 ∃ 𝑣 ∈ 𝑉 𝑣 ∈ 𝑒 )
10 8 9 bitri ⊢ ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑒 ∈ 𝐸 ¬ 𝑣 ∈ 𝑒 ↔ ¬ ∃ 𝑒 ∈ 𝐸 ∃ 𝑣 ∈ 𝑉 𝑣 ∈ 𝑒 )
11 simpr ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ∈ 𝐸 )
12 2 eleq2i ⊢ ( 𝑒 ∈ 𝐸 ↔ 𝑒 ∈ ( Edg ‘ 𝐺 ) )
13 uhgredgn0 ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑒 ∈ ( Edg ‘ 𝐺 ) ) → 𝑒 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
14 12 13 sylan2b ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑒 ∈ 𝐸 ) → 𝑒 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) )
15 eldifsn ⊢ ( 𝑒 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) ↔ ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝑒 ≠ ∅ ) )
16 elpwi ⊢ ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) → 𝑒 ⊆ ( Vtx ‘ 𝐺 ) )
17 1 sseq2i ⊢ ( 𝑒 ⊆ 𝑉 ↔ 𝑒 ⊆ ( Vtx ‘ 𝐺 ) )
18 ssn0rex ⊢ ( ( 𝑒 ⊆ 𝑉 ∧ 𝑒 ≠ ∅ ) → ∃ 𝑣 ∈ 𝑉 𝑣 ∈ 𝑒 )
19 18 ex ⊢ ( 𝑒 ⊆ 𝑉 → ( 𝑒 ≠ ∅ → ∃ 𝑣 ∈ 𝑉 𝑣 ∈ 𝑒 ) )
20 17 19 sylbir ⊢ ( 𝑒 ⊆ ( Vtx ‘ 𝐺 ) → ( 𝑒 ≠ ∅ → ∃ 𝑣 ∈ 𝑉 𝑣 ∈ 𝑒 ) )
21 16 20 syl ⊢ ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) → ( 𝑒 ≠ ∅ → ∃ 𝑣 ∈ 𝑉 𝑣 ∈ 𝑒 ) )
22 21 imp ⊢ ( ( 𝑒 ∈ 𝒫 ( Vtx ‘ 𝐺 ) ∧ 𝑒 ≠ ∅ ) → ∃ 𝑣 ∈ 𝑉 𝑣 ∈ 𝑒 )
23 15 22 sylbi ⊢ ( 𝑒 ∈ ( 𝒫 ( Vtx ‘ 𝐺 ) ∖ { ∅ } ) → ∃ 𝑣 ∈ 𝑉 𝑣 ∈ 𝑒 )
24 14 23 syl ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑒 ∈ 𝐸 ) → ∃ 𝑣 ∈ 𝑉 𝑣 ∈ 𝑒 )
25 11 24 jca ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝑒 ∈ 𝐸 ) → ( 𝑒 ∈ 𝐸 ∧ ∃ 𝑣 ∈ 𝑉 𝑣 ∈ 𝑒 ) )
26 25 ex ⊢ ( 𝐺 ∈ UHGraph → ( 𝑒 ∈ 𝐸 → ( 𝑒 ∈ 𝐸 ∧ ∃ 𝑣 ∈ 𝑉 𝑣 ∈ 𝑒 ) ) )
27 26 eximdv ⊢ ( 𝐺 ∈ UHGraph → ( ∃ 𝑒 𝑒 ∈ 𝐸 → ∃ 𝑒 ( 𝑒 ∈ 𝐸 ∧ ∃ 𝑣 ∈ 𝑉 𝑣 ∈ 𝑒 ) ) )
28 n0 ⊢ ( 𝐸 ≠ ∅ ↔ ∃ 𝑒 𝑒 ∈ 𝐸 )
29 df-rex ⊢ ( ∃ 𝑒 ∈ 𝐸 ∃ 𝑣 ∈ 𝑉 𝑣 ∈ 𝑒 ↔ ∃ 𝑒 ( 𝑒 ∈ 𝐸 ∧ ∃ 𝑣 ∈ 𝑉 𝑣 ∈ 𝑒 ) )
30 27 28 29 3imtr4g ⊢ ( 𝐺 ∈ UHGraph → ( 𝐸 ≠ ∅ → ∃ 𝑒 ∈ 𝐸 ∃ 𝑣 ∈ 𝑉 𝑣 ∈ 𝑒 ) )
31 30 con3d ⊢ ( 𝐺 ∈ UHGraph → ( ¬ ∃ 𝑒 ∈ 𝐸 ∃ 𝑣 ∈ 𝑉 𝑣 ∈ 𝑒 → ¬ 𝐸 ≠ ∅ ) )
32 10 31 biimtrid ⊢ ( 𝐺 ∈ UHGraph → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑒 ∈ 𝐸 ¬ 𝑣 ∈ 𝑒 → ¬ 𝐸 ≠ ∅ ) )
33 nne ⊢ ( ¬ 𝐸 ≠ ∅ ↔ 𝐸 = ∅ )
34 32 33 imbitrdi ⊢ ( 𝐺 ∈ UHGraph → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑒 ∈ 𝐸 ¬ 𝑣 ∈ 𝑒 → 𝐸 = ∅ ) )
35 7 34 sylbid ⊢ ( 𝐺 ∈ UHGraph → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 → 𝐸 = ∅ ) )