Metamath Proof Explorer

Theorem clwlkl1loop

Description: A closed walk of length 1 is a loop. (Contributed by AV, 22-Apr-2021)

Ref Expression
Assertion clwlkl1loop ⊢Fun⁡iEdg⁡G∧FClWalks⁡GP∧F=1→P⁡0=P⁡1∧P⁡0∈Edg⁡G

Proof

Step Hyp Ref Expression
1 isclwlk ⊢FClWalks⁡GP↔FWalks⁡GP∧P⁡0=P⁡F
2 fveq2 ⊢F=1→P⁡F=P⁡1
3 2 eqeq2d ⊢F=1→P⁡0=P⁡F↔P⁡0=P⁡1
4 3 anbi2d ⊢F=1→FWalks⁡GP∧P⁡0=P⁡F↔FWalks⁡GP∧P⁡0=P⁡1
5 simp2r ⊢F=1∧FWalks⁡GP∧P⁡0=P⁡1∧Fun⁡iEdg⁡G→P⁡0=P⁡1
6 simp3 ⊢F=1∧FWalks⁡GP∧P⁡0=P⁡1∧Fun⁡iEdg⁡G→Fun⁡iEdg⁡G
7 simp2l ⊢F=1∧FWalks⁡GP∧P⁡0=P⁡1∧Fun⁡iEdg⁡G→FWalks⁡GP
8 simpr ⊢FWalks⁡GP∧P⁡0=P⁡1→P⁡0=P⁡1
9 8 anim2i ⊢F=1∧FWalks⁡GP∧P⁡0=P⁡1→F=1∧P⁡0=P⁡1
10 9 3adant3 ⊢F=1∧FWalks⁡GP∧P⁡0=P⁡1∧Fun⁡iEdg⁡G→F=1∧P⁡0=P⁡1
11 wlkl1loop ⊢Fun⁡iEdg⁡G∧FWalks⁡GP∧F=1∧P⁡0=P⁡1→P⁡0∈Edg⁡G
12 6 7 10 11 syl21anc ⊢F=1∧FWalks⁡GP∧P⁡0=P⁡1∧Fun⁡iEdg⁡G→P⁡0∈Edg⁡G
13 5 12 jca ⊢F=1∧FWalks⁡GP∧P⁡0=P⁡1∧Fun⁡iEdg⁡G→P⁡0=P⁡1∧P⁡0∈Edg⁡G
14 13 3exp ⊢F=1→FWalks⁡GP∧P⁡0=P⁡1→Fun⁡iEdg⁡G→P⁡0=P⁡1∧P⁡0∈Edg⁡G
15 4 14 sylbid ⊢F=1→FWalks⁡GP∧P⁡0=P⁡F→Fun⁡iEdg⁡G→P⁡0=P⁡1∧P⁡0∈Edg⁡G
16 15 com13 ⊢Fun⁡iEdg⁡G→FWalks⁡GP∧P⁡0=P⁡F→F=1→P⁡0=P⁡1∧P⁡0∈Edg⁡G
17 1 16 biimtrid ⊢Fun⁡iEdg⁡G→FClWalks⁡GP→F=1→P⁡0=P⁡1∧P⁡0∈Edg⁡G
18 17 3imp ⊢Fun⁡iEdg⁡G∧FClWalks⁡GP∧F=1→P⁡0=P⁡1∧P⁡0∈Edg⁡G