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

Theorem upgr3v3e3cycl 26906
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 26557 . . 3 (𝐹(Cycles‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))
2 pthiswlk 26492 . . . . 5 (𝐹(Paths‘𝐺)𝑃𝐹(Walks‘𝐺)𝑃)
3 upgr3v3e3cycl.e . . . . . . . . . 10 𝐸 = (Edg‘𝐺)
43upgrwlkvtxedg 26410 . . . . . . . . 9 ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)
5 fveq2 6148 . . . . . . . . . . . . . . 15 ((#‘𝐹) = 3 → (𝑃‘(#‘𝐹)) = (𝑃‘3))
65eqeq2d 2631 . . . . . . . . . . . . . 14 ((#‘𝐹) = 3 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) ↔ (𝑃‘0) = (𝑃‘3)))
76anbi2d 739 . . . . . . . . . . . . 13 ((#‘𝐹) = 3 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ↔ (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3))))
8 oveq2 6612 . . . . . . . . . . . . . . . 16 ((#‘𝐹) = 3 → (0..^(#‘𝐹)) = (0..^3))
9 fzo0to3tp 12495 . . . . . . . . . . . . . . . 16 (0..^3) = {0, 1, 2}
108, 9syl6eq 2671 . . . . . . . . . . . . . . 15 ((#‘𝐹) = 3 → (0..^(#‘𝐹)) = {0, 1, 2})
1110raleqdv 3133 . . . . . . . . . . . . . 14 ((#‘𝐹) = 3 → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ {0, 1, 2} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
12 c0ex 9978 . . . . . . . . . . . . . . 15 0 ∈ V
13 1ex 9979 . . . . . . . . . . . . . . 15 1 ∈ V
14 2ex 11036 . . . . . . . . . . . . . . 15 2 ∈ V
15 fveq2 6148 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (𝑃𝑘) = (𝑃‘0))
16 oveq1 6611 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 0 → (𝑘 + 1) = (0 + 1))
17 0p1e1 11076 . . . . . . . . . . . . . . . . . . 19 (0 + 1) = 1
1816, 17syl6eq 2671 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → (𝑘 + 1) = 1)
1918fveq2d 6152 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1))
2015, 19preq12d 4246 . . . . . . . . . . . . . . . 16 (𝑘 = 0 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)})
2120eleq1d 2683 . . . . . . . . . . . . . . 15 (𝑘 = 0 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
22 fveq2 6148 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → (𝑃𝑘) = (𝑃‘1))
23 oveq1 6611 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
24 1p1e2 11078 . . . . . . . . . . . . . . . . . . 19 (1 + 1) = 2
2523, 24syl6eq 2671 . . . . . . . . . . . . . . . . . 18 (𝑘 = 1 → (𝑘 + 1) = 2)
2625fveq2d 6152 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2))
2722, 26preq12d 4246 . . . . . . . . . . . . . . . 16 (𝑘 = 1 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)})
2827eleq1d 2683 . . . . . . . . . . . . . . 15 (𝑘 = 1 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
29 fveq2 6148 . . . . . . . . . . . . . . . . 17 (𝑘 = 2 → (𝑃𝑘) = (𝑃‘2))
30 oveq1 6611 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 2 → (𝑘 + 1) = (2 + 1))
31 2p1e3 11095 . . . . . . . . . . . . . . . . . . 19 (2 + 1) = 3
3230, 31syl6eq 2671 . . . . . . . . . . . . . . . . . 18 (𝑘 = 2 → (𝑘 + 1) = 3)
3332fveq2d 6152 . . . . . . . . . . . . . . . . 17 (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3))
3429, 33preq12d 4246 . . . . . . . . . . . . . . . 16 (𝑘 = 2 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)})
3534eleq1d 2683 . . . . . . . . . . . . . . 15 (𝑘 = 2 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
3612, 13, 14, 21, 28, 35raltp 4211 . . . . . . . . . . . . . 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 746 . . . . . . . . . . . 12 ((#‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))))
39 upgr3v3e3cycl.v . . . . . . . . . . . . . . . . . . 19 𝑉 = (Vtx‘𝐺)
4039wlkp 26382 . . . . . . . . . . . . . . . . . 18 (𝐹(Walks‘𝐺)𝑃𝑃:(0...(#‘𝐹))⟶𝑉)
41 oveq2 6612 . . . . . . . . . . . . . . . . . . . . 21 ((#‘𝐹) = 3 → (0...(#‘𝐹)) = (0...3))
4241feq2d 5988 . . . . . . . . . . . . . . . . . . . 20 ((#‘𝐹) = 3 → (𝑃:(0...(#‘𝐹))⟶𝑉𝑃:(0...3)⟶𝑉))
43 id 22 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃:(0...3)⟶𝑉𝑃:(0...3)⟶𝑉)
44 3nn0 11254 . . . . . . . . . . . . . . . . . . . . . . 23 3 ∈ ℕ0
45 0elfz 12377 . . . . . . . . . . . . . . . . . . . . . . 23 (3 ∈ ℕ0 → 0 ∈ (0...3))
4644, 45mp1i 13 . . . . . . . . . . . . . . . . . . . . . 22 (𝑃:(0...3)⟶𝑉 → 0 ∈ (0...3))
4743, 46ffvelrnd 6316 . . . . . . . . . . . . . . . . . . . . 21 (𝑃:(0...3)⟶𝑉 → (𝑃‘0) ∈ 𝑉)
48 1nn0 11252 . . . . . . . . . . . . . . . . . . . . . 22 1 ∈ ℕ0
49 1lt3 11140 . . . . . . . . . . . . . . . . . . . . . 22 1 < 3
50 fvffz0 12398 . . . . . . . . . . . . . . . . . . . . . . 23 (((3 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 3) ∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
5150ex 450 . . . . . . . . . . . . . . . . . . . . . 22 ((3 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 3) → (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉))
5244, 48, 49, 51mp3an 1421 . . . . . . . . . . . . . . . . . . . . 21 (𝑃:(0...3)⟶𝑉 → (𝑃‘1) ∈ 𝑉)
53 2nn0 11253 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ ℕ0
54 2lt3 11139 . . . . . . . . . . . . . . . . . . . . . 22 2 < 3
55 fvffz0 12398 . . . . . . . . . . . . . . . . . . . . . . 23 (((3 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 3) ∧ 𝑃:(0...3)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
5655ex 450 . . . . . . . . . . . . . . . . . . . . . 22 ((3 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 3) → (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉))
5744, 53, 54, 56mp3an 1421 . . . . . . . . . . . . . . . . . . . . 21 (𝑃:(0...3)⟶𝑉 → (𝑃‘2) ∈ 𝑉)
5847, 52, 573jca 1240 . . . . . . . . . . . . . . . . . . . 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 481 . . . . . . . . . . . . . . . 16 ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((#‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
6362adantr 481 . . . . . . . . . . . . . . 15 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((#‘𝐹) = 3 → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉)))
6463impcom 446 . . . . . . . . . . . . . 14 (((#‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉))
65 preq2 4239 . . . . . . . . . . . . . . . . . . . 20 ((𝑃‘3) = (𝑃‘0) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
6665eqcoms 2629 . . . . . . . . . . . . . . . . . . 19 ((𝑃‘0) = (𝑃‘3) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
6766adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → {(𝑃‘2), (𝑃‘3)} = {(𝑃‘2), (𝑃‘0)})
6867eleq1d 2683 . . . . . . . . . . . . . . . . 17 ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
69683anbi3d 1402 . . . . . . . . . . . . . . . 16 ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)))
7069biimpa 501 . . . . . . . . . . . . . . 15 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
7170adantl 482 . . . . . . . . . . . . . 14 (((#‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
72 simpll 789 . . . . . . . . . . . . . . . . . . 19 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → 𝐹(Paths‘𝐺)𝑃)
73 breq2 4617 . . . . . . . . . . . . . . . . . . . . 21 ((#‘𝐹) = 3 → (1 < (#‘𝐹) ↔ 1 < 3))
7449, 73mpbiri 248 . . . . . . . . . . . . . . . . . . . 20 ((#‘𝐹) = 3 → 1 < (#‘𝐹))
7574adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → 1 < (#‘𝐹))
76 3nn 11130 . . . . . . . . . . . . . . . . . . . . . 22 3 ∈ ℕ
77 lbfzo0 12448 . . . . . . . . . . . . . . . . . . . . . 22 (0 ∈ (0..^3) ↔ 3 ∈ ℕ)
7876, 77mpbir 221 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ (0..^3)
7978, 8syl5eleqr 2705 . . . . . . . . . . . . . . . . . . . 20 ((#‘𝐹) = 3 → 0 ∈ (0..^(#‘𝐹)))
8079adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → 0 ∈ (0..^(#‘𝐹)))
81 pthdadjvtx 26495 . . . . . . . . . . . . . . . . . . . 20 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 0 ∈ (0..^(#‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
82 1e0p1 11496 . . . . . . . . . . . . . . . . . . . . . 22 1 = (0 + 1)
8382fveq2i 6151 . . . . . . . . . . . . . . . . . . . . 21 (𝑃‘1) = (𝑃‘(0 + 1))
8483neeq2i 2855 . . . . . . . . . . . . . . . . . . . 20 ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 + 1)))
8581, 84sylibr 224 . . . . . . . . . . . . . . . . . . 19 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 0 ∈ (0..^(#‘𝐹))) → (𝑃‘0) ≠ (𝑃‘1))
8672, 75, 80, 85syl3anc 1323 . . . . . . . . . . . . . . . . . 18 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → (𝑃‘0) ≠ (𝑃‘1))
87 elfzo0 12449 . . . . . . . . . . . . . . . . . . . . . 22 (1 ∈ (0..^3) ↔ (1 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 1 < 3))
8848, 76, 49, 87mpbir3an 1242 . . . . . . . . . . . . . . . . . . . . 21 1 ∈ (0..^3)
8988, 8syl5eleqr 2705 . . . . . . . . . . . . . . . . . . . 20 ((#‘𝐹) = 3 → 1 ∈ (0..^(#‘𝐹)))
9089adantl 482 . . . . . . . . . . . . . . . . . . 19 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → 1 ∈ (0..^(#‘𝐹)))
91 pthdadjvtx 26495 . . . . . . . . . . . . . . . . . . . 20 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 1 ∈ (0..^(#‘𝐹))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
92 df-2 11023 . . . . . . . . . . . . . . . . . . . . . 22 2 = (1 + 1)
9392fveq2i 6151 . . . . . . . . . . . . . . . . . . . . 21 (𝑃‘2) = (𝑃‘(1 + 1))
9493neeq2i 2855 . . . . . . . . . . . . . . . . . . . 20 ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 + 1)))
9591, 94sylibr 224 . . . . . . . . . . . . . . . . . . 19 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 1 ∈ (0..^(#‘𝐹))) → (𝑃‘1) ≠ (𝑃‘2))
9672, 75, 90, 95syl3anc 1323 . . . . . . . . . . . . . . . . . 18 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → (𝑃‘1) ≠ (𝑃‘2))
97 elfzo0 12449 . . . . . . . . . . . . . . . . . . . . . . 23 (2 ∈ (0..^3) ↔ (2 ∈ ℕ0 ∧ 3 ∈ ℕ ∧ 2 < 3))
9853, 76, 54, 97mpbir3an 1242 . . . . . . . . . . . . . . . . . . . . . 22 2 ∈ (0..^3)
9998, 8syl5eleqr 2705 . . . . . . . . . . . . . . . . . . . . 21 ((#‘𝐹) = 3 → 2 ∈ (0..^(#‘𝐹)))
10099adantl 482 . . . . . . . . . . . . . . . . . . . 20 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → 2 ∈ (0..^(#‘𝐹)))
101 pthdadjvtx 26495 . . . . . . . . . . . . . . . . . . . 20 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 2 ∈ (0..^(#‘𝐹))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
10272, 75, 100, 101syl3anc 1323 . . . . . . . . . . . . . . . . . . 19 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
103 neeq2 2853 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘3)))
104 df-3 11024 . . . . . . . . . . . . . . . . . . . . . . . 24 3 = (2 + 1)
105104fveq2i 6151 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑃‘3) = (𝑃‘(2 + 1))
106105neeq2i 2855 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))
107103, 106syl6bb 276 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃‘0) = (𝑃‘3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
108107adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
109108adantr 481 . . . . . . . . . . . . . . . . . . 19 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → ((𝑃‘2) ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1))))
110102, 109mpbird 247 . . . . . . . . . . . . . . . . . 18 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → (𝑃‘2) ≠ (𝑃‘0))
11186, 96, 1103jca 1240 . . . . . . . . . . . . . . . . 17 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ (#‘𝐹) = 3) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))
112111ex 450 . . . . . . . . . . . . . . . 16 ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) → ((#‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
113112adantr 481 . . . . . . . . . . . . . . 15 (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ((#‘𝐹) = 3 → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
114113impcom 446 . . . . . . . . . . . . . 14 (((#‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))
115 preq1 4238 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏})
116115eleq1d 2683 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸))
117 preq2 4239 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → {𝑐, 𝑎} = {𝑐, (𝑃‘0)})
118117eleq1d 2683 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → ({𝑐, 𝑎} ∈ 𝐸 ↔ {𝑐, (𝑃‘0)} ∈ 𝐸))
119116, 1183anbi13d 1398 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸)))
120 neeq1 2852 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → (𝑎𝑏 ↔ (𝑃‘0) ≠ 𝑏))
121 neeq2 2853 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → (𝑐𝑎𝑐 ≠ (𝑃‘0)))
122120, 1213anbi13d 1398 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑃‘0) → ((𝑎𝑏𝑏𝑐𝑐𝑎) ↔ ((𝑃‘0) ≠ 𝑏𝑏𝑐𝑐 ≠ (𝑃‘0))))
123119, 122anbi12d 746 . . . . . . . . . . . . . . 15 (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏𝑏𝑐𝑐 ≠ (𝑃‘0)))))
124 preq2 4239 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)})
125124eleq1d 2683 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
126 preq1 4238 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐})
127126eleq1d 2683 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸))
128125, 1273anbi12d 1397 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸)))
129 neeq2 2853 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1)))
130 neeq1 2852 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → (𝑏𝑐 ↔ (𝑃‘1) ≠ 𝑐))
131129, 1303anbi12d 1397 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏𝑏𝑐𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐𝑐 ≠ (𝑃‘0))))
132128, 131anbi12d 746 . . . . . . . . . . . . . . 15 (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ 𝑏𝑏𝑐𝑐 ≠ (𝑃‘0))) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐𝑐 ≠ (𝑃‘0)))))
133 preq2 4239 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)})
134133eleq1d 2683 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
135 preq1 4238 . . . . . . . . . . . . . . . . . 18 (𝑐 = (𝑃‘2) → {𝑐, (𝑃‘0)} = {(𝑃‘2), (𝑃‘0)})
136135eleq1d 2683 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑃‘2) → ({𝑐, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸))
137134, 1363anbi23d 1399 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸 ∧ {𝑐, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸)))
138 neeq2 2853 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2)))
139 neeq1 2852 . . . . . . . . . . . . . . . . 17 (𝑐 = (𝑃‘2) → (𝑐 ≠ (𝑃‘0) ↔ (𝑃‘2) ≠ (𝑃‘0)))
140138, 1393anbi23d 1399 . . . . . . . . . . . . . . . 16 (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ 𝑐𝑐 ≠ (𝑃‘0)) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0))))
141137, 140anbi12d 746 . . . . . . . . . . . . . . 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 3310 . . . . . . . . . . . . . 14 ((((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ (𝑃‘2) ∈ 𝑉) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘0)} ∈ 𝐸) ∧ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘2) ≠ (𝑃‘0)))) → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))
14364, 71, 114, 142syl12anc 1321 . . . . . . . . . . . . 13 (((#‘𝐹) = 3 ∧ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))) → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))
144143ex 450 . . . . . . . . . . . 12 ((#‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘3)) ∧ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸 ∧ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸)) → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎))))
14538, 144sylbid 230 . . . . . . . . . . 11 ((#‘𝐹) = 3 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎))))
146145expd 452 . . . . . . . . . 10 ((#‘𝐹) = 3 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))
147146com13 88 . . . . . . . . 9 (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))
1484, 147syl 17 . . . . . . . 8 ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))
149148expcom 451 . . . . . . 7 (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎))))))
150149com23 86 . . . . . 6 (𝐹(Walks‘𝐺)𝑃 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎))))))
151150expd 452 . . . . 5 (𝐹(Walks‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))))
1522, 151mpcom 38 . . . 4 (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎))))))
153152imp 445 . . 3 ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))
1541, 153syl 17 . 2 (𝐹(Cycles‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((#‘𝐹) = 3 → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))))
1551543imp21 1274 1 ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (#‘𝐹) = 3) → ∃𝑎𝑉𝑏𝑉𝑐𝑉 (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸 ∧ {𝑐, 𝑎} ∈ 𝐸) ∧ (𝑎𝑏𝑏𝑐𝑐𝑎)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wne 2790  wral 2907  wrex 2908  {cpr 4150  {ctp 4152   class class class wbr 4613  wf 5843  cfv 5847  (class class class)co 6604  0cc0 9880  1c1 9881   + caddc 9883   < clt 10018  cn 10964  2c2 11014  3c3 11015  0cn0 11236  ...cfz 12268  ..^cfzo 12406  #chash 13057  Vtxcvtx 25774  Edgcedg 25839   UPGraph cupgr 25871  Walkscwlks 26362  Pathscpths 26477  Cyclesccycls 26549
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ifp 1012  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-2o 7506  df-oadd 7509  df-er 7687  df-map 7804  df-pm 7805  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-card 8709  df-cda 8934  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-nn 10965  df-2 11023  df-3 11024  df-n0 11237  df-xnn0 11308  df-z 11322  df-uz 11632  df-fz 12269  df-fzo 12407  df-hash 13058  df-word 13238  df-edg 25840  df-uhgr 25849  df-upgr 25873  df-wlks 26365  df-trls 26458  df-pths 26481  df-cycls 26551
This theorem is referenced by:  umgr3v3e3cycl  26910
  Copyright terms: Public domain W3C validator