umgracycusgr

Description: An acyclic multigraph is a simple graph. (Contributed by BTernaryTau, 17-Oct-2023)

		Ref	Expression
	Assertion	umgracycusgr	$⊢ (G \in UMGraph \land G \in AcyclicGraph) \to G \in USGraph$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2		eqid	$⊢ iEdg (G) = iEdg (G)$
3	1 2	umgrf	$⊢ G \in UMGraph \to iEdg (G) : dom iEdg (G) ⟶ \{x \in 𝒫 Vtx (G) \| \|x\| = 2\}$
4		isacycgr	$⊢ G \in UMGraph \to (G \in AcyclicGraph \leftrightarrow \neg \exists f \exists p (f Cycles (G) p \land f \neq \emptyset))$
5	4	biimpa	$⊢ (G \in UMGraph \land G \in AcyclicGraph) \to \neg \exists f \exists p (f Cycles (G) p \land f \neq \emptyset)$
6	2	umgr2cycl	$⊢ (G \in UMGraph \land \exists j \in dom iEdg (G) \exists k \in dom iEdg (G) (iEdg (G) (j) = iEdg (G) (k) \land j \neq k)) \to \exists f \exists p (f Cycles (G) p \land \|f\| = 2)$
7		2ne0	$⊢ 2 \neq 0$
8		neeq1	$⊢ \|f\| = 2 \to (\|f\| \neq 0 \leftrightarrow 2 \neq 0)$
9	7 8	mpbiri	$⊢ \|f\| = 2 \to \|f\| \neq 0$
10		hasheq0	$⊢ f \in V \to (\|f\| = 0 \leftrightarrow f = \emptyset)$
11	10	elv	$⊢ \|f\| = 0 \leftrightarrow f = \emptyset$
12	11	necon3bii	$⊢ \|f\| \neq 0 \leftrightarrow f \neq \emptyset$
13	9 12	sylib	$⊢ \|f\| = 2 \to f \neq \emptyset$
14	13	anim2i	$⊢ (f Cycles (G) p \land \|f\| = 2) \to (f Cycles (G) p \land f \neq \emptyset)$
15	14	2eximi	$⊢ \exists f \exists p (f Cycles (G) p \land \|f\| = 2) \to \exists f \exists p (f Cycles (G) p \land f \neq \emptyset)$
16	6 15	syl	$⊢ (G \in UMGraph \land \exists j \in dom iEdg (G) \exists k \in dom iEdg (G) (iEdg (G) (j) = iEdg (G) (k) \land j \neq k)) \to \exists f \exists p (f Cycles (G) p \land f \neq \emptyset)$
17	16	ex	$⊢ G \in UMGraph \to (\exists j \in dom iEdg (G) \exists k \in dom iEdg (G) (iEdg (G) (j) = iEdg (G) (k) \land j \neq k) \to \exists f \exists p (f Cycles (G) p \land f \neq \emptyset))$
18	17	con3d	$⊢ G \in UMGraph \to (\neg \exists f \exists p (f Cycles (G) p \land f \neq \emptyset) \to \neg \exists j \in dom iEdg (G) \exists k \in dom iEdg (G) (iEdg (G) (j) = iEdg (G) (k) \land j \neq k))$
19	18	adantr	$⊢ (G \in UMGraph \land G \in AcyclicGraph) \to (\neg \exists f \exists p (f Cycles (G) p \land f \neq \emptyset) \to \neg \exists j \in dom iEdg (G) \exists k \in dom iEdg (G) (iEdg (G) (j) = iEdg (G) (k) \land j \neq k))$
20	5 19	mpd	$⊢ (G \in UMGraph \land G \in AcyclicGraph) \to \neg \exists j \in dom iEdg (G) \exists k \in dom iEdg (G) (iEdg (G) (j) = iEdg (G) (k) \land j \neq k)$
21		dff15	$⊢ iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} \{x \in 𝒫 Vtx (G) \| \|x\| = 2\} \leftrightarrow (iEdg (G) : dom iEdg (G) ⟶ \{x \in 𝒫 Vtx (G) \| \|x\| = 2\} \land \neg \exists j \in dom iEdg (G) \exists k \in dom iEdg (G) (iEdg (G) (j) = iEdg (G) (k) \land j \neq k))$
22	21	biimpri	$⊢ (iEdg (G) : dom iEdg (G) ⟶ \{x \in 𝒫 Vtx (G) \| \|x\| = 2\} \land \neg \exists j \in dom iEdg (G) \exists k \in dom iEdg (G) (iEdg (G) (j) = iEdg (G) (k) \land j \neq k)) \to iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} \{x \in 𝒫 Vtx (G) \| \|x\| = 2\}$
23	3 20 22	syl2an2r	$⊢ (G \in UMGraph \land G \in AcyclicGraph) \to iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} \{x \in 𝒫 Vtx (G) \| \|x\| = 2\}$
24	1 2	isusgrs	$⊢ G \in UMGraph \to (G \in USGraph \leftrightarrow iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} \{x \in 𝒫 Vtx (G) \| \|x\| = 2\})$
25	24	biimprd	$⊢ G \in UMGraph \to (iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} \{x \in 𝒫 Vtx (G) \| \|x\| = 2\} \to G \in USGraph)$
26	25	adantr	$⊢ (G \in UMGraph \land G \in AcyclicGraph) \to (iEdg (G) : dom iEdg (G) \underset{1-1}{⟶} \{x \in 𝒫 Vtx (G) \| \|x\| = 2\} \to G \in USGraph)$
27	23 26	mpd	$⊢ (G \in UMGraph \land G \in AcyclicGraph) \to G \in USGraph$

Metamath Proof Explorer

Theorem umgracycusgr

Proof