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	syl5bi	⊢ ( 𝐺 ∈ UHGraph → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑒 ∈ 𝐸 ¬ 𝑣 ∈ 𝑒 → ¬ 𝐸 ≠ ∅ ) )
33		nne	⊢ ( ¬ 𝐸 ≠ ∅ ↔ 𝐸 = ∅ )
34	32 33	syl6ib	⊢ ( 𝐺 ∈ UHGraph → ( ∀ 𝑣 ∈ 𝑉 ∀ 𝑒 ∈ 𝐸 ¬ 𝑣 ∈ 𝑒 → 𝐸 = ∅ ) )
35	7 34	sylbid	⊢ ( 𝐺 ∈ UHGraph → ( ∀ 𝑣 ∈ 𝑉 ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑣 ) = 0 → 𝐸 = ∅ ) )