acycgr0v

Description: A null graph (with no vertices) is an acyclic graph. (Contributed by BTernaryTau, 11-Oct-2023)

		Ref	Expression
	Hypothesis	acycgr0v.1	$⊢ V = Vtx (G)$
	Assertion	acycgr0v	$⊢ (G \in W \land V = \emptyset) \to G \in AcyclicGraph$

Proof

Step	Hyp	Ref	Expression
1		acycgr0v.1	$⊢ V = Vtx (G)$
2		br0	$⊢ \neg f \emptyset p$
3		df-cycls	$⊢ Cycles = (g \in V ⟼ \{⟨f, p⟩ \| (f Paths (g) p \land p (0) = p (\|f\|))\})$
4	3	relmptopab	$⊢ Rel Cycles (G)$
5		cycliswlk	$⊢ f Cycles (G) p \to f Walks (G) p$
6		df-br	$⊢ f Cycles (G) p \leftrightarrow ⟨f, p⟩ \in Cycles (G)$
7		df-br	$⊢ f Walks (G) p \leftrightarrow ⟨f, p⟩ \in Walks (G)$
8	5 6 7	3imtr3i	$⊢ ⟨f, p⟩ \in Cycles (G) \to ⟨f, p⟩ \in Walks (G)$
9	4 8	relssi	$⊢ Cycles (G) \subseteq Walks (G)$
10	1	eqeq1i	$⊢ V = \emptyset \leftrightarrow Vtx (G) = \emptyset$
11		g0wlk0	$⊢ Vtx (G) = \emptyset \to Walks (G) = \emptyset$
12	10 11	sylbi	$⊢ V = \emptyset \to Walks (G) = \emptyset$
13	9 12	sseqtrid	$⊢ V = \emptyset \to Cycles (G) \subseteq \emptyset$
14		ss0	$⊢ Cycles (G) \subseteq \emptyset \to Cycles (G) = \emptyset$
15		breq	$⊢ Cycles (G) = \emptyset \to (f Cycles (G) p \leftrightarrow f \emptyset p)$
16	15	notbid	$⊢ Cycles (G) = \emptyset \to (\neg f Cycles (G) p \leftrightarrow \neg f \emptyset p)$
17	13 14 16	3syl	$⊢ V = \emptyset \to (\neg f Cycles (G) p \leftrightarrow \neg f \emptyset p)$
18	2 17	mpbiri	$⊢ V = \emptyset \to \neg f Cycles (G) p$
19	18	intnanrd	$⊢ V = \emptyset \to \neg (f Cycles (G) p \land f \neq \emptyset)$
20	19	nexdv	$⊢ V = \emptyset \to \neg \exists p (f Cycles (G) p \land f \neq \emptyset)$
21	20	nexdv	$⊢ V = \emptyset \to \neg \exists f \exists p (f Cycles (G) p \land f \neq \emptyset)$
22		isacycgr	$⊢ G \in W \to (G \in AcyclicGraph \leftrightarrow \neg \exists f \exists p (f Cycles (G) p \land f \neq \emptyset))$
23	22	biimpar	$⊢ (G \in W \land \neg \exists f \exists p (f Cycles (G) p \land f \neq \emptyset)) \to G \in AcyclicGraph$
24	21 23	sylan2	$⊢ (G \in W \land V = \emptyset) \to G \in AcyclicGraph$

Metamath Proof Explorer

Theorem acycgr0v

Proof