# Metamath Proof Explorer

## Theorem uspgrn2crct

Description: In a simple pseudograph there are no circuits with length 2 (consisting of two edges). (Contributed by Alexander van der Vekens, 9-Nov-2017) (Revised by AV, 3-Feb-2021) (Proof shortened by AV, 31-Oct-2021)

Ref Expression
Assertion uspgrn2crct ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {F}\mathrm{Circuits}\left({G}\right){P}\right)\to \left|{F}\right|\ne 2$

### Proof

Step Hyp Ref Expression
1 crctprop ${⊢}{F}\mathrm{Circuits}\left({G}\right){P}\to \left({F}\mathrm{Trails}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)$
2 istrl ${⊢}{F}\mathrm{Trails}\left({G}\right){P}↔\left({F}\mathrm{Walks}\left({G}\right){P}\wedge \mathrm{Fun}{{F}}^{-1}\right)$
3 uspgrupgr ${⊢}{G}\in \mathrm{USHGraph}\to {G}\in \mathrm{UPGraph}$
4 eqid ${⊢}\mathrm{Vtx}\left({G}\right)=\mathrm{Vtx}\left({G}\right)$
5 eqid ${⊢}\mathrm{iEdg}\left({G}\right)=\mathrm{iEdg}\left({G}\right)$
6 4 5 upgriswlk ${⊢}{G}\in \mathrm{UPGraph}\to \left({F}\mathrm{Walks}\left({G}\right){P}↔\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge {P}:\left(0\dots \left|{F}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\wedge \forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\right)\right)$
7 preq2 ${⊢}{P}\left(2\right)={P}\left(0\right)\to \left\{{P}\left(1\right),{P}\left(2\right)\right\}=\left\{{P}\left(1\right),{P}\left(0\right)\right\}$
8 prcom ${⊢}\left\{{P}\left(1\right),{P}\left(0\right)\right\}=\left\{{P}\left(0\right),{P}\left(1\right)\right\}$
9 7 8 eqtrdi ${⊢}{P}\left(2\right)={P}\left(0\right)\to \left\{{P}\left(1\right),{P}\left(2\right)\right\}=\left\{{P}\left(0\right),{P}\left(1\right)\right\}$
10 9 eqcoms ${⊢}{P}\left(0\right)={P}\left(2\right)\to \left\{{P}\left(1\right),{P}\left(2\right)\right\}=\left\{{P}\left(0\right),{P}\left(1\right)\right\}$
11 10 eqeq2d ${⊢}{P}\left(0\right)={P}\left(2\right)\to \left(\mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(1\right),{P}\left(2\right)\right\}↔\mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\right)$
12 11 anbi2d ${⊢}{P}\left(0\right)={P}\left(2\right)\to \left(\left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(1\right),{P}\left(2\right)\right\}\right)↔\left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\right)\right)$
13 12 ad2antrr ${⊢}\left(\left({P}\left(0\right)={P}\left(2\right)\wedge \left(\left|{F}\right|=2\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\right)\right)\wedge {F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \left(\left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(1\right),{P}\left(2\right)\right\}\right)↔\left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\right)\right)$
14 eqtr3 ${⊢}\left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\right)\to \mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)$
15 4 5 uspgrf ${⊢}{G}\in \mathrm{USHGraph}\to \mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)\underset{1-1}{⟶}\left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}$
16 15 adantl ${⊢}\left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\to \mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)\underset{1-1}{⟶}\left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}$
17 16 adantl ${⊢}\left(\left|{F}\right|=2\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\right)\to \mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)\underset{1-1}{⟶}\left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}$
18 17 adantr ${⊢}\left(\left(\left|{F}\right|=2\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\right)\wedge {F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)\underset{1-1}{⟶}\left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}$
19 df-f1 ${⊢}{F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}\mathrm{iEdg}\left({G}\right)↔\left({F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \mathrm{Fun}{{F}}^{-1}\right)$
20 19 simplbi2 ${⊢}{F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)\to \left(\mathrm{Fun}{{F}}^{-1}\to {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)$
21 wrdf ${⊢}{F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\to {F}:\left(0..^\left|{F}\right|\right)⟶\mathrm{dom}\mathrm{iEdg}\left({G}\right)$
22 20 21 syl11 ${⊢}\mathrm{Fun}{{F}}^{-1}\to \left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\to {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)$
23 22 adantr ${⊢}\left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\to \left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\to {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)$
24 23 adantl ${⊢}\left(\left|{F}\right|=2\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\right)\to \left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\to {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)$
25 24 imp ${⊢}\left(\left(\left|{F}\right|=2\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\right)\wedge {F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}\mathrm{iEdg}\left({G}\right)$
26 2nn ${⊢}2\in ℕ$
27 lbfzo0 ${⊢}0\in \left(0..^2\right)↔2\in ℕ$
28 26 27 mpbir ${⊢}0\in \left(0..^2\right)$
29 1nn0 ${⊢}1\in {ℕ}_{0}$
30 1lt2 ${⊢}1<2$
31 elfzo0 ${⊢}1\in \left(0..^2\right)↔\left(1\in {ℕ}_{0}\wedge 2\in ℕ\wedge 1<2\right)$
32 29 26 30 31 mpbir3an ${⊢}1\in \left(0..^2\right)$
33 28 32 pm3.2i ${⊢}\left(0\in \left(0..^2\right)\wedge 1\in \left(0..^2\right)\right)$
34 oveq2 ${⊢}\left|{F}\right|=2\to \left(0..^\left|{F}\right|\right)=\left(0..^2\right)$
35 34 eleq2d ${⊢}\left|{F}\right|=2\to \left(0\in \left(0..^\left|{F}\right|\right)↔0\in \left(0..^2\right)\right)$
36 34 eleq2d ${⊢}\left|{F}\right|=2\to \left(1\in \left(0..^\left|{F}\right|\right)↔1\in \left(0..^2\right)\right)$
37 35 36 anbi12d ${⊢}\left|{F}\right|=2\to \left(\left(0\in \left(0..^\left|{F}\right|\right)\wedge 1\in \left(0..^\left|{F}\right|\right)\right)↔\left(0\in \left(0..^2\right)\wedge 1\in \left(0..^2\right)\right)\right)$
38 33 37 mpbiri ${⊢}\left|{F}\right|=2\to \left(0\in \left(0..^\left|{F}\right|\right)\wedge 1\in \left(0..^\left|{F}\right|\right)\right)$
39 38 ad2antrr ${⊢}\left(\left(\left|{F}\right|=2\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\right)\wedge {F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \left(0\in \left(0..^\left|{F}\right|\right)\wedge 1\in \left(0..^\left|{F}\right|\right)\right)$
40 f1cofveqaeq ${⊢}\left(\left(\mathrm{iEdg}\left({G}\right):\mathrm{dom}\mathrm{iEdg}\left({G}\right)\underset{1-1}{⟶}\left\{{x}\in \left(𝒫\mathrm{Vtx}\left({G}\right)\setminus \left\{\varnothing \right\}\right)|\left|{x}\right|\le 2\right\}\wedge {F}:\left(0..^\left|{F}\right|\right)\underset{1-1}{⟶}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\wedge \left(0\in \left(0..^\left|{F}\right|\right)\wedge 1\in \left(0..^\left|{F}\right|\right)\right)\right)\to \left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)\to 0=1\right)$
41 18 25 39 40 syl21anc ${⊢}\left(\left(\left|{F}\right|=2\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\right)\wedge {F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)\to 0=1\right)$
42 0ne1 ${⊢}0\ne 1$
43 eqneqall ${⊢}0=1\to \left(0\ne 1\to {P}\left(0\right)\ne {P}\left(2\right)\right)$
44 41 42 43 syl6mpi ${⊢}\left(\left(\left|{F}\right|=2\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\right)\wedge {F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)\to {P}\left(0\right)\ne {P}\left(2\right)\right)$
45 44 adantll ${⊢}\left(\left({P}\left(0\right)={P}\left(2\right)\wedge \left(\left|{F}\right|=2\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\right)\right)\wedge {F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)\to {P}\left(0\right)\ne {P}\left(2\right)\right)$
46 14 45 syl5 ${⊢}\left(\left({P}\left(0\right)={P}\left(2\right)\wedge \left(\left|{F}\right|=2\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\right)\right)\wedge {F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \left(\left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\right)\to {P}\left(0\right)\ne {P}\left(2\right)\right)$
47 13 46 sylbid ${⊢}\left(\left({P}\left(0\right)={P}\left(2\right)\wedge \left(\left|{F}\right|=2\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\right)\right)\wedge {F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\right)\to \left(\left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(1\right),{P}\left(2\right)\right\}\right)\to {P}\left(0\right)\ne {P}\left(2\right)\right)$
48 47 expimpd ${⊢}\left({P}\left(0\right)={P}\left(2\right)\wedge \left(\left|{F}\right|=2\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\right)\right)\to \left(\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(1\right),{P}\left(2\right)\right\}\right)\right)\to {P}\left(0\right)\ne {P}\left(2\right)\right)$
49 48 ex ${⊢}{P}\left(0\right)={P}\left(2\right)\to \left(\left(\left|{F}\right|=2\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\right)\to \left(\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(1\right),{P}\left(2\right)\right\}\right)\right)\to {P}\left(0\right)\ne {P}\left(2\right)\right)\right)$
50 2a1 ${⊢}{P}\left(0\right)\ne {P}\left(2\right)\to \left(\left(\left|{F}\right|=2\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\right)\to \left(\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(1\right),{P}\left(2\right)\right\}\right)\right)\to {P}\left(0\right)\ne {P}\left(2\right)\right)\right)$
51 49 50 pm2.61ine ${⊢}\left(\left|{F}\right|=2\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\right)\to \left(\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(1\right),{P}\left(2\right)\right\}\right)\right)\to {P}\left(0\right)\ne {P}\left(2\right)\right)$
52 fzo0to2pr ${⊢}\left(0..^2\right)=\left\{0,1\right\}$
53 34 52 eqtrdi ${⊢}\left|{F}\right|=2\to \left(0..^\left|{F}\right|\right)=\left\{0,1\right\}$
54 53 raleqdv ${⊢}\left|{F}\right|=2\to \left(\forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}↔\forall {k}\in \left\{0,1\right\}\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\right)$
55 2wlklem ${⊢}\forall {k}\in \left\{0,1\right\}\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}↔\left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(1\right),{P}\left(2\right)\right\}\right)$
56 54 55 syl6bb ${⊢}\left|{F}\right|=2\to \left(\forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}↔\left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(1\right),{P}\left(2\right)\right\}\right)\right)$
57 56 anbi2d ${⊢}\left|{F}\right|=2\to \left(\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\right)↔\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(1\right),{P}\left(2\right)\right\}\right)\right)\right)$
58 fveq2 ${⊢}\left|{F}\right|=2\to {P}\left(\left|{F}\right|\right)={P}\left(2\right)$
59 58 neeq2d ${⊢}\left|{F}\right|=2\to \left({P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)↔{P}\left(0\right)\ne {P}\left(2\right)\right)$
60 57 59 imbi12d ${⊢}\left|{F}\right|=2\to \left(\left(\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\right)\to {P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)\right)↔\left(\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(1\right),{P}\left(2\right)\right\}\right)\right)\to {P}\left(0\right)\ne {P}\left(2\right)\right)\right)$
61 60 adantr ${⊢}\left(\left|{F}\right|=2\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\right)\to \left(\left(\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\right)\to {P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)\right)↔\left(\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \left(\mathrm{iEdg}\left({G}\right)\left({F}\left(0\right)\right)=\left\{{P}\left(0\right),{P}\left(1\right)\right\}\wedge \mathrm{iEdg}\left({G}\right)\left({F}\left(1\right)\right)=\left\{{P}\left(1\right),{P}\left(2\right)\right\}\right)\right)\to {P}\left(0\right)\ne {P}\left(2\right)\right)\right)$
62 51 61 mpbird ${⊢}\left(\left|{F}\right|=2\wedge \left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\right)\to \left(\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\right)\to {P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)\right)$
63 62 ex ${⊢}\left|{F}\right|=2\to \left(\left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\to \left(\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\right)\to {P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)\right)\right)$
64 63 com13 ${⊢}\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\right)\to \left(\left(\mathrm{Fun}{{F}}^{-1}\wedge {G}\in \mathrm{USHGraph}\right)\to \left(\left|{F}\right|=2\to {P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)\right)\right)$
65 64 expd ${⊢}\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge \forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\right)\to \left(\mathrm{Fun}{{F}}^{-1}\to \left({G}\in \mathrm{USHGraph}\to \left(\left|{F}\right|=2\to {P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)\right)\right)\right)$
66 65 3adant2 ${⊢}\left({F}\in \mathrm{Word}\mathrm{dom}\mathrm{iEdg}\left({G}\right)\wedge {P}:\left(0\dots \left|{F}\right|\right)⟶\mathrm{Vtx}\left({G}\right)\wedge \forall {k}\in \left(0..^\left|{F}\right|\right)\phantom{\rule{.4em}{0ex}}\mathrm{iEdg}\left({G}\right)\left({F}\left({k}\right)\right)=\left\{{P}\left({k}\right),{P}\left({k}+1\right)\right\}\right)\to \left(\mathrm{Fun}{{F}}^{-1}\to \left({G}\in \mathrm{USHGraph}\to \left(\left|{F}\right|=2\to {P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)\right)\right)\right)$
67 6 66 syl6bi ${⊢}{G}\in \mathrm{UPGraph}\to \left({F}\mathrm{Walks}\left({G}\right){P}\to \left(\mathrm{Fun}{{F}}^{-1}\to \left({G}\in \mathrm{USHGraph}\to \left(\left|{F}\right|=2\to {P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)\right)\right)\right)\right)$
68 67 impd ${⊢}{G}\in \mathrm{UPGraph}\to \left(\left({F}\mathrm{Walks}\left({G}\right){P}\wedge \mathrm{Fun}{{F}}^{-1}\right)\to \left({G}\in \mathrm{USHGraph}\to \left(\left|{F}\right|=2\to {P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)\right)\right)\right)$
69 68 com23 ${⊢}{G}\in \mathrm{UPGraph}\to \left({G}\in \mathrm{USHGraph}\to \left(\left({F}\mathrm{Walks}\left({G}\right){P}\wedge \mathrm{Fun}{{F}}^{-1}\right)\to \left(\left|{F}\right|=2\to {P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)\right)\right)\right)$
70 3 69 mpcom ${⊢}{G}\in \mathrm{USHGraph}\to \left(\left({F}\mathrm{Walks}\left({G}\right){P}\wedge \mathrm{Fun}{{F}}^{-1}\right)\to \left(\left|{F}\right|=2\to {P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)\right)\right)$
71 70 com12 ${⊢}\left({F}\mathrm{Walks}\left({G}\right){P}\wedge \mathrm{Fun}{{F}}^{-1}\right)\to \left({G}\in \mathrm{USHGraph}\to \left(\left|{F}\right|=2\to {P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)\right)\right)$
72 2 71 sylbi ${⊢}{F}\mathrm{Trails}\left({G}\right){P}\to \left({G}\in \mathrm{USHGraph}\to \left(\left|{F}\right|=2\to {P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)\right)\right)$
73 72 imp ${⊢}\left({F}\mathrm{Trails}\left({G}\right){P}\wedge {G}\in \mathrm{USHGraph}\right)\to \left(\left|{F}\right|=2\to {P}\left(0\right)\ne {P}\left(\left|{F}\right|\right)\right)$
74 73 necon2d ${⊢}\left({F}\mathrm{Trails}\left({G}\right){P}\wedge {G}\in \mathrm{USHGraph}\right)\to \left({P}\left(0\right)={P}\left(\left|{F}\right|\right)\to \left|{F}\right|\ne 2\right)$
75 74 impancom ${⊢}\left({F}\mathrm{Trails}\left({G}\right){P}\wedge {P}\left(0\right)={P}\left(\left|{F}\right|\right)\right)\to \left({G}\in \mathrm{USHGraph}\to \left|{F}\right|\ne 2\right)$
76 1 75 syl ${⊢}{F}\mathrm{Circuits}\left({G}\right){P}\to \left({G}\in \mathrm{USHGraph}\to \left|{F}\right|\ne 2\right)$
77 76 impcom ${⊢}\left({G}\in \mathrm{USHGraph}\wedge {F}\mathrm{Circuits}\left({G}\right){P}\right)\to \left|{F}\right|\ne 2$