Mathbox for Alexander van der Vekens < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  upgr3v3e3cycl Structured version   Visualization version   GIF version

Theorem upgr3v3e3cycl 41347
 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 40999 . . 3 (𝐹(CycleS‘𝐺)𝑃 → (𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))
2 pthis1wlk 40933 . . . . 5 (𝐹(PathS‘𝐺)𝑃𝐹(1Walks‘𝐺)𝑃)
3 upgr3v3e3cycl.e . . . . . . . . . 10 𝐸 = (Edg‘𝐺)
43upgr1wlkvtxedg 40853 . . . . . . . . 9 ((𝐺 ∈ UPGraph ∧ 𝐹(1Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)
5 fveq2 6103 . . . . . . . . . . . . . . 15 ((#‘𝐹) = 3 → (𝑃‘(#‘𝐹)) = (𝑃‘3))
65eqeq2d 2620 . . . . . . . . . . . . . 14 ((#‘𝐹) = 3 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) ↔ (𝑃‘0) = (𝑃‘3)))
76anbi2d 736 . . . . . . . . . . . . 13 ((#‘𝐹) = 3 → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ↔ (𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3))))
8 oveq2 6557 . . . . . . . . . . . . . . . 16 ((#‘𝐹) = 3 → (0..^(#‘𝐹)) = (0..^3))
9 fzo0to3tp 12421 . . . . . . . . . . . . . . . 16 (0..^3) = {0, 1, 2}
108, 9syl6eq 2660 . . . . . . . . . . . . . . 15 ((#‘𝐹) = 3 → (0..^(#‘𝐹)) = {0, 1, 2})
1110raleqdv 3121 . . . . . . . . . . . . . 14 ((#‘𝐹) = 3 → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ {0, 1, 2} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
12 c0ex 9913 . . . . . . . . . . . . . . 15 0 ∈ V
13 1ex 9914 . . . . . . . . . . . . . . 15 1 ∈ V
14 2ex 10969 . . . . . . . . . . . . . . 15 2 ∈ V
15 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (𝑃𝑘) = (𝑃‘0))
16 oveq1 6556 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 0 → (𝑘 + 1) = (0 + 1))
17 0p1e1 11009 . . . . . . . . . . . . . . . . . . 19 (0 + 1) = 1
1816, 17syl6eq 2660 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → (𝑘 + 1) = 1)
1918fveq2d 6107 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1))
2015, 19preq12d 4220 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)})
2120eleq1d 2672 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
22 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → (𝑃𝑘) = (𝑃‘1))
23 oveq1 6556 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
24 1p1e2 11011 . . . . . . . . . . . . . . . . . . 19 (1 + 1) = 2
2523, 24syl6eq 2660 . . . . . . . . . . . . . . . . . 18 (𝑘 = 1 → (𝑘 + 1) = 2)
2625fveq2d 6107 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2))
2722, 26preq12d 4220 . . . . . . . . . . . . . . . 16 (𝑘 = 1 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)})
2827eleq1d 2672 . . . . . . . . . . . . . . 15 (𝑘 = 1 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
29 fveq2 6103 . . . . . . . . . . . . . . . . 17 (𝑘 = 2 → (𝑃𝑘) = (𝑃‘2))
30 oveq1 6556 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 2 → (𝑘 + 1) = (2 + 1))
31 2p1e3 11028 . . . . . . . . . . . . . . . . . . 19 (2 + 1) = 3
3230, 31syl6eq 2660 . . . . . . . . . . . . . . . . . 18 (𝑘 = 2 → (𝑘 + 1) = 3)
3332fveq2d 6107 . . . . . . . . . . . . . . . . 17 (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3))
3429, 33preq12d 4220 . . . . . . . . . . . . . . . 16 (𝑘 = 2 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)})
3534eleq1d 2672 . . . . . . . . . . . . . . 15 (𝑘 = 2 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
3612, 13, 14, 21, 28, 35raltp 4187 . . . . . . . . . . . . . 14 (∀𝑘 ∈ {0, 1, 2} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
3711, 36syl6bb 275 . . . . . . . . . . . . 13 ((#‘𝐹) = 3 → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)))
387, 37anbi12d 743 . . . . . . . . . . . 12 ((#‘𝐹) = 3 → (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))))
39 upgr3v3e3cycl.v . . . . . . . . . . . . . . . . . . 19 𝑉 = (Vtx‘𝐺)
40391wlkp 40821 . . . . . . . . . . . . . . . . . 18 (𝐹(1Walks‘𝐺)𝑃𝑃:(0...(#‘𝐹))⟶𝑉)
41 oveq2 6557 . . . . . . . . . . . . . . . . . . . . 21 ((#‘𝐹) = 3 → (0...(#‘𝐹)) = (0...3))
4241feq2d 5944 . . . . . . . . . . . . . . . . . . . 20 ((#‘𝐹) = 3 → (𝑃:(0...(#‘𝐹))⟶𝑉𝑃:(0...3)⟶𝑉))
43 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃:(0...3)⟶𝑉𝑃:(0...3)⟶𝑉)
44 3nn0 11187 . . . . . . . . . . . . . . . . . . . . . . 23 3 ∈ ℕ0
45 0elfz 12305 . . . . . . . . . . . . . . . . . . . . . . 23 (3 ∈ ℕ0 → 0 ∈ (0...3))
4644, 45mp1i 13 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃:(0...3)⟶𝑉 → 0 ∈ (0...3))
4743, 46ffvelrnd 6268 . . . . . . . . . . . . . . . . . . . . 21 (𝑃:(0...3)⟶𝑉 → (𝑃‘0) ∈ 𝑉)
48 1nn0 11185 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℕ0
49 1lt3 11073 . . . . . . . . . . . . . . . . . . . . . 22 1 < 3
50 fvffz0 12326 . . . . . . . . . . . . . . . . . . . . . . 23 (((3 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 3) ∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
5150ex 449 . . . . . . . . . . . . . . . . . . . . . 22 ((3 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 3) → (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉))
5244, 48, 49, 51mp3an 1416 . . . . . . . . . . . . . . . . . . . . 21 (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉)
53 2nn0 11186 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℕ0
54 2lt3 11072 . . . . . . . . . . . . . . . . . . . . . 22 2 < 3
55 fvffz0 12326 . . . . . . . . . . . . . . . . . . . . . . 23 (((3 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 3) ∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
5655ex 449 . . . . . . . . . . . . . . . . . . . . . 22 ((3 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 3) → (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉))
5744, 53, 54, 56mp3an 1416 . . . . . . . . . . . . . . . . . . . . 21 (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉)
5847, 52, 573jca 1235 . . . . . . . . . . . . . . . . . . . 20 (𝑃:(0...3)⟶𝑉 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))
5942, 58syl6bi 242 . . . . . . . . . . . . . . . . . . 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 480 . . . . . . . . . . . . . . . 16 ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((#‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
6362adantr 480 . . . . . . . . . . . . . . 15 (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((#‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
6463impcom 445 . . . . . . . . . . . . . 14 (((#‘𝐹) = 3 ∧ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))
65 preq2 4213 . . . . . . . . . . . . . . . . . . . 20 ((𝑃‘3) = (𝑃‘0) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
6665eqcoms 2618 . . . . . . . . . . . . . . . . . . 19 ((𝑃‘0) = (𝑃‘3) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
6766adantl 481 . . . . . . . . . . . . . . . . . 18 ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
6867eleq1d 2672 . . . . . . . . . . . . . . . . 17 ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
69683anbi3d 1397 . . . . . . . . . . . . . . . 16 ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)))
7069biimpa 500 . . . . . . . . . . . . . . 15 (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
7170adantl 481 . . . . . . . . . . . . . 14 (((#‘𝐹) = 3 ∧ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
72 simpll 786 . . . . . . . . . . . . . . . . . . 19 (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → 𝐹(PathS‘𝐺)𝑃)
73 breq2 4587 . . . . . . . . . . . . . . . . . . . . 21 ((#‘𝐹) = 3 → (1 < (#‘𝐹) ↔ 1 < 3))
7449, 73mpbiri 247 . . . . . . . . . . . . . . . . . . . 20 ((#‘𝐹) = 3 → 1 < (#‘𝐹))
7574adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → 1 < (#‘𝐹))
76 3nn 11063 . . . . . . . . . . . . . . . . . . . . . 22 3 ∈ ℕ
77 lbfzo0 12375 . . . . . . . . . . . . . . . . . . . . . 22 (0 ∈ (0..^3) ↔ 3 ∈ ℕ)
7876, 77mpbir 220 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ (0..^3)
7978, 8syl5eleqr 2695 . . . . . . . . . . . . . . . . . . . 20 ((#‘𝐹) = 3 → 0 ∈ (0..^(#‘𝐹)))
8079adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → 0 ∈ (0..^(#‘𝐹)))
81 pthdadjvtx 40936 . . . . . . . . . . . . . . . . . . . 20 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 0 ∈ (0..^(#‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
82 1e0p1 11428 . . . . . . . . . . . . . . . . . . . . . 22 1 = (0 + 1)
8382fveq2i 6106 . . . . . . . . . . . . . . . . . . . . 21 (𝑃‘1) = (𝑃‘(0 + 1))
8483neeq2i 2847 . . . . . . . . . . . . . . . . . . . 20 ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 + 1)))
8581, 84sylibr 223 . . . . . . . . . . . . . . . . . . 19 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 0 ∈ (0..^(#‘𝐹))) → (𝑃‘0) ≠ (𝑃‘1))
8672, 75, 80, 85syl3anc 1318 . . . . . . . . . . . . . . . . . 18 (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → (𝑃‘0) ≠ (𝑃‘1))
87 elfzo0 12376 . . . . . . . . . . . . . . . . . . . . . 22 (1 ∈ (0..^3) ↔ (1 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 1 < 3))
8848, 76, 49, 87mpbir3an 1237 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ (0..^3)
8988, 8syl5eleqr 2695 . . . . . . . . . . . . . . . . . . . 20 ((#‘𝐹) = 3 → 1 ∈ (0..^(#‘𝐹)))
9089adantl 481 . . . . . . . . . . . . . . . . . . 19 (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → 1 ∈ (0..^(#‘𝐹)))
91 pthdadjvtx 40936 . . . . . . . . . . . . . . . . . . . 20 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 1 ∈ (0..^(#‘𝐹))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
92 df-2 10956 . . . . . . . . . . . . . . . . . . . . . 22 2 = (1 + 1)
9392fveq2i 6106 . . . . . . . . . . . . . . . . . . . . 21 (𝑃‘2) = (𝑃‘(1 + 1))
9493neeq2i 2847 . . . . . . . . . . . . . . . . . . . 20 ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 + 1)))
9591, 94sylibr 223 . . . . . . . . . . . . . . . . . . 19 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 1 ∈ (0..^(#‘𝐹))) → (𝑃‘1) ≠ (𝑃‘2))
9672, 75, 90, 95syl3anc 1318 . . . . . . . . . . . . . . . . . 18 (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → (𝑃‘1) ≠ (𝑃‘2))
97 elfzo0 12376 . . . . . . . . . . . . . . . . . . . . . . 23 (2 ∈ (0..^3) ↔ (2 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 2 < 3))
9853, 76, 54, 97mpbir3an 1237 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ (0..^3)
9998, 8syl5eleqr 2695 . . . . . . . . . . . . . . . . . . . . 21 ((#‘𝐹) = 3 → 2 ∈ (0..^(#‘𝐹)))
10099adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → 2 ∈ (0..^(#‘𝐹)))
101 pthdadjvtx 40936 . . . . . . . . . . . . . . . . . . . 20 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 2 ∈ (0..^(#‘𝐹))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
10272, 75, 100, 101syl3anc 1318 . . . . . . . . . . . . . . . . . . 19 (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
103 neeq2 2845 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘3)))
104 df-3 10957 . . . . . . . . . . . . . . . . . . . . . . . 24 3 = (2 + 1)
105104fveq2i 6106 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃‘3) = (𝑃‘(2 + 1))
106105neeq2i 2847 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))
107103, 106syl6bb 275 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
108107adantl 481 . . . . . . . . . . . . . . . . . . . 20 ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
109108adantr 480 . . . . . . . . . . . . . . . . . . 19 (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
110102, 109mpbird 246 . . . . . . . . . . . . . . . . . 18 (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘0))
11186, 96, 1103jca 1235 . . . . . . . . . . . . . . . . 17 (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))
112111ex 449 . . . . . . . . . . . . . . . 16 ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((#‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
113112adantr 480 . . . . . . . . . . . . . . 15 (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((#‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
114113impcom 445 . . . . . . . . . . . . . 14 (((#‘𝐹) = 3 ∧ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))
115 preq1 4212 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏})
116115eleq1d 2672 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸))
117 preq2 4213 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → {𝑐, 𝑎} = {𝑐, (𝑃‘0)})
118117eleq1d 2672 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑐, (𝑃‘0)} ∈ 𝐸))
119116, 1183anbi13d 1393 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸)))
120 neeq1 2844 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → (𝑎𝑏 ↔ (𝑃‘0) ≠ 𝑏))
121 neeq2 2845 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → (𝑐𝑎𝑐 ≠ (𝑃‘0)))
122120, 1213anbi13d 1393 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑃‘0) → ((𝑎𝑏𝑏𝑐𝑐𝑎) ↔ ((𝑃‘0) ≠ 𝑏𝑏𝑐𝑐 ≠ (𝑃‘0))))
123119, 122anbi12d 743 . . . . . . . . . . . . . . 15 (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏𝑏𝑐𝑐 ≠ (𝑃‘0)))))
124 preq2 4213 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)})
125124eleq1d 2672 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
126 preq1 4212 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐})
127126eleq1d 2672 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸))
128125, 1273anbi12d 1392 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸)))
129 neeq2 2845 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1)))
130 neeq1 2844 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → (𝑏𝑐 ↔ (𝑃‘1) ≠ 𝑐))
131129, 1303anbi12d 1392 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏𝑏𝑐𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐𝑐 ≠ (𝑃‘0))))
132128, 131anbi12d 743 . . . . . . . . . . . . . . 15 (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏𝑏𝑐𝑐 ≠ (𝑃‘0))) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐𝑐 ≠ (𝑃‘0)))))
133 preq2 4213 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)})
134133eleq1d 2672 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
135 preq1 4212 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝑃‘2) → {𝑐, (𝑃‘0)} = {(𝑃‘2), (𝑃‘0)})
136135eleq1d 2672 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑃‘2) → ({𝑐, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
137134, 1363anbi23d 1394 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)))
138 neeq2 2845 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2)))
139 neeq1 2844 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑃‘2) → (𝑐 ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘0)))
140138, 1393anbi23d 1394 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
141137, 140anbi12d 743 . . . . . . . . . . . . . . 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 3297 . . . . . . . . . . . . . 14 ((((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))
14364, 71, 114, 142syl12anc 1316 . . . . . . . . . . . . 13 (((#‘𝐹) = 3 ∧ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))
144143ex 449 . . . . . . . . . . . 12 ((#‘𝐹) = 3 → (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎))))
14538, 144sylbid 229 . . . . . . . . . . 11 ((#‘𝐹) = 3 → (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎))))
146145expd 451 . . . . . . . . . 10 ((#‘𝐹) = 3 → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))
147146com13 86 . . . . . . . . 9 (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))
1484, 147syl 17 . . . . . . . 8 ((𝐺 ∈ UPGraph ∧ 𝐹(1Walks‘𝐺)𝑃) → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))
149148expcom 450 . . . . . . 7 (𝐹(1Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎))))))
150149com23 84 . . . . . 6 (𝐹(1Walks‘𝐺)𝑃 → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎))))))
151150expd 451 . . . . 5 (𝐹(1Walks‘𝐺)𝑃 → (𝐹(PathS‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))))
1522, 151mpcom 37 . . . 4 (𝐹(PathS‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎))))))
153152imp 444 . . 3 ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))
1541, 153syl 17 . 2 (𝐹(CycleS‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((#‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))
1551543imp21 1269 1 ((𝐺 ∈ UPGraph ∧ 𝐹(CycleS‘𝐺)𝑃 ∧ (#‘𝐹) = 3) → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   ∧ w3a 1031   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  {cpr 4127  {ctp 4129   class class class wbr 4583  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  0cc0 9815  1c1 9816   + caddc 9818   < clt 9953  ℕcn 10897  2c2 10947  3c3 10948  ℕ0cn0 11169  ...cfz 12197  ..^cfzo 12334  #chash 12979  Vtxcvtx 25673   UPGraph cupgr 25747  Edgcedga 25792  1Walksc1wlks 40796  PathScpths 40919  CycleSccycls 40991 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-ifp 1007  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-2o 7448  df-oadd 7451  df-er 7629  df-map 7746  df-pm 7747  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-3 10957  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-fzo 12335  df-hash 12980  df-word 13154  df-uhgr 25724  df-upgr 25749  df-edga 25793  df-1wlks 40800  df-wlks 40801  df-trls 40901  df-pths 40923  df-cycls 40993 This theorem is referenced by:  umgr3v3e3cycl  41351
 Copyright terms: Public domain W3C validator