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

Theorem upgr4cycl4dv4e 41352
 Description: If there is a cycle of length 4 in a pseudograph, there are four (different) vertices in the graph which are mutually connected by edges. (Contributed by Alexander van der Vekens, 9-Nov-2017.) (Revised by AV, 13-Feb-2021.)
Hypotheses
Ref Expression
upgr4cycl4dv4e.v 𝑉 = (Vtx‘𝐺)
upgr4cycl4dv4e.e 𝐸 = (Edg‘𝐺)
Assertion
Ref Expression
upgr4cycl4dv4e ((𝐺 ∈ UPGraph ∧ 𝐹(CycleS‘𝐺)𝑃 ∧ (#‘𝐹) = 4) → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))
Distinct variable groups:   𝐸,𝑎,𝑏,𝑐,𝑑   𝑃,𝑎,𝑏,𝑐,𝑑   𝑉,𝑎,𝑏,𝑐,𝑑
Allowed substitution hints:   𝐹(𝑎,𝑏,𝑐,𝑑)   𝐺(𝑎,𝑏,𝑐,𝑑)

Proof of Theorem upgr4cycl4dv4e
Dummy variable 𝑘 is distinct from all other variables.
StepHypRef Expression
1 cyclprop 40999 . . 3 (𝐹(CycleS‘𝐺)𝑃 → (𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))
2 pthis1wlk 40933 . . . . 5 (𝐹(PathS‘𝐺)𝑃𝐹(1Walks‘𝐺)𝑃)
3 upgr4cycl4dv4e.e . . . . . . . . . 10 𝐸 = (Edg‘𝐺)
43upgr1wlkvtxedg 40853 . . . . . . . . 9 ((𝐺 ∈ UPGraph ∧ 𝐹(1Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)
5 fveq2 6103 . . . . . . . . . . . . . . 15 ((#‘𝐹) = 4 → (𝑃‘(#‘𝐹)) = (𝑃‘4))
65eqeq2d 2620 . . . . . . . . . . . . . 14 ((#‘𝐹) = 4 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) ↔ (𝑃‘0) = (𝑃‘4)))
76anbi2d 736 . . . . . . . . . . . . 13 ((#‘𝐹) = 4 → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ↔ (𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4))))
8 oveq2 6557 . . . . . . . . . . . . . . . 16 ((#‘𝐹) = 4 → (0..^(#‘𝐹)) = (0..^4))
9 fzo0to42pr 12422 . . . . . . . . . . . . . . . 16 (0..^4) = ({0, 1} ∪ {2, 3})
108, 9syl6eq 2660 . . . . . . . . . . . . . . 15 ((#‘𝐹) = 4 → (0..^(#‘𝐹)) = ({0, 1} ∪ {2, 3}))
1110raleqdv 3121 . . . . . . . . . . . . . 14 ((#‘𝐹) = 4 → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
12 ralunb 3756 . . . . . . . . . . . . . . 15 (∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (∀𝑘 ∈ {0, 1} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ∧ ∀𝑘 ∈ {2, 3} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
13 c0ex 9913 . . . . . . . . . . . . . . . . 17 0 ∈ V
14 1ex 9914 . . . . . . . . . . . . . . . . 17 1 ∈ V
15 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 0 → (𝑃𝑘) = (𝑃‘0))
16 oveq1 6556 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 0 → (𝑘 + 1) = (0 + 1))
17 0p1e1 11009 . . . . . . . . . . . . . . . . . . . . 21 (0 + 1) = 1
1816, 17syl6eq 2660 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 0 → (𝑘 + 1) = 1)
1918fveq2d 6107 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1))
2015, 19preq12d 4220 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)})
2120eleq1d 2672 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
22 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 1 → (𝑃𝑘) = (𝑃‘1))
23 oveq1 6556 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
24 1p1e2 11011 . . . . . . . . . . . . . . . . . . . . 21 (1 + 1) = 2
2523, 24syl6eq 2660 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 1 → (𝑘 + 1) = 2)
2625fveq2d 6107 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2))
2722, 26preq12d 4220 . . . . . . . . . . . . . . . . . 18 (𝑘 = 1 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)})
2827eleq1d 2672 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
2913, 14, 21, 28ralpr 4185 . . . . . . . . . . . . . . . 16 (∀𝑘 ∈ {0, 1} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
30 2ex 10969 . . . . . . . . . . . . . . . . 17 2 ∈ V
31 3ex 10973 . . . . . . . . . . . . . . . . 17 3 ∈ V
32 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 2 → (𝑃𝑘) = (𝑃‘2))
33 oveq1 6556 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 2 → (𝑘 + 1) = (2 + 1))
34 2p1e3 11028 . . . . . . . . . . . . . . . . . . . . 21 (2 + 1) = 3
3533, 34syl6eq 2660 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 2 → (𝑘 + 1) = 3)
3635fveq2d 6107 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3))
3732, 36preq12d 4220 . . . . . . . . . . . . . . . . . 18 (𝑘 = 2 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)})
3837eleq1d 2672 . . . . . . . . . . . . . . . . 17 (𝑘 = 2 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
39 fveq2 6103 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 3 → (𝑃𝑘) = (𝑃‘3))
40 oveq1 6556 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 3 → (𝑘 + 1) = (3 + 1))
41 3p1e4 11030 . . . . . . . . . . . . . . . . . . . . 21 (3 + 1) = 4
4240, 41syl6eq 2660 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 3 → (𝑘 + 1) = 4)
4342fveq2d 6107 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 3 → (𝑃‘(𝑘 + 1)) = (𝑃‘4))
4439, 43preq12d 4220 . . . . . . . . . . . . . . . . . 18 (𝑘 = 3 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘3), (𝑃‘4)})
4544eleq1d 2672 . . . . . . . . . . . . . . . . 17 (𝑘 = 3 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))
4630, 31, 38, 45ralpr 4185 . . . . . . . . . . . . . . . 16 (∀𝑘 ∈ {2, 3} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))
4729, 46anbi12i 729 . . . . . . . . . . . . . . 15 ((∀𝑘 ∈ {0, 1} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ∧ ∀𝑘 ∈ {2, 3} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))
4812, 47bitri 263 . . . . . . . . . . . . . 14 (∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))
4911, 48syl6bb 275 . . . . . . . . . . . . 13 ((#‘𝐹) = 4 → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))))
507, 49anbi12d 743 . . . . . . . . . . . 12 ((#‘𝐹) = 4 → (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))))
51 preq2 4213 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃‘4) = (𝑃‘0) → {(𝑃‘3), (𝑃‘4)} = {(𝑃‘3), (𝑃‘0)})
5251eleq1d 2672 . . . . . . . . . . . . . . . . . . . 20 ((𝑃‘4) = (𝑃‘0) → ({(𝑃‘3), (𝑃‘4)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
5352eqcoms 2618 . . . . . . . . . . . . . . . . . . 19 ((𝑃‘0) = (𝑃‘4) → ({(𝑃‘3), (𝑃‘4)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
5453anbi2d 736 . . . . . . . . . . . . . . . . . 18 ((𝑃‘0) = (𝑃‘4) → (({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸) ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
5554anbi2d 736 . . . . . . . . . . . . . . . . 17 ((𝑃‘0) = (𝑃‘4) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
5655adantl 481 . . . . . . . . . . . . . . . 16 ((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (𝑃‘0) = (𝑃‘4)) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
57 4nn0 11188 . . . . . . . . . . . . . . . . . . 19 4 ∈ ℕ0
5857a1i 11 . . . . . . . . . . . . . . . . . 18 (((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) → 4 ∈ ℕ0)
59 upgr4cycl4dv4e.v . . . . . . . . . . . . . . . . . . . . 21 𝑉 = (Vtx‘𝐺)
60591wlkp 40821 . . . . . . . . . . . . . . . . . . . 20 (𝐹(1Walks‘𝐺)𝑃𝑃:(0...(#‘𝐹))⟶𝑉)
61 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . 22 ((#‘𝐹) = 4 → (0...(#‘𝐹)) = (0...4))
6261feq2d 5944 . . . . . . . . . . . . . . . . . . . . 21 ((#‘𝐹) = 4 → (𝑃:(0...(#‘𝐹))⟶𝑉𝑃:(0...4)⟶𝑉))
6362biimpcd 238 . . . . . . . . . . . . . . . . . . . 20 (𝑃:(0...(#‘𝐹))⟶𝑉 → ((#‘𝐹) = 4 → 𝑃:(0...4)⟶𝑉))
642, 60, 633syl 18 . . . . . . . . . . . . . . . . . . 19 (𝐹(PathS‘𝐺)𝑃 → ((#‘𝐹) = 4 → 𝑃:(0...4)⟶𝑉))
6564impcom 445 . . . . . . . . . . . . . . . . . 18 (((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) → 𝑃:(0...4)⟶𝑉)
66 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → 4 ∈ ℕ0)
67 0nn0 11184 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ ℕ0
6867a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → 0 ∈ ℕ0)
69 4pos 10993 . . . . . . . . . . . . . . . . . . . . . . . 24 0 < 4
7069a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → 0 < 4)
7166, 68, 703jca 1235 . . . . . . . . . . . . . . . . . . . . . 22 (4 ∈ ℕ0 → (4 ∈ ℕ0 ∧ 0 ∈ ℕ0 ∧ 0 < 4))
72 fvffz0 12326 . . . . . . . . . . . . . . . . . . . . . 22 (((4 ∈ ℕ0 ∧ 0 ∈ ℕ0 ∧ 0 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉)
7371, 72sylan 487 . . . . . . . . . . . . . . . . . . . . 21 ((4 ∈ ℕ0𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉)
7473ad2antlr 759 . . . . . . . . . . . . . . . . . . . 20 (((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘0) ∈ 𝑉)
75 1nn0 11185 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ ℕ0
7675a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → 1 ∈ ℕ0)
77 1lt4 11076 . . . . . . . . . . . . . . . . . . . . . . . 24 1 < 4
7877a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → 1 < 4)
7966, 76, 783jca 1235 . . . . . . . . . . . . . . . . . . . . . 22 (4 ∈ ℕ0 → (4 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 4))
80 fvffz0 12326 . . . . . . . . . . . . . . . . . . . . . 22 (((4 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
8179, 80sylan 487 . . . . . . . . . . . . . . . . . . . . 21 ((4 ∈ ℕ0𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
8281ad2antlr 759 . . . . . . . . . . . . . . . . . . . 20 (((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘1) ∈ 𝑉)
83 2nn0 11186 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℕ0
8483a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (4 ∈ ℕ0 → 2 ∈ ℕ0)
85 2lt4 11075 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 < 4
8685a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (4 ∈ ℕ0 → 2 < 4)
8766, 84, 863jca 1235 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → (4 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 4))
88 fvffz0 12326 . . . . . . . . . . . . . . . . . . . . . . 23 (((4 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
8987, 88sylan 487 . . . . . . . . . . . . . . . . . . . . . 22 ((4 ∈ ℕ0𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
9089ad2antlr 759 . . . . . . . . . . . . . . . . . . . . 21 (((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘2) ∈ 𝑉)
91 3nn0 11187 . . . . . . . . . . . . . . . . . . . . . . . . 25 3 ∈ ℕ0
9291a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (4 ∈ ℕ0 → 3 ∈ ℕ0)
93 3lt4 11074 . . . . . . . . . . . . . . . . . . . . . . . . 25 3 < 4
9493a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (4 ∈ ℕ0 → 3 < 4)
9566, 92, 943jca 1235 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → (4 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 3 < 4))
96 fvffz0 12326 . . . . . . . . . . . . . . . . . . . . . . 23 (((4 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 3 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉)
9795, 96sylan 487 . . . . . . . . . . . . . . . . . . . . . 22 ((4 ∈ ℕ0𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉)
9897ad2antlr 759 . . . . . . . . . . . . . . . . . . . . 21 (((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘3) ∈ 𝑉)
99 simpr 476 . . . . . . . . . . . . . . . . . . . . 21 (((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
100 simplr 788 . . . . . . . . . . . . . . . . . . . . . . 23 ((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) → 𝐹(PathS‘𝐺)𝑃)
101 breq2 4587 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((#‘𝐹) = 4 → (1 < (#‘𝐹) ↔ 1 < 4))
10277, 101mpbiri 247 . . . . . . . . . . . . . . . . . . . . . . . 24 ((#‘𝐹) = 4 → 1 < (#‘𝐹))
103102ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . 23 ((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) → 1 < (#‘𝐹))
104 simpll 786 . . . . . . . . . . . . . . . . . . . . . . 23 ((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) → (#‘𝐹) = 4)
1058ad2antrr 758 . . . . . . . . . . . . . . . . . . . . . . 23 ((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) → (0..^(#‘𝐹)) = (0..^4))
106 4nn 11064 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 4 ∈ ℕ
107 lbfzo0 12375 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0 ∈ (0..^4) ↔ 4 ∈ ℕ)
108106, 107mpbir 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 0 ∈ (0..^4)
109 eleq2 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((0..^(#‘𝐹)) = (0..^4) → (0 ∈ (0..^(#‘𝐹)) ↔ 0 ∈ (0..^4)))
110108, 109mpbiri 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0..^(#‘𝐹)) = (0..^4) → 0 ∈ (0..^(#‘𝐹)))
111110adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → 0 ∈ (0..^(#‘𝐹)))
112 pthdadjvtx 40936 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 0 ∈ (0..^(#‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
113111, 112syl3an3 1353 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
114 1e0p1 11428 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 = (0 + 1)
115114fveq2i 6106 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃‘1) = (𝑃‘(0 + 1))
116115neeq2i 2847 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 + 1)))
117113, 116sylibr 223 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘1))
118 simp1 1054 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → 𝐹(PathS‘𝐺)𝑃)
119 elfzo0 12376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (2 ∈ (0..^4) ↔ (2 ∈ ℕ0 ∧ 4 ∈ ℕ ∧ 2 < 4))
12083, 106, 85, 119mpbir3an 1237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ∈ (0..^4)
121 2ne0 10990 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ≠ 0
122 fzo1fzo0n0 12386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (2 ∈ (1..^4) ↔ (2 ∈ (0..^4) ∧ 2 ≠ 0))
123120, 121, 122mpbir2an 957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2 ∈ (1..^4)
124 oveq2 6557 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((#‘𝐹) = 4 → (1..^(#‘𝐹)) = (1..^4))
125123, 124syl5eleqr 2695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐹) = 4 → 2 ∈ (1..^(#‘𝐹)))
126 0elfz 12305 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (4 ∈ ℕ0 → 0 ∈ (0...4))
12757, 126ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 0 ∈ (0...4)
128127, 61syl5eleqr 2695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐹) = 4 → 0 ∈ (0...(#‘𝐹)))
129121a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐹) = 4 → 2 ≠ 0)
130125, 128, 1293jca 1235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝐹) = 4 → (2 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 2 ≠ 0))
131130adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → (2 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 2 ≠ 0))
1321313ad2ant3 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (2 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 2 ≠ 0))
133 pthdivtx 40935 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(PathS‘𝐺)𝑃 ∧ (2 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 2 ≠ 0)) → (𝑃‘2) ≠ (𝑃‘0))
134118, 132, 133syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘0))
135134necomd 2837 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘2))
136 elfzo0 12376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (3 ∈ (0..^4) ↔ (3 ∈ ℕ0 ∧ 4 ∈ ℕ ∧ 3 < 4))
13791, 106, 93, 136mpbir3an 1237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3 ∈ (0..^4)
138 3ne0 10992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3 ≠ 0
139 fzo1fzo0n0 12386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (3 ∈ (1..^4) ↔ (3 ∈ (0..^4) ∧ 3 ≠ 0))
140137, 138, 139mpbir2an 957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3 ∈ (1..^4)
141140, 124syl5eleqr 2695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐹) = 4 → 3 ∈ (1..^(#‘𝐹)))
142138a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐹) = 4 → 3 ≠ 0)
143141, 128, 1423jca 1235 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝐹) = 4 → (3 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 3 ≠ 0))
144143adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → (3 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 3 ≠ 0))
1451443ad2ant3 1077 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (3 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 3 ≠ 0))
146 pthdivtx 40935 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(PathS‘𝐺)𝑃 ∧ (3 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 3 ≠ 0)) → (𝑃‘3) ≠ (𝑃‘0))
147118, 145, 146syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘3) ≠ (𝑃‘0))
148147necomd 2837 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘3))
149117, 135, 1483jca 1235 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)))
150 elfzo0 12376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 ∈ (0..^4) ↔ (1 ∈ ℕ0 ∧ 4 ∈ ℕ ∧ 1 < 4))
15175, 106, 77, 150mpbir3an 1237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ (0..^4)
152 eleq2 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((0..^(#‘𝐹)) = (0..^4) → (1 ∈ (0..^(#‘𝐹)) ↔ 1 ∈ (0..^4)))
153151, 152mpbiri 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0..^(#‘𝐹)) = (0..^4) → 1 ∈ (0..^(#‘𝐹)))
154153adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → 1 ∈ (0..^(#‘𝐹)))
155 pthdadjvtx 40936 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 1 ∈ (0..^(#‘𝐹))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
156154, 155syl3an3 1353 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
157 df-2 10956 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2 = (1 + 1)
158157fveq2i 6106 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃‘2) = (𝑃‘(1 + 1))
159158neeq2i 2847 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 + 1)))
160156, 159sylibr 223 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘2))
161 ax-1ne0 9884 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 ≠ 0
162 fzo1fzo0n0 12386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (1 ∈ (1..^4) ↔ (1 ∈ (0..^4) ∧ 1 ≠ 0))
163151, 161, 162mpbir2an 957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1 ∈ (1..^4)
164163, 124syl5eleqr 2695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝐹) = 4 → 1 ∈ (1..^(#‘𝐹)))
165 3re 10971 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3 ∈ ℝ
166 4re 10974 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 4 ∈ ℝ
167165, 166, 93ltleii 10039 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3 ≤ 4
168 elfz2nn0 12300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (3 ∈ (0...4) ↔ (3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ∧ 3 ≤ 4))
16991, 57, 167, 168mpbir3an 1237 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3 ∈ (0...4)
170169, 61syl5eleqr 2695 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝐹) = 4 → 3 ∈ (0...(#‘𝐹)))
171 1re 9918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 ∈ ℝ
172 1lt3 11073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 < 3
173171, 172ltneii 10029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1 ≠ 3
174173a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝐹) = 4 → 1 ≠ 3)
175164, 170, 1743jca 1235 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((#‘𝐹) = 4 → (1 ∈ (1..^(#‘𝐹)) ∧ 3 ∈ (0...(#‘𝐹)) ∧ 1 ≠ 3))
176175adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → (1 ∈ (1..^(#‘𝐹)) ∧ 3 ∈ (0...(#‘𝐹)) ∧ 1 ≠ 3))
1771763ad2ant3 1077 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (1 ∈ (1..^(#‘𝐹)) ∧ 3 ∈ (0...(#‘𝐹)) ∧ 1 ≠ 3))
178 pthdivtx 40935 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(PathS‘𝐺)𝑃 ∧ (1 ∈ (1..^(#‘𝐹)) ∧ 3 ∈ (0...(#‘𝐹)) ∧ 1 ≠ 3)) → (𝑃‘1) ≠ (𝑃‘3))
179118, 177, 178syl2anc 691 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘3))
180 eleq2 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((0..^(#‘𝐹)) = (0..^4) → (2 ∈ (0..^(#‘𝐹)) ↔ 2 ∈ (0..^4)))
181120, 180mpbiri 247 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0..^(#‘𝐹)) = (0..^4) → 2 ∈ (0..^(#‘𝐹)))
182181adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → 2 ∈ (0..^(#‘𝐹)))
183 pthdadjvtx 40936 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 2 ∈ (0..^(#‘𝐹))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
184182, 183syl3an3 1353 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
185 df-3 10957 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 3 = (2 + 1)
186185fveq2i 6106 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃‘3) = (𝑃‘(2 + 1))
187186neeq2i 2847 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))
188184, 187sylibr 223 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘3))
189160, 179, 1883jca 1235 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3)))
190149, 189jca 553 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
191100, 103, 104, 105, 190syl112anc 1322 . . . . . . . . . . . . . . . . . . . . . 22 ((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
192191adantr 480 . . . . . . . . . . . . . . . . . . . . 21 (((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
193 preq2 4213 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)})
194193eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
195194anbi2d 736 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸)))
196 preq1 4212 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = (𝑃‘2) → {𝑐, 𝑑} = {(𝑃‘2), 𝑑})
197196eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑃‘2) → ({𝑐, 𝑑} ∈ 𝐸 ↔ {(𝑃‘2), 𝑑} ∈ 𝐸))
198197anbi1d 737 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑃‘2) → (({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))
199195, 198anbi12d 743 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = (𝑃‘2) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
200 neeq2 2845 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑃‘2) → ((𝑃‘0) ≠ 𝑐 ↔ (𝑃‘0) ≠ (𝑃‘2)))
2012003anbi2d 1396 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑)))
202 neeq2 2845 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2)))
203 neeq1 2844 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑃‘2) → (𝑐𝑑 ↔ (𝑃‘2) ≠ 𝑑))
204202, 2033anbi13d 1393 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑃‘2) → (((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑) ↔ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑)))
205201, 204anbi12d 743 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = (𝑃‘2) → ((((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑))))
206199, 205anbi12d 743 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 = (𝑃‘2) → (((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑))) ↔ ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑)))))
207 preq2 4213 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = (𝑃‘3) → {(𝑃‘2), 𝑑} = {(𝑃‘2), (𝑃‘3)})
208207eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑃‘3) → ({(𝑃‘2), 𝑑} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
209 preq1 4212 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = (𝑃‘3) → {𝑑, (𝑃‘0)} = {(𝑃‘3), (𝑃‘0)})
210209eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑃‘3) → ({𝑑, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
211208, 210anbi12d 743 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 = (𝑃‘3) → (({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
212211anbi2d 736 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = (𝑃‘3) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
213 neeq2 2845 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑃‘3) → ((𝑃‘0) ≠ 𝑑 ↔ (𝑃‘0) ≠ (𝑃‘3)))
2142133anbi3d 1397 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 = (𝑃‘3) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3))))
215 neeq2 2845 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑃‘3) → ((𝑃‘1) ≠ 𝑑 ↔ (𝑃‘1) ≠ (𝑃‘3)))
216 neeq2 2845 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑃‘3) → ((𝑃‘2) ≠ 𝑑 ↔ (𝑃‘2) ≠ (𝑃‘3)))
217215, 2163anbi23d 1394 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 = (𝑃‘3) → (((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑) ↔ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
218214, 217anbi12d 743 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = (𝑃‘3) → ((((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3)))))
219212, 218anbi12d 743 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 = (𝑃‘3) → (((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑))) ↔ ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))))
220206, 219rspc2ev 3295 . . . . . . . . . . . . . . . . . . . . 21 (((𝑃‘2) ∈ 𝑉 ∧ (𝑃‘3) ∈ 𝑉 ∧ ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))) → ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑))))
22190, 98, 99, 192, 220syl112anc 1322 . . . . . . . . . . . . . . . . . . . 20 (((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑))))
22274, 82, 2213jca 1235 . . . . . . . . . . . . . . . . . . 19 (((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑)))))
223222exp31 628 . . . . . . . . . . . . . . . . . 18 (((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) → ((4 ∈ ℕ0𝑃:(0...4)⟶𝑉) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑)))))))
22458, 65, 223mp2and 711 . . . . . . . . . . . . . . . . 17 (((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑))))))
225224adantr 480 . . . . . . . . . . . . . . . 16 ((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (𝑃‘0) = (𝑃‘4)) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑))))))
22656, 225sylbid 229 . . . . . . . . . . . . . . 15 ((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (𝑃‘0) = (𝑃‘4)) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑))))))
227226exp31 628 . . . . . . . . . . . . . 14 ((#‘𝐹) = 4 → (𝐹(PathS‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘4) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑))))))))
228227imp4c 615 . . . . . . . . . . . . 13 ((#‘𝐹) = 4 → (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑))))))
229 preq1 4212 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏})
230229eleq1d 2672 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸))
231230anbi1d 737 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
232 preq2 4213 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑃‘0) → {𝑑, 𝑎} = {𝑑, (𝑃‘0)})
233232eleq1d 2672 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → ({𝑑, 𝑎} ∈ 𝐸 ↔ {𝑑, (𝑃‘0)} ∈ 𝐸))
234233anbi2d 736 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → (({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸) ↔ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))
235231, 234anbi12d 743 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
236 neeq1 2844 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → (𝑎𝑏 ↔ (𝑃‘0) ≠ 𝑏))
237 neeq1 2844 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → (𝑎𝑐 ↔ (𝑃‘0) ≠ 𝑐))
238 neeq1 2844 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → (𝑎𝑑 ↔ (𝑃‘0) ≠ 𝑑))
239236, 237, 2383anbi123d 1391 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → ((𝑎𝑏𝑎𝑐𝑎𝑑) ↔ ((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑)))
240239anbi1d 737 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑃‘0) → (((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)) ↔ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))
241235, 240anbi12d 743 . . . . . . . . . . . . . . 15 (𝑎 = (𝑃‘0) → (((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))) ↔ ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))
2422412rexbidv 3039 . . . . . . . . . . . . . 14 (𝑎 = (𝑃‘0) → (∃𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))) ↔ ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))
243 preq2 4213 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)})
244243eleq1d 2672 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
245 preq1 4212 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐})
246245eleq1d 2672 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸))
247244, 246anbi12d 743 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸)))
248247anbi1d 737 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
249 neeq2 2845 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1)))
2502493anbi1d 1395 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑)))
251 neeq1 2844 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → (𝑏𝑐 ↔ (𝑃‘1) ≠ 𝑐))
252 neeq1 2844 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → (𝑏𝑑 ↔ (𝑃‘1) ≠ 𝑑))
253251, 2523anbi12d 1392 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → ((𝑏𝑐𝑏𝑑𝑐𝑑) ↔ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑)))
254250, 253anbi12d 743 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑃‘1) → ((((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑))))
255248, 254anbi12d 743 . . . . . . . . . . . . . . 15 (𝑏 = (𝑃‘1) → (((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))) ↔ ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑)))))
2562552rexbidv 3039 . . . . . . . . . . . . . 14 (𝑏 = (𝑃‘1) → (∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))) ↔ ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑)))))
257242, 256rspc2ev 3295 . . . . . . . . . . . . 13 (((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑)))) → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))
258228, 257syl6 34 . . . . . . . . . . . 12 ((#‘𝐹) = 4 → (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))) → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))
25950, 258sylbid 229 . . . . . . . . . . 11 ((#‘𝐹) = 4 → (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))
260259expd 451 . . . . . . . . . 10 ((#‘𝐹) = 4 → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))
261260com13 86 . . . . . . . . 9 (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))
2624, 261syl 17 . . . . . . . 8 ((𝐺 ∈ UPGraph ∧ 𝐹(1Walks‘𝐺)𝑃) → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))
263262expcom 450 . . . . . . 7 (𝐹(1Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))))
264263com23 84 . . . . . 6 (𝐹(1Walks‘𝐺)𝑃 → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))))
265264expd 451 . . . . 5 (𝐹(1Walks‘𝐺)𝑃 → (𝐹(PathS‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))))
2662, 265mpcom 37 . . . 4 (𝐹(PathS‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))))
267266imp 444 . . 3 ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))
2681, 267syl 17 . 2 (𝐹(CycleS‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))
2692683imp21 1269 1 ((𝐺 ∈ UPGraph ∧ 𝐹(CycleS‘𝐺)𝑃 ∧ (#‘𝐹) = 4) → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))
 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   ∪ cun 3538  {cpr 4127   class class class wbr 4583  ⟶wf 5800  ‘cfv 5804  (class class class)co 6549  0cc0 9815  1c1 9816   + caddc 9818   < clt 9953   ≤ cle 9954  ℕcn 10897  2c2 10947  3c3 10948  4c4 10949  ℕ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-4 10958  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:  n4cyclfrgr  41461
 Copyright terms: Public domain W3C validator