usgrcyclgt2v

Description: A simple graph with a non-trivial cycle must have at least 3 vertices. (Contributed by BTernaryTau, 5-Oct-2023)

		Ref	Expression
	Hypothesis	usgrcyclgt2v.1	$⊢ V = Vtx (G)$
	Assertion	usgrcyclgt2v	$⊢ (G \in USGraph \land F Cycles (G) P \land F \neq \emptyset) \to 2 < \|V\|$

Step	Hyp	Ref	Expression
1		usgrcyclgt2v.1	$⊢ V = Vtx (G)$
2		2re	$⊢ 2 \in ℝ$
3	2	rexri	$⊢ 2 \in ℝ^{*}$
4	3	a1i	$⊢ (G \in USGraph \land F Cycles (G) P \land F \neq \emptyset) \to 2 \in ℝ^{*}$
5		cycliswlk	$⊢ F Cycles (G) P \to F Walks (G) P$
6		wlkcl	$⊢ F Walks (G) P \to \|F\| \in ℕ_{0}$
7	5 6	syl	$⊢ F Cycles (G) P \to \|F\| \in ℕ_{0}$
8		nn0xnn0	$⊢ \|F\| \in ℕ_{0} \to \|F\| \in ℕ_{0}^{*}$
9		xnn0xr	$⊢ \|F\| \in ℕ_{0}^{} \to \|F\| \in ℝ^{}$
10	7 8 9	3syl	$⊢ F Cycles (G) P \to \|F\| \in ℝ^{*}$
11	10	3ad2ant2	$⊢ (G \in USGraph \land F Cycles (G) P \land F \neq \emptyset) \to \|F\| \in ℝ^{*}$
12	1	fvexi	$⊢ V \in V$
13		hashxnn0	$⊢ V \in V \to \|V\| \in ℕ_{0}^{*}$
14		xnn0xr	$⊢ \|V\| \in ℕ_{0}^{} \to \|V\| \in ℝ^{}$
15	12 13 14	mp2b	$⊢ \|V\| \in ℝ^{*}$
16	15	a1i	$⊢ (G \in USGraph \land F Cycles (G) P \land F \neq \emptyset) \to \|V\| \in ℝ^{*}$
17		usgrgt2cycl	$⊢ (G \in USGraph \land F Cycles (G) P \land F \neq \emptyset) \to 2 < \|F\|$
18		cyclispth	$⊢ F Cycles (G) P \to F Paths (G) P$
19	1	pthhashvtx	$⊢ F Paths (G) P \to \|F\| \leq \|V\|$
20	18 19	syl	$⊢ F Cycles (G) P \to \|F\| \leq \|V\|$
21	20	3ad2ant2	$⊢ (G \in USGraph \land F Cycles (G) P \land F \neq \emptyset) \to \|F\| \leq \|V\|$
22	4 11 16 17 21	xrltletrd	$⊢ (G \in USGraph \land F Cycles (G) P \land F \neq \emptyset) \to 2 < \|V\|$

Metamath Proof Explorer