Metamath Proof Explorer


Theorem acycgr2v

Description: A simple graph with two vertices is an acyclic graph. (Contributed by BTernaryTau, 12-Oct-2023)

Ref Expression
Hypothesis acycgrv.1 V=VtxG
Assertion acycgr2v GUSGraphV=2GAcyclicGraph

Proof

Step Hyp Ref Expression
1 acycgrv.1 V=VtxG
2 1 usgrcyclgt2v GUSGraphfCyclesGpf2<V
3 2re 2
4 3 rexri 2*
5 1 fvexi VV
6 hashxrcl VVV*
7 5 6 ax-mp V*
8 xrltne 2*V*2<VV2
9 4 7 8 mp3an12 2<VV2
10 9 neneqd 2<V¬V=2
11 2 10 syl GUSGraphfCyclesGpf¬V=2
12 11 3expib GUSGraphfCyclesGpf¬V=2
13 12 con2d GUSGraphV=2¬fCyclesGpf
14 13 imp GUSGraphV=2¬fCyclesGpf
15 14 nexdv GUSGraphV=2¬pfCyclesGpf
16 15 nexdv GUSGraphV=2¬fpfCyclesGpf
17 isacycgr GUSGraphGAcyclicGraph¬fpfCyclesGpf
18 17 adantr GUSGraphV=2GAcyclicGraph¬fpfCyclesGpf
19 16 18 mpbird GUSGraphV=2GAcyclicGraph