MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  usgrcyclnl2 Structured version   Visualization version   GIF version

Theorem usgrcyclnl2 25935
Description: In an undirected simple graph (with no loops!) there are no cycles with length 2 (consisting of two edges ). (Contributed by Alexander van der Vekens, 9-Nov-2017.)
Assertion
Ref Expression
usgrcyclnl2 ((𝑉 USGrph 𝐸𝐹(𝑉 Cycles 𝐸)𝑃) → (#‘𝐹) ≠ 2)

Proof of Theorem usgrcyclnl2
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 cyclispth 25923 . . . 4 (𝐹(𝑉 Cycles 𝐸)𝑃𝐹(𝑉 Paths 𝐸)𝑃)
2 pthistrl 25868 . . . . 5 (𝐹(𝑉 Paths 𝐸)𝑃𝐹(𝑉 Trails 𝐸)𝑃)
3 cycliswlk 25926 . . . . . 6 (𝐹(𝑉 Cycles 𝐸)𝑃𝐹(𝑉 Walks 𝐸)𝑃)
4 wlkbprop 25817 . . . . . 6 (𝐹(𝑉 Walks 𝐸)𝑃 → ((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)))
5 istrl2 25834 . . . . . . . 8 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Trails 𝐸)𝑃 ↔ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})))
6 pm3.2 461 . . . . . . . 8 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}))))
75, 6sylbid 228 . . . . . . 7 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Trails 𝐸)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}))))
873adant1 1071 . . . . . 6 (((#‘𝐹) ∈ ℕ0 ∧ (𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Trails 𝐸)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}))))
93, 4, 83syl 18 . . . . 5 (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝐹(𝑉 Trails 𝐸)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}))))
102, 9syl5com 31 . . . 4 (𝐹(𝑉 Paths 𝐸)𝑃 → (𝐹(𝑉 Cycles 𝐸)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}))))
111, 10mpcom 37 . . 3 (𝐹(𝑉 Cycles 𝐸)𝑃 → (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})))
12 iscycl 25919 . . . . 5 (((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) → (𝐹(𝑉 Cycles 𝐸)𝑃 ↔ (𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))))
1312adantr 479 . . . 4 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})) → (𝐹(𝑉 Cycles 𝐸)𝑃 ↔ (𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹)))))
14 oveq2 6535 . . . . . . . . . . . . . 14 ((#‘𝐹) = 2 → (0..^(#‘𝐹)) = (0..^2))
15 f1eq2 5995 . . . . . . . . . . . . . 14 ((0..^(#‘𝐹)) = (0..^2) → (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸𝐹:(0..^2)–1-1→dom 𝐸))
1614, 15syl 17 . . . . . . . . . . . . 13 ((#‘𝐹) = 2 → (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸𝐹:(0..^2)–1-1→dom 𝐸))
1714raleqdv 3120 . . . . . . . . . . . . 13 ((#‘𝐹) = 2 → (∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ↔ ∀𝑘 ∈ (0..^2)(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}))
1816, 17anbi12d 742 . . . . . . . . . . . 12 ((#‘𝐹) = 2 → ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) ↔ (𝐹:(0..^2)–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^2)(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})))
19 fveq2 6088 . . . . . . . . . . . . 13 ((#‘𝐹) = 2 → (𝑃‘(#‘𝐹)) = (𝑃‘2))
2019eqeq2d 2619 . . . . . . . . . . . 12 ((#‘𝐹) = 2 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) ↔ (𝑃‘0) = (𝑃‘2)))
2118, 20anbi12d 742 . . . . . . . . . . 11 ((#‘𝐹) = 2 → (((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ↔ ((𝐹:(0..^2)–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^2)(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) ∧ (𝑃‘0) = (𝑃‘2))))
2221anbi1d 736 . . . . . . . . . 10 ((#‘𝐹) = 2 → ((((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ 𝑉 USGrph 𝐸) ↔ (((𝐹:(0..^2)–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^2)(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) ∧ (𝑃‘0) = (𝑃‘2)) ∧ 𝑉 USGrph 𝐸)))
23 fzo0to2pr 12375 . . . . . . . . . . . . . 14 (0..^2) = {0, 1}
2423raleqi 3118 . . . . . . . . . . . . 13 (∀𝑘 ∈ (0..^2)(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ↔ ∀𝑘 ∈ {0, 1} (𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})
25 2wlklem 25860 . . . . . . . . . . . . . 14 (∀𝑘 ∈ {0, 1} (𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}))
26 prcom 4210 . . . . . . . . . . . . . . . . . . 19 {(𝑃‘1), (𝑃‘2)} = {(𝑃‘2), (𝑃‘1)}
2726eqeq2i 2621 . . . . . . . . . . . . . . . . . 18 ((𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ↔ (𝐸‘(𝐹‘1)) = {(𝑃‘2), (𝑃‘1)})
28 preq1 4211 . . . . . . . . . . . . . . . . . . . 20 ((𝑃‘2) = (𝑃‘0) → {(𝑃‘2), (𝑃‘1)} = {(𝑃‘0), (𝑃‘1)})
2928eqcoms 2617 . . . . . . . . . . . . . . . . . . 19 ((𝑃‘0) = (𝑃‘2) → {(𝑃‘2), (𝑃‘1)} = {(𝑃‘0), (𝑃‘1)})
3029eqeq2d 2619 . . . . . . . . . . . . . . . . . 18 ((𝑃‘0) = (𝑃‘2) → ((𝐸‘(𝐹‘1)) = {(𝑃‘2), (𝑃‘1)} ↔ (𝐸‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)}))
3127, 30syl5bb 270 . . . . . . . . . . . . . . . . 17 ((𝑃‘0) = (𝑃‘2) → ((𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)} ↔ (𝐸‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)}))
3231anbi2d 735 . . . . . . . . . . . . . . . 16 ((𝑃‘0) = (𝑃‘2) → (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) ↔ ((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)})))
33 eqtr3 2630 . . . . . . . . . . . . . . . . 17 (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)}) → (𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1)))
34 usgraf1 25655 . . . . . . . . . . . . . . . . . . 19 (𝑉 USGrph 𝐸𝐸:dom 𝐸1-1→ran 𝐸)
35 f1f 5999 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:(0..^2)–1-1→dom 𝐸𝐹:(0..^2)⟶dom 𝐸)
36 2nn 11032 . . . . . . . . . . . . . . . . . . . . . . . . . 26 2 ∈ ℕ
37 lbfzo0 12330 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 ∈ (0..^2) ↔ 2 ∈ ℕ)
3836, 37mpbir 219 . . . . . . . . . . . . . . . . . . . . . . . . 25 0 ∈ (0..^2)
39 ffvelrn 6250 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹:(0..^2)⟶dom 𝐸 ∧ 0 ∈ (0..^2)) → (𝐹‘0) ∈ dom 𝐸)
4038, 39mpan2 702 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:(0..^2)⟶dom 𝐸 → (𝐹‘0) ∈ dom 𝐸)
41 1nn0 11155 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 ∈ ℕ0
42 1lt2 11041 . . . . . . . . . . . . . . . . . . . . . . . . . 26 1 < 2
43 elfzo0 12331 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (1 ∈ (0..^2) ↔ (1 ∈ ℕ0 ∧ 2 ∈ ℕ ∧ 1 < 2))
4441, 36, 42, 43mpbir3an 1236 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 ∈ (0..^2)
45 ffvelrn 6250 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹:(0..^2)⟶dom 𝐸 ∧ 1 ∈ (0..^2)) → (𝐹‘1) ∈ dom 𝐸)
4644, 45mpan2 702 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝐹:(0..^2)⟶dom 𝐸 → (𝐹‘1) ∈ dom 𝐸)
4740, 46jca 552 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:(0..^2)⟶dom 𝐸 → ((𝐹‘0) ∈ dom 𝐸 ∧ (𝐹‘1) ∈ dom 𝐸))
4835, 47syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:(0..^2)–1-1→dom 𝐸 → ((𝐹‘0) ∈ dom 𝐸 ∧ (𝐹‘1) ∈ dom 𝐸))
49 f1fveq 6398 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐸:dom 𝐸1-1→ran 𝐸 ∧ ((𝐹‘0) ∈ dom 𝐸 ∧ (𝐹‘1) ∈ dom 𝐸)) → ((𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1)) ↔ (𝐹‘0) = (𝐹‘1)))
5048, 49sylan2 489 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸:dom 𝐸1-1→ran 𝐸𝐹:(0..^2)–1-1→dom 𝐸) → ((𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1)) ↔ (𝐹‘0) = (𝐹‘1)))
51 f1fveq 6398 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹:(0..^2)–1-1→dom 𝐸 ∧ (0 ∈ (0..^2) ∧ 1 ∈ (0..^2))) → ((𝐹‘0) = (𝐹‘1) ↔ 0 = 1))
5238, 44, 51mpanr12 716 . . . . . . . . . . . . . . . . . . . . . . 23 (𝐹:(0..^2)–1-1→dom 𝐸 → ((𝐹‘0) = (𝐹‘1) ↔ 0 = 1))
53 ax-1ne0 9861 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ≠ 0
54 necom 2834 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1 ≠ 0 ↔ 0 ≠ 1)
55 df-ne 2781 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (0 ≠ 1 ↔ ¬ 0 = 1)
56 pm2.21 118 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (¬ 0 = 1 → (0 = 1 → (#‘𝐹) ≠ 2))
5755, 56sylbi 205 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 ≠ 1 → (0 = 1 → (#‘𝐹) ≠ 2))
5854, 57sylbi 205 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 ≠ 0 → (0 = 1 → (#‘𝐹) ≠ 2))
5953, 58ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23 (0 = 1 → (#‘𝐹) ≠ 2)
6052, 59syl6bi 241 . . . . . . . . . . . . . . . . . . . . . 22 (𝐹:(0..^2)–1-1→dom 𝐸 → ((𝐹‘0) = (𝐹‘1) → (#‘𝐹) ≠ 2))
6160adantl 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝐸:dom 𝐸1-1→ran 𝐸𝐹:(0..^2)–1-1→dom 𝐸) → ((𝐹‘0) = (𝐹‘1) → (#‘𝐹) ≠ 2))
6250, 61sylbid 228 . . . . . . . . . . . . . . . . . . . 20 ((𝐸:dom 𝐸1-1→ran 𝐸𝐹:(0..^2)–1-1→dom 𝐸) → ((𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1)) → (#‘𝐹) ≠ 2))
6362ex 448 . . . . . . . . . . . . . . . . . . 19 (𝐸:dom 𝐸1-1→ran 𝐸 → (𝐹:(0..^2)–1-1→dom 𝐸 → ((𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1)) → (#‘𝐹) ≠ 2)))
6434, 63syl 17 . . . . . . . . . . . . . . . . . 18 (𝑉 USGrph 𝐸 → (𝐹:(0..^2)–1-1→dom 𝐸 → ((𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1)) → (#‘𝐹) ≠ 2)))
6564com13 85 . . . . . . . . . . . . . . . . 17 ((𝐸‘(𝐹‘0)) = (𝐸‘(𝐹‘1)) → (𝐹:(0..^2)–1-1→dom 𝐸 → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2)))
6633, 65syl 17 . . . . . . . . . . . . . . . 16 (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘0), (𝑃‘1)}) → (𝐹:(0..^2)–1-1→dom 𝐸 → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2)))
6732, 66syl6bi 241 . . . . . . . . . . . . . . 15 ((𝑃‘0) = (𝑃‘2) → (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐹:(0..^2)–1-1→dom 𝐸 → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2))))
6867com3l 86 . . . . . . . . . . . . . 14 (((𝐸‘(𝐹‘0)) = {(𝑃‘0), (𝑃‘1)} ∧ (𝐸‘(𝐹‘1)) = {(𝑃‘1), (𝑃‘2)}) → (𝐹:(0..^2)–1-1→dom 𝐸 → ((𝑃‘0) = (𝑃‘2) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2))))
6925, 68sylbi 205 . . . . . . . . . . . . 13 (∀𝑘 ∈ {0, 1} (𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → (𝐹:(0..^2)–1-1→dom 𝐸 → ((𝑃‘0) = (𝑃‘2) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2))))
7024, 69sylbi 205 . . . . . . . . . . . 12 (∀𝑘 ∈ (0..^2)(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))} → (𝐹:(0..^2)–1-1→dom 𝐸 → ((𝑃‘0) = (𝑃‘2) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2))))
7170impcom 444 . . . . . . . . . . 11 ((𝐹:(0..^2)–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^2)(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) → ((𝑃‘0) = (𝑃‘2) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2)))
7271imp31 446 . . . . . . . . . 10 ((((𝐹:(0..^2)–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^2)(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) ∧ (𝑃‘0) = (𝑃‘2)) ∧ 𝑉 USGrph 𝐸) → (#‘𝐹) ≠ 2)
7322, 72syl6bi 241 . . . . . . . . 9 ((#‘𝐹) = 2 → ((((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ 𝑉 USGrph 𝐸) → (#‘𝐹) ≠ 2))
74 ax-1 6 . . . . . . . . 9 ((#‘𝐹) ≠ 2 → ((((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ 𝑉 USGrph 𝐸) → (#‘𝐹) ≠ 2))
7573, 74pm2.61ine 2864 . . . . . . . 8 ((((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ 𝑉 USGrph 𝐸) → (#‘𝐹) ≠ 2)
7675exp31 627 . . . . . . 7 ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2)))
77763adant2 1072 . . . . . 6 ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2)))
7877adantld 481 . . . . 5 ((𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))}) → ((𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2)))
7978adantl 480 . . . 4 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})) → ((𝐹(𝑉 Paths 𝐸)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2)))
8013, 79sylbid 228 . . 3 ((((𝑉 ∈ V ∧ 𝐸 ∈ V) ∧ (𝐹 ∈ V ∧ 𝑃 ∈ V)) ∧ (𝐹:(0..^(#‘𝐹))–1-1→dom 𝐸𝑃:(0...(#‘𝐹))⟶𝑉 ∧ ∀𝑘 ∈ (0..^(#‘𝐹))(𝐸‘(𝐹𝑘)) = {(𝑃𝑘), (𝑃‘(𝑘 + 1))})) → (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2)))
8111, 80mpcom 37 . 2 (𝐹(𝑉 Cycles 𝐸)𝑃 → (𝑉 USGrph 𝐸 → (#‘𝐹) ≠ 2))
8281impcom 444 1 ((𝑉 USGrph 𝐸𝐹(𝑉 Cycles 𝐸)𝑃) → (#‘𝐹) ≠ 2)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  wral 2895  Vcvv 3172  {cpr 4126   class class class wbr 4577  dom cdm 5028  ran crn 5029  wf 5786  1-1wf1 5787  cfv 5790  (class class class)co 6527  0cc0 9792  1c1 9793   + caddc 9795   < clt 9930  cn 10867  2c2 10917  0cn0 11139  ...cfz 12152  ..^cfzo 12289  #chash 12934   USGrph cusg 25625   Walks cwalk 25792   Trails ctrail 25793   Paths cpath 25794   Cycles ccycl 25801
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824  ax-cnex 9848  ax-resscn 9849  ax-1cn 9850  ax-icn 9851  ax-addcl 9852  ax-addrcl 9853  ax-mulcl 9854  ax-mulrcl 9855  ax-mulcom 9856  ax-addass 9857  ax-mulass 9858  ax-distr 9859  ax-i2m1 9860  ax-1ne0 9861  ax-1rid 9862  ax-rnegex 9863  ax-rrecex 9864  ax-cnre 9865  ax-pre-lttri 9866  ax-pre-lttrn 9867  ax-pre-ltadd 9868  ax-pre-mulgt0 9869
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6935  df-1st 7036  df-2nd 7037  df-wrecs 7271  df-recs 7332  df-rdg 7370  df-1o 7424  df-oadd 7428  df-er 7606  df-map 7723  df-pm 7724  df-en 7819  df-dom 7820  df-sdom 7821  df-fin 7822  df-card 8625  df-pnf 9932  df-mnf 9933  df-xr 9934  df-ltxr 9935  df-le 9936  df-sub 10119  df-neg 10120  df-nn 10868  df-2 10926  df-n0 11140  df-z 11211  df-uz 11520  df-fz 12153  df-fzo 12290  df-hash 12935  df-word 13100  df-usgra 25628  df-wlk 25802  df-trail 25803  df-pth 25804  df-cycl 25807
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator