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

Theorem upgr3v3e3cycl 27360
Description: If there is a cycle of length 3 in a pseudograph, there are three distinct vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.)
Hypotheses
Ref Expression
upgr3v3e3cycl.e 𝐸 = (Edg‘𝐺)
upgr3v3e3cycl.v 𝑉 = (Vtx‘𝐺)
Assertion
Ref Expression
upgr3v3e3cycl ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 3) → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))
Distinct variable groups:   𝐸,𝑎,𝑏,𝑐   𝑃,𝑎,𝑏,𝑐   𝑉,𝑎,𝑏,𝑐
Allowed substitution hints:   𝐹(𝑎,𝑏,𝑐)   𝐺(𝑎,𝑏,𝑐)

Proof of Theorem upgr3v3e3cycl
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 cyclprop 26924 . . 3 (𝐹(Cycles‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))))
2 pthiswlk 26858 . . . . 5 (𝐹(Paths‘𝐺)𝑃𝐹(Walks‘𝐺)𝑃)
3 upgr3v3e3cycl.e . . . . . . . . . 10 𝐸 = (Edg‘𝐺)
43upgrwlkvtxedg 26776 . . . . . . . . 9 ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)
5 fveq2 6332 . . . . . . . . . . . . . . 15 ((♯‘𝐹) = 3 → (𝑃‘(♯‘𝐹)) = (𝑃‘3))
65eqeq2d 2781 . . . . . . . . . . . . . 14 ((♯‘𝐹) = 3 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) ↔ (𝑃‘0) = (𝑃‘3)))
76anbi2d 614 . . . . . . . . . . . . 13 ((♯‘𝐹) = 3 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ↔ (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3))))
8 oveq2 6801 . . . . . . . . . . . . . . . 16 ((♯‘𝐹) = 3 → (0..^(♯‘𝐹)) = (0..^3))
9 fzo0to3tp 12762 . . . . . . . . . . . . . . . 16 (0..^3) = {0, 1, 2}
108, 9syl6eq 2821 . . . . . . . . . . . . . . 15 ((♯‘𝐹) = 3 → (0..^(♯‘𝐹)) = {0, 1, 2})
1110raleqdv 3293 . . . . . . . . . . . . . 14 ((♯‘𝐹) = 3 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ {0, 1, 2} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
12 c0ex 10236 . . . . . . . . . . . . . . 15 0 ∈ V
13 1ex 10237 . . . . . . . . . . . . . . 15 1 ∈ V
14 2ex 11294 . . . . . . . . . . . . . . 15 2 ∈ V
15 fveq2 6332 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (𝑃𝑘) = (𝑃‘0))
16 oveq1 6800 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 0 → (𝑘 + 1) = (0 + 1))
17 0p1e1 11334 . . . . . . . . . . . . . . . . . . 19 (0 + 1) = 1
1816, 17syl6eq 2821 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → (𝑘 + 1) = 1)
1918fveq2d 6336 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1))
2015, 19preq12d 4412 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)})
2120eleq1d 2835 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
22 fveq2 6332 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → (𝑃𝑘) = (𝑃‘1))
23 oveq1 6800 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
24 1p1e2 11336 . . . . . . . . . . . . . . . . . . 19 (1 + 1) = 2
2523, 24syl6eq 2821 . . . . . . . . . . . . . . . . . 18 (𝑘 = 1 → (𝑘 + 1) = 2)
2625fveq2d 6336 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2))
2722, 26preq12d 4412 . . . . . . . . . . . . . . . 16 (𝑘 = 1 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)})
2827eleq1d 2835 . . . . . . . . . . . . . . 15 (𝑘 = 1 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
29 fveq2 6332 . . . . . . . . . . . . . . . . 17 (𝑘 = 2 → (𝑃𝑘) = (𝑃‘2))
30 oveq1 6800 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 2 → (𝑘 + 1) = (2 + 1))
31 2p1e3 11353 . . . . . . . . . . . . . . . . . . 19 (2 + 1) = 3
3230, 31syl6eq 2821 . . . . . . . . . . . . . . . . . 18 (𝑘 = 2 → (𝑘 + 1) = 3)
3332fveq2d 6336 . . . . . . . . . . . . . . . . 17 (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3))
3429, 33preq12d 4412 . . . . . . . . . . . . . . . 16 (𝑘 = 2 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)})
3534eleq1d 2835 . . . . . . . . . . . . . . 15 (𝑘 = 2 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
3612, 13, 14, 21, 28, 35raltp 4377 . . . . . . . . . . . . . 14 (∀𝑘 ∈ {0, 1, 2} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
3711, 36syl6bb 276 . . . . . . . . . . . . 13 ((♯‘𝐹) = 3 → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)))
387, 37anbi12d 616 . . . . . . . . . . . 12 ((♯‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))))
39 upgr3v3e3cycl.v . . . . . . . . . . . . . . . . . . 19 𝑉 = (Vtx‘𝐺)
4039wlkp 26747 . . . . . . . . . . . . . . . . . 18 (𝐹(Walks‘𝐺)𝑃𝑃:(0...(♯‘𝐹))⟶𝑉)
41 oveq2 6801 . . . . . . . . . . . . . . . . . . . . 21 ((♯‘𝐹) = 3 → (0...(♯‘𝐹)) = (0...3))
4241feq2d 6171 . . . . . . . . . . . . . . . . . . . 20 ((♯‘𝐹) = 3 → (𝑃:(0...(♯‘𝐹))⟶𝑉𝑃:(0...3)⟶𝑉))
43 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃:(0...3)⟶𝑉𝑃:(0...3)⟶𝑉)
44 3nn0 11512 . . . . . . . . . . . . . . . . . . . . . . 23 3 ∈ ℕ0
45 0elfz 12644 . . . . . . . . . . . . . . . . . . . . . . 23 (3 ∈ ℕ0 → 0 ∈ (0...3))
4644, 45mp1i 13 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃:(0...3)⟶𝑉 → 0 ∈ (0...3))
4743, 46ffvelrnd 6503 . . . . . . . . . . . . . . . . . . . . 21 (𝑃:(0...3)⟶𝑉 → (𝑃‘0) ∈ 𝑉)
48 1nn0 11510 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℕ0
49 1lt3 11398 . . . . . . . . . . . . . . . . . . . . . 22 1 < 3
50 fvffz0 12665 . . . . . . . . . . . . . . . . . . . . . . 23 (((3 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 3) ∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
5150ex 397 . . . . . . . . . . . . . . . . . . . . . 22 ((3 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 3) → (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉))
5244, 48, 49, 51mp3an 1572 . . . . . . . . . . . . . . . . . . . . 21 (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉)
53 2nn0 11511 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℕ0
54 2lt3 11397 . . . . . . . . . . . . . . . . . . . . . 22 2 < 3
55 fvffz0 12665 . . . . . . . . . . . . . . . . . . . . . . 23 (((3 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 3) ∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
5655ex 397 . . . . . . . . . . . . . . . . . . . . . 22 ((3 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 3) → (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉))
5744, 53, 54, 56mp3an 1572 . . . . . . . . . . . . . . . . . . . . 21 (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉)
5847, 52, 573jca 1122 . . . . . . . . . . . . . . . . . . . 20 (𝑃:(0...3)⟶𝑉 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))
5942, 58syl6bi 243 . . . . . . . . . . . . . . . . . . 19 ((♯‘𝐹) = 3 → (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
6059com12 32 . . . . . . . . . . . . . . . . . 18 (𝑃:(0...(♯‘𝐹))⟶𝑉 → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
612, 40, 603syl 18 . . . . . . . . . . . . . . . . 17 (𝐹(Paths‘𝐺)𝑃 → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
6261adantr 466 . . . . . . . . . . . . . . . 16 ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
6362adantr 466 . . . . . . . . . . . . . . 15 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
6463impcom 394 . . . . . . . . . . . . . 14 (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))
65 preq2 4405 . . . . . . . . . . . . . . . . . . . 20 ((𝑃‘3) = (𝑃‘0) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
6665eqcoms 2779 . . . . . . . . . . . . . . . . . . 19 ((𝑃‘0) = (𝑃‘3) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
6766adantl 467 . . . . . . . . . . . . . . . . . 18 ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
6867eleq1d 2835 . . . . . . . . . . . . . . . . 17 ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
69683anbi3d 1553 . . . . . . . . . . . . . . . 16 ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)))
7069biimpa 462 . . . . . . . . . . . . . . 15 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
7170adantl 467 . . . . . . . . . . . . . 14 (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
72 simpll 750 . . . . . . . . . . . . . . . . . . 19 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 𝐹(Paths‘𝐺)𝑃)
73 breq2 4790 . . . . . . . . . . . . . . . . . . . . 21 ((♯‘𝐹) = 3 → (1 < (♯‘𝐹) ↔ 1 < 3))
7449, 73mpbiri 248 . . . . . . . . . . . . . . . . . . . 20 ((♯‘𝐹) = 3 → 1 < (♯‘𝐹))
7574adantl 467 . . . . . . . . . . . . . . . . . . 19 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 1 < (♯‘𝐹))
76 3nn 11388 . . . . . . . . . . . . . . . . . . . . . 22 3 ∈ ℕ
77 lbfzo0 12716 . . . . . . . . . . . . . . . . . . . . . 22 (0 ∈ (0..^3) ↔ 3 ∈ ℕ)
7876, 77mpbir 221 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ (0..^3)
7978, 8syl5eleqr 2857 . . . . . . . . . . . . . . . . . . . 20 ((♯‘𝐹) = 3 → 0 ∈ (0..^(♯‘𝐹)))
8079adantl 467 . . . . . . . . . . . . . . . . . . 19 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 0 ∈ (0..^(♯‘𝐹)))
81 pthdadjvtx 26861 . . . . . . . . . . . . . . . . . . . 20 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈ (0..^(♯‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
82 1e0p1 11754 . . . . . . . . . . . . . . . . . . . . . 22 1 = (0 + 1)
8382fveq2i 6335 . . . . . . . . . . . . . . . . . . . . 21 (𝑃‘1) = (𝑃‘(0 + 1))
8483neeq2i 3008 . . . . . . . . . . . . . . . . . . . 20 ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 + 1)))
8581, 84sylibr 224 . . . . . . . . . . . . . . . . . . 19 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 0 ∈ (0..^(♯‘𝐹))) → (𝑃‘0) ≠ (𝑃‘1))
8672, 75, 80, 85syl3anc 1476 . . . . . . . . . . . . . . . . . 18 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘0) ≠ (𝑃‘1))
87 elfzo0 12717 . . . . . . . . . . . . . . . . . . . . . 22 (1 ∈ (0..^3) ↔ (1 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 1 < 3))
8848, 76, 49, 87mpbir3an 1426 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ (0..^3)
8988, 8syl5eleqr 2857 . . . . . . . . . . . . . . . . . . . 20 ((♯‘𝐹) = 3 → 1 ∈ (0..^(♯‘𝐹)))
9089adantl 467 . . . . . . . . . . . . . . . . . . 19 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 1 ∈ (0..^(♯‘𝐹)))
91 pthdadjvtx 26861 . . . . . . . . . . . . . . . . . . . 20 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈ (0..^(♯‘𝐹))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
92 df-2 11281 . . . . . . . . . . . . . . . . . . . . . 22 2 = (1 + 1)
9392fveq2i 6335 . . . . . . . . . . . . . . . . . . . . 21 (𝑃‘2) = (𝑃‘(1 + 1))
9493neeq2i 3008 . . . . . . . . . . . . . . . . . . . 20 ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 + 1)))
9591, 94sylibr 224 . . . . . . . . . . . . . . . . . . 19 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 1 ∈ (0..^(♯‘𝐹))) → (𝑃‘1) ≠ (𝑃‘2))
9672, 75, 90, 95syl3anc 1476 . . . . . . . . . . . . . . . . . 18 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘1) ≠ (𝑃‘2))
97 elfzo0 12717 . . . . . . . . . . . . . . . . . . . . . . 23 (2 ∈ (0..^3) ↔ (2 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 2 < 3))
9853, 76, 54, 97mpbir3an 1426 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ (0..^3)
9998, 8syl5eleqr 2857 . . . . . . . . . . . . . . . . . . . . 21 ((♯‘𝐹) = 3 → 2 ∈ (0..^(♯‘𝐹)))
10099adantl 467 . . . . . . . . . . . . . . . . . . . 20 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → 2 ∈ (0..^(♯‘𝐹)))
101 pthdadjvtx 26861 . . . . . . . . . . . . . . . . . . . 20 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (♯‘𝐹) ∧ 2 ∈ (0..^(♯‘𝐹))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
10272, 75, 100, 101syl3anc 1476 . . . . . . . . . . . . . . . . . . 19 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
103 neeq2 3006 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘3)))
104 df-3 11282 . . . . . . . . . . . . . . . . . . . . . . . 24 3 = (2 + 1)
105104fveq2i 6335 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃‘3) = (𝑃‘(2 + 1))
106105neeq2i 3008 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))
107103, 106syl6bb 276 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
108107adantl 467 . . . . . . . . . . . . . . . . . . . 20 ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
109108adantr 466 . . . . . . . . . . . . . . . . . . 19 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
110102, 109mpbird 247 . . . . . . . . . . . . . . . . . 18 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘0))
11186, 96, 1103jca 1122 . . . . . . . . . . . . . . . . 17 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (♯‘𝐹) = 3) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))
112111ex 397 . . . . . . . . . . . . . . . 16 ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
113112adantr 466 . . . . . . . . . . . . . . 15 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((♯‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
114113impcom 394 . . . . . . . . . . . . . 14 (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))
115 preq1 4404 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏})
116115eleq1d 2835 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸))
117 preq2 4405 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → {𝑐, 𝑎} = {𝑐, (𝑃‘0)})
118117eleq1d 2835 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑐, (𝑃‘0)} ∈ 𝐸))
119116, 1183anbi13d 1549 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸)))
120 neeq1 3005 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → (𝑎𝑏 ↔ (𝑃‘0) ≠ 𝑏))
121 neeq2 3006 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → (𝑐𝑎𝑐 ≠ (𝑃‘0)))
122120, 1213anbi13d 1549 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑃‘0) → ((𝑎𝑏𝑏𝑐𝑐𝑎) ↔ ((𝑃‘0) ≠ 𝑏𝑏𝑐𝑐 ≠ (𝑃‘0))))
123119, 122anbi12d 616 . . . . . . . . . . . . . . 15 (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏𝑏𝑐𝑐 ≠ (𝑃‘0)))))
124 preq2 4405 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)})
125124eleq1d 2835 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
126 preq1 4404 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐})
127126eleq1d 2835 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸))
128125, 1273anbi12d 1548 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸)))
129 neeq2 3006 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1)))
130 neeq1 3005 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → (𝑏𝑐 ↔ (𝑃‘1) ≠ 𝑐))
131129, 1303anbi12d 1548 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏𝑏𝑐𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐𝑐 ≠ (𝑃‘0))))
132128, 131anbi12d 616 . . . . . . . . . . . . . . 15 (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏𝑏𝑐𝑐 ≠ (𝑃‘0))) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐𝑐 ≠ (𝑃‘0)))))
133 preq2 4405 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)})
134133eleq1d 2835 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
135 preq1 4404 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝑃‘2) → {𝑐, (𝑃‘0)} = {(𝑃‘2), (𝑃‘0)})
136135eleq1d 2835 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑃‘2) → ({𝑐, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
137134, 1363anbi23d 1550 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)))
138 neeq2 3006 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2)))
139 neeq1 3005 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑃‘2) → (𝑐 ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘0)))
140138, 1393anbi23d 1550 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
141137, 140anbi12d 616 . . . . . . . . . . . . . . 15 (𝑐 = (𝑃‘2) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐𝑐 ≠ (𝑃‘0))) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))))
142123, 132, 141rspc3ev 3476 . . . . . . . . . . . . . 14 ((((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))
14364, 71, 114, 142syl12anc 1474 . . . . . . . . . . . . 13 (((♯‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))
144143ex 397 . . . . . . . . . . . 12 ((♯‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎))))
14538, 144sylbid 230 . . . . . . . . . . 11 ((♯‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) ∧ ∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎))))
146145expd 400 . . . . . . . . . 10 ((♯‘𝐹) = 3 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))
147146com13 88 . . . . . . . . 9 (∀𝑘 ∈ (0..^(♯‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))
1484, 147syl 17 . . . . . . . 8 ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))
149148expcom 398 . . . . . . 7 (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → ((♯‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎))))))
150149com23 86 . . . . . 6 (𝐹(Walks‘𝐺)𝑃 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎))))))
151150expd 400 . . . . 5 (𝐹(Walks‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))))
1522, 151mpcom 38 . . . 4 (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(♯‘𝐹)) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎))))))
153152imp 393 . . 3 ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(♯‘𝐹))) → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))
1541, 153syl 17 . 2 (𝐹(Cycles‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((♯‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))
1551543imp21 1105 1 ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (♯‘𝐹) = 3) → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1071   = wceq 1631  wcel 2145  wne 2943  wral 3061  wrex 3062  {cpr 4318  {ctp 4320   class class class wbr 4786  wf 6027  cfv 6031  (class class class)co 6793  0cc0 10138  1c1 10139   + caddc 10141   < clt 10276  cn 11222  2c2 11272  3c3 11273  0cn0 11494  ...cfz 12533  ..^cfzo 12673  chash 13321  Vtxcvtx 26095  Edgcedg 26160  UPGraphcupgr 26196  Walkscwlks 26727  Pathscpths 26843  Cyclesccycls 26916
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-ifp 1050  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-nn 11223  df-2 11281  df-3 11282  df-n0 11495  df-xnn0 11566  df-z 11580  df-uz 11889  df-fz 12534  df-fzo 12674  df-hash 13322  df-word 13495  df-edg 26161  df-uhgr 26174  df-upgr 26198  df-wlks 26730  df-trls 26824  df-pths 26847  df-cycls 26918
This theorem is referenced by:  umgr3v3e3cycl  27364
  Copyright terms: Public domain W3C validator