Users' Mathboxes 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 41374
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 41021 . . 3 (𝐹(CycleS‘𝐺)𝑃 → (𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))
2 pthis1wlk 40955 . . . . 5 (𝐹(PathS‘𝐺)𝑃𝐹(1Walks‘𝐺)𝑃)
3 upgr4cycl4dv4e.e . . . . . . . . . 10 𝐸 = (Edg‘𝐺)
43upgr1wlkvtxedg 40875 . . . . . . . . 9 ((𝐺 ∈ UPGraph ∧ 𝐹(1Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)
5 fveq2 6088 . . . . . . . . . . . . . . 15 ((#‘𝐹) = 4 → (𝑃‘(#‘𝐹)) = (𝑃‘4))
65eqeq2d 2619 . . . . . . . . . . . . . 14 ((#‘𝐹) = 4 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) ↔ (𝑃‘0) = (𝑃‘4)))
76anbi2d 735 . . . . . . . . . . . . 13 ((#‘𝐹) = 4 → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ↔ (𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4))))
8 oveq2 6535 . . . . . . . . . . . . . . . 16 ((#‘𝐹) = 4 → (0..^(#‘𝐹)) = (0..^4))
9 fzo0to42pr 12380 . . . . . . . . . . . . . . . 16 (0..^4) = ({0, 1} ∪ {2, 3})
108, 9syl6eq 2659 . . . . . . . . . . . . . . 15 ((#‘𝐹) = 4 → (0..^(#‘𝐹)) = ({0, 1} ∪ {2, 3}))
1110raleqdv 3120 . . . . . . . . . . . . . 14 ((#‘𝐹) = 4 → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
12 ralunb 3755 . . . . . . . . . . . . . . 15 (∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (∀𝑘 ∈ {0, 1} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ∧ ∀𝑘 ∈ {2, 3} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
13 c0ex 9891 . . . . . . . . . . . . . . . . 17 0 ∈ V
14 1ex 9892 . . . . . . . . . . . . . . . . 17 1 ∈ V
15 fveq2 6088 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 0 → (𝑃𝑘) = (𝑃‘0))
16 oveq1 6534 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 0 → (𝑘 + 1) = (0 + 1))
17 0p1e1 10982 . . . . . . . . . . . . . . . . . . . . 21 (0 + 1) = 1
1816, 17syl6eq 2659 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 0 → (𝑘 + 1) = 1)
1918fveq2d 6092 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1))
2015, 19preq12d 4219 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)})
2120eleq1d 2671 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
22 fveq2 6088 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 1 → (𝑃𝑘) = (𝑃‘1))
23 oveq1 6534 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
24 1p1e2 10984 . . . . . . . . . . . . . . . . . . . . 21 (1 + 1) = 2
2523, 24syl6eq 2659 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 1 → (𝑘 + 1) = 2)
2625fveq2d 6092 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2))
2722, 26preq12d 4219 . . . . . . . . . . . . . . . . . 18 (𝑘 = 1 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)})
2827eleq1d 2671 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
2913, 14, 21, 28ralpr 4184 . . . . . . . . . . . . . . . 16 (∀𝑘 ∈ {0, 1} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
30 2ex 10942 . . . . . . . . . . . . . . . . 17 2 ∈ V
31 3ex 10946 . . . . . . . . . . . . . . . . 17 3 ∈ V
32 fveq2 6088 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 2 → (𝑃𝑘) = (𝑃‘2))
33 oveq1 6534 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 2 → (𝑘 + 1) = (2 + 1))
34 2p1e3 11001 . . . . . . . . . . . . . . . . . . . . 21 (2 + 1) = 3
3533, 34syl6eq 2659 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 2 → (𝑘 + 1) = 3)
3635fveq2d 6092 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3))
3732, 36preq12d 4219 . . . . . . . . . . . . . . . . . 18 (𝑘 = 2 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)})
3837eleq1d 2671 . . . . . . . . . . . . . . . . 17 (𝑘 = 2 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
39 fveq2 6088 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 3 → (𝑃𝑘) = (𝑃‘3))
40 oveq1 6534 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 3 → (𝑘 + 1) = (3 + 1))
41 3p1e4 11003 . . . . . . . . . . . . . . . . . . . . 21 (3 + 1) = 4
4240, 41syl6eq 2659 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 3 → (𝑘 + 1) = 4)
4342fveq2d 6092 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 3 → (𝑃‘(𝑘 + 1)) = (𝑃‘4))
4439, 43preq12d 4219 . . . . . . . . . . . . . . . . . 18 (𝑘 = 3 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘3), (𝑃‘4)})
4544eleq1d 2671 . . . . . . . . . . . . . . . . 17 (𝑘 = 3 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))
4630, 31, 38, 45ralpr 4184 . . . . . . . . . . . . . . . 16 (∀𝑘 ∈ {2, 3} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))
4729, 46anbi12i 728 . . . . . . . . . . . . . . 15 ((∀𝑘 ∈ {0, 1} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ∧ ∀𝑘 ∈ {2, 3} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))
4812, 47bitri 262 . . . . . . . . . . . . . 14 (∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))
4911, 48syl6bb 274 . . . . . . . . . . . . 13 ((#‘𝐹) = 4 → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))))
507, 49anbi12d 742 . . . . . . . . . . . 12 ((#‘𝐹) = 4 → (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))))
51 preq2 4212 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃‘4) = (𝑃‘0) → {(𝑃‘3), (𝑃‘4)} = {(𝑃‘3), (𝑃‘0)})
5251eleq1d 2671 . . . . . . . . . . . . . . . . . . . 20 ((𝑃‘4) = (𝑃‘0) → ({(𝑃‘3), (𝑃‘4)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
5352eqcoms 2617 . . . . . . . . . . . . . . . . . . 19 ((𝑃‘0) = (𝑃‘4) → ({(𝑃‘3), (𝑃‘4)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
5453anbi2d 735 . . . . . . . . . . . . . . . . . 18 ((𝑃‘0) = (𝑃‘4) → (({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸) ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
5554anbi2d 735 . . . . . . . . . . . . . . . . 17 ((𝑃‘0) = (𝑃‘4) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
5655adantl 480 . . . . . . . . . . . . . . . 16 ((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (𝑃‘0) = (𝑃‘4)) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
57 4nn0 11161 . . . . . . . . . . . . . . . . . . 19 4 ∈ ℕ0
5857a1i 11 . . . . . . . . . . . . . . . . . 18 (((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) → 4 ∈ ℕ0)
59 upgr4cycl4dv4e.v . . . . . . . . . . . . . . . . . . . . 21 𝑉 = (Vtx‘𝐺)
60591wlkp 40843 . . . . . . . . . . . . . . . . . . . 20 (𝐹(1Walks‘𝐺)𝑃𝑃:(0...(#‘𝐹))⟶𝑉)
61 oveq2 6535 . . . . . . . . . . . . . . . . . . . . . 22 ((#‘𝐹) = 4 → (0...(#‘𝐹)) = (0...4))
6261feq2d 5930 . . . . . . . . . . . . . . . . . . . . 21 ((#‘𝐹) = 4 → (𝑃:(0...(#‘𝐹))⟶𝑉𝑃:(0...4)⟶𝑉))
6362biimpcd 237 . . . . . . . . . . . . . . . . . . . 20 (𝑃:(0...(#‘𝐹))⟶𝑉 → ((#‘𝐹) = 4 → 𝑃:(0...4)⟶𝑉))
642, 60, 633syl 18 . . . . . . . . . . . . . . . . . . 19 (𝐹(PathS‘𝐺)𝑃 → ((#‘𝐹) = 4 → 𝑃:(0...4)⟶𝑉))
6564impcom 444 . . . . . . . . . . . . . . . . . 18 (((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) → 𝑃:(0...4)⟶𝑉)
66 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → 4 ∈ ℕ0)
67 0nn0 11157 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ ℕ0
6867a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → 0 ∈ ℕ0)
69 4pos 10966 . . . . . . . . . . . . . . . . . . . . . . . 24 0 < 4
7069a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → 0 < 4)
7166, 68, 703jca 1234 . . . . . . . . . . . . . . . . . . . . . 22 (4 ∈ ℕ0 → (4 ∈ ℕ0 ∧ 0 ∈ ℕ0 ∧ 0 < 4))
72 fvffz0 12284 . . . . . . . . . . . . . . . . . . . . . 22 (((4 ∈ ℕ0 ∧ 0 ∈ ℕ0 ∧ 0 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉)
7371, 72sylan 486 . . . . . . . . . . . . . . . . . . . . 21 ((4 ∈ ℕ0𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉)
7473ad2antlr 758 . . . . . . . . . . . . . . . . . . . 20 (((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘0) ∈ 𝑉)
75 1nn0 11158 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ ℕ0
7675a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → 1 ∈ ℕ0)
77 1lt4 11049 . . . . . . . . . . . . . . . . . . . . . . . 24 1 < 4
7877a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → 1 < 4)
7966, 76, 783jca 1234 . . . . . . . . . . . . . . . . . . . . . 22 (4 ∈ ℕ0 → (4 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 4))
80 fvffz0 12284 . . . . . . . . . . . . . . . . . . . . . 22 (((4 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
8179, 80sylan 486 . . . . . . . . . . . . . . . . . . . . 21 ((4 ∈ ℕ0𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
8281ad2antlr 758 . . . . . . . . . . . . . . . . . . . 20 (((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘1) ∈ 𝑉)
83 2nn0 11159 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℕ0
8483a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (4 ∈ ℕ0 → 2 ∈ ℕ0)
85 2lt4 11048 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 < 4
8685a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (4 ∈ ℕ0 → 2 < 4)
8766, 84, 863jca 1234 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → (4 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 4))
88 fvffz0 12284 . . . . . . . . . . . . . . . . . . . . . . 23 (((4 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
8987, 88sylan 486 . . . . . . . . . . . . . . . . . . . . . 22 ((4 ∈ ℕ0𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
9089ad2antlr 758 . . . . . . . . . . . . . . . . . . . . 21 (((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘2) ∈ 𝑉)
91 3nn0 11160 . . . . . . . . . . . . . . . . . . . . . . . . 25 3 ∈ ℕ0
9291a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (4 ∈ ℕ0 → 3 ∈ ℕ0)
93 3lt4 11047 . . . . . . . . . . . . . . . . . . . . . . . . 25 3 < 4
9493a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (4 ∈ ℕ0 → 3 < 4)
9566, 92, 943jca 1234 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → (4 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 3 < 4))
96 fvffz0 12284 . . . . . . . . . . . . . . . . . . . . . . 23 (((4 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 3 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉)
9795, 96sylan 486 . . . . . . . . . . . . . . . . . . . . . 22 ((4 ∈ ℕ0𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉)
9897ad2antlr 758 . . . . . . . . . . . . . . . . . . . . 21 (((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘3) ∈ 𝑉)
99 simpr 475 . . . . . . . . . . . . . . . . . . . . 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 787 . . . . . . . . . . . . . . . . . . . . . . 23 ((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) → 𝐹(PathS‘𝐺)𝑃)
101 breq2 4581 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((#‘𝐹) = 4 → (1 < (#‘𝐹) ↔ 1 < 4))
10277, 101mpbiri 246 . . . . . . . . . . . . . . . . . . . . . . . 24 ((#‘𝐹) = 4 → 1 < (#‘𝐹))
103102ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . 23 ((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) → 1 < (#‘𝐹))
104 simpll 785 . . . . . . . . . . . . . . . . . . . . . . 23 ((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) → (#‘𝐹) = 4)
1058ad2antrr 757 . . . . . . . . . . . . . . . . . . . . . . 23 ((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) → (0..^(#‘𝐹)) = (0..^4))
106 4nn 11037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 4 ∈ ℕ
107 lbfzo0 12333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0 ∈ (0..^4) ↔ 4 ∈ ℕ)
108106, 107mpbir 219 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 0 ∈ (0..^4)
109 eleq2 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((0..^(#‘𝐹)) = (0..^4) → (0 ∈ (0..^(#‘𝐹)) ↔ 0 ∈ (0..^4)))
110108, 109mpbiri 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0..^(#‘𝐹)) = (0..^4) → 0 ∈ (0..^(#‘𝐹)))
111110adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → 0 ∈ (0..^(#‘𝐹)))
112 pthdadjvtx 40958 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 0 ∈ (0..^(#‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
113111, 112syl3an3 1352 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
114 1e0p1 11387 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 = (0 + 1)
115114fveq2i 6091 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃‘1) = (𝑃‘(0 + 1))
116115neeq2i 2846 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 + 1)))
117113, 116sylibr 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘1))
118 simp1 1053 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → 𝐹(PathS‘𝐺)𝑃)
119 elfzo0 12334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (2 ∈ (0..^4) ↔ (2 ∈ ℕ0 ∧ 4 ∈ ℕ ∧ 2 < 4))
12083, 106, 85, 119mpbir3an 1236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ∈ (0..^4)
121 2ne0 10963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ≠ 0
122 fzo1fzo0n0 12344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (2 ∈ (1..^4) ↔ (2 ∈ (0..^4) ∧ 2 ≠ 0))
123120, 121, 122mpbir2an 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2 ∈ (1..^4)
124 oveq2 6535 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((#‘𝐹) = 4 → (1..^(#‘𝐹)) = (1..^4))
125123, 124syl5eleqr 2694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐹) = 4 → 2 ∈ (1..^(#‘𝐹)))
126 0elfz 12263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (4 ∈ ℕ0 → 0 ∈ (0...4))
12757, 126ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 0 ∈ (0...4)
128127, 61syl5eleqr 2694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐹) = 4 → 0 ∈ (0...(#‘𝐹)))
129121a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐹) = 4 → 2 ≠ 0)
130125, 128, 1293jca 1234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝐹) = 4 → (2 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 2 ≠ 0))
131130adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → (2 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 2 ≠ 0))
1321313ad2ant3 1076 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (2 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 2 ≠ 0))
133 pthdivtx 40957 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(PathS‘𝐺)𝑃 ∧ (2 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 2 ≠ 0)) → (𝑃‘2) ≠ (𝑃‘0))
134118, 132, 133syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘0))
135134necomd 2836 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘2))
136 elfzo0 12334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (3 ∈ (0..^4) ↔ (3 ∈ ℕ0 ∧ 4 ∈ ℕ ∧ 3 < 4))
13791, 106, 93, 136mpbir3an 1236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3 ∈ (0..^4)
138 3ne0 10965 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3 ≠ 0
139 fzo1fzo0n0 12344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (3 ∈ (1..^4) ↔ (3 ∈ (0..^4) ∧ 3 ≠ 0))
140137, 138, 139mpbir2an 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3 ∈ (1..^4)
141140, 124syl5eleqr 2694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐹) = 4 → 3 ∈ (1..^(#‘𝐹)))
142138a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐹) = 4 → 3 ≠ 0)
143141, 128, 1423jca 1234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝐹) = 4 → (3 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 3 ≠ 0))
144143adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → (3 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 3 ≠ 0))
1451443ad2ant3 1076 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (3 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 3 ≠ 0))
146 pthdivtx 40957 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(PathS‘𝐺)𝑃 ∧ (3 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 3 ≠ 0)) → (𝑃‘3) ≠ (𝑃‘0))
147118, 145, 146syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘3) ≠ (𝑃‘0))
148147necomd 2836 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘3))
149117, 135, 1483jca 1234 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)))
150 elfzo0 12334 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 ∈ (0..^4) ↔ (1 ∈ ℕ0 ∧ 4 ∈ ℕ ∧ 1 < 4))
15175, 106, 77, 150mpbir3an 1236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ (0..^4)
152 eleq2 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((0..^(#‘𝐹)) = (0..^4) → (1 ∈ (0..^(#‘𝐹)) ↔ 1 ∈ (0..^4)))
153151, 152mpbiri 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0..^(#‘𝐹)) = (0..^4) → 1 ∈ (0..^(#‘𝐹)))
154153adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → 1 ∈ (0..^(#‘𝐹)))
155 pthdadjvtx 40958 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 1 ∈ (0..^(#‘𝐹))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
156154, 155syl3an3 1352 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
157 df-2 10929 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2 = (1 + 1)
158157fveq2i 6091 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃‘2) = (𝑃‘(1 + 1))
159158neeq2i 2846 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 + 1)))
160156, 159sylibr 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘2))
161 ax-1ne0 9862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 ≠ 0
162 fzo1fzo0n0 12344 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (1 ∈ (1..^4) ↔ (1 ∈ (0..^4) ∧ 1 ≠ 0))
163151, 161, 162mpbir2an 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1 ∈ (1..^4)
164163, 124syl5eleqr 2694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝐹) = 4 → 1 ∈ (1..^(#‘𝐹)))
165 3re 10944 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3 ∈ ℝ
166 4re 10947 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 4 ∈ ℝ
167165, 166, 93ltleii 10012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3 ≤ 4
168 elfz2nn0 12258 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (3 ∈ (0...4) ↔ (3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ∧ 3 ≤ 4))
16991, 57, 167, 168mpbir3an 1236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3 ∈ (0...4)
170169, 61syl5eleqr 2694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝐹) = 4 → 3 ∈ (0...(#‘𝐹)))
171 1re 9896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 ∈ ℝ
172 1lt3 11046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 < 3
173171, 172ltneii 10002 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1 ≠ 3
174173a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝐹) = 4 → 1 ≠ 3)
175164, 170, 1743jca 1234 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((#‘𝐹) = 4 → (1 ∈ (1..^(#‘𝐹)) ∧ 3 ∈ (0...(#‘𝐹)) ∧ 1 ≠ 3))
176175adantr 479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → (1 ∈ (1..^(#‘𝐹)) ∧ 3 ∈ (0...(#‘𝐹)) ∧ 1 ≠ 3))
1771763ad2ant3 1076 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (1 ∈ (1..^(#‘𝐹)) ∧ 3 ∈ (0...(#‘𝐹)) ∧ 1 ≠ 3))
178 pthdivtx 40957 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(PathS‘𝐺)𝑃 ∧ (1 ∈ (1..^(#‘𝐹)) ∧ 3 ∈ (0...(#‘𝐹)) ∧ 1 ≠ 3)) → (𝑃‘1) ≠ (𝑃‘3))
179118, 177, 178syl2anc 690 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘3))
180 eleq2 2676 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((0..^(#‘𝐹)) = (0..^4) → (2 ∈ (0..^(#‘𝐹)) ↔ 2 ∈ (0..^4)))
181120, 180mpbiri 246 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0..^(#‘𝐹)) = (0..^4) → 2 ∈ (0..^(#‘𝐹)))
182181adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → 2 ∈ (0..^(#‘𝐹)))
183 pthdadjvtx 40958 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 2 ∈ (0..^(#‘𝐹))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
184182, 183syl3an3 1352 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
185 df-3 10930 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 3 = (2 + 1)
186185fveq2i 6091 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃‘3) = (𝑃‘(2 + 1))
187186neeq2i 2846 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))
188184, 187sylibr 222 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘3))
189160, 179, 1883jca 1234 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3)))
190149, 189jca 552 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐹(PathS‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
191100, 103, 104, 105, 190syl112anc 1321 . . . . . . . . . . . . . . . . . . . . . 22 ((((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
192191adantr 479 . . . . . . . . . . . . . . . . . . . . 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 4212 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)})
194193eleq1d 2671 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
195194anbi2d 735 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸)))
196 preq1 4211 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = (𝑃‘2) → {𝑐, 𝑑} = {(𝑃‘2), 𝑑})
197196eleq1d 2671 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑃‘2) → ({𝑐, 𝑑} ∈ 𝐸 ↔ {(𝑃‘2), 𝑑} ∈ 𝐸))
198197anbi1d 736 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑃‘2) → (({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))
199195, 198anbi12d 742 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = (𝑃‘2) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
200 neeq2 2844 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑃‘2) → ((𝑃‘0) ≠ 𝑐 ↔ (𝑃‘0) ≠ (𝑃‘2)))
2012003anbi2d 1395 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑)))
202 neeq2 2844 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2)))
203 neeq1 2843 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑃‘2) → (𝑐𝑑 ↔ (𝑃‘2) ≠ 𝑑))
204202, 2033anbi13d 1392 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑃‘2) → (((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑) ↔ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑)))
205201, 204anbi12d 742 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = (𝑃‘2) → ((((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑))))
206199, 205anbi12d 742 . . . . . . . . . . . . . . . . . . . . . 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 4212 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = (𝑃‘3) → {(𝑃‘2), 𝑑} = {(𝑃‘2), (𝑃‘3)})
208207eleq1d 2671 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑃‘3) → ({(𝑃‘2), 𝑑} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
209 preq1 4211 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = (𝑃‘3) → {𝑑, (𝑃‘0)} = {(𝑃‘3), (𝑃‘0)})
210209eleq1d 2671 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑃‘3) → ({𝑑, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
211208, 210anbi12d 742 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 = (𝑃‘3) → (({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
212211anbi2d 735 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = (𝑃‘3) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
213 neeq2 2844 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑃‘3) → ((𝑃‘0) ≠ 𝑑 ↔ (𝑃‘0) ≠ (𝑃‘3)))
2142133anbi3d 1396 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 = (𝑃‘3) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3))))
215 neeq2 2844 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑃‘3) → ((𝑃‘1) ≠ 𝑑 ↔ (𝑃‘1) ≠ (𝑃‘3)))
216 neeq2 2844 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑃‘3) → ((𝑃‘2) ≠ 𝑑 ↔ (𝑃‘2) ≠ (𝑃‘3)))
217215, 2163anbi23d 1393 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 = (𝑃‘3) → (((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑) ↔ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
218214, 217anbi12d 742 . . . . . . . . . . . . . . . . . . . . . . 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 742 . . . . . . . . . . . . . . . . . . . . . 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 3294 . . . . . . . . . . . . . . . . . . . . 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 1321 . . . . . . . . . . . . . . . . . . . 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 1234 . . . . . . . . . . . . . . . . . . 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 627 . . . . . . . . . . . . . . . . . 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 710 . . . . . . . . . . . . . . . . 17 (((#‘𝐹) = 4 ∧ 𝐹(PathS‘𝐺)𝑃) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)) → ((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑))))))
225224adantr 479 . . . . . . . . . . . . . . . 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 228 . . . . . . . . . . . . . . 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 627 . . . . . . . . . . . . . 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 614 . . . . . . . . . . . . 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 4211 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏})
230229eleq1d 2671 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸))
231230anbi1d 736 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
232 preq2 4212 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑃‘0) → {𝑑, 𝑎} = {𝑑, (𝑃‘0)})
233232eleq1d 2671 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → ({𝑑, 𝑎} ∈ 𝐸 ↔ {𝑑, (𝑃‘0)} ∈ 𝐸))
234233anbi2d 735 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → (({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸) ↔ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))
235231, 234anbi12d 742 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
236 neeq1 2843 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → (𝑎𝑏 ↔ (𝑃‘0) ≠ 𝑏))
237 neeq1 2843 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → (𝑎𝑐 ↔ (𝑃‘0) ≠ 𝑐))
238 neeq1 2843 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → (𝑎𝑑 ↔ (𝑃‘0) ≠ 𝑑))
239236, 237, 2383anbi123d 1390 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → ((𝑎𝑏𝑎𝑐𝑎𝑑) ↔ ((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑)))
240239anbi1d 736 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑃‘0) → (((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)) ↔ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))
241235, 240anbi12d 742 . . . . . . . . . . . . . . 15 (𝑎 = (𝑃‘0) → (((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))) ↔ ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))
2422412rexbidv 3038 . . . . . . . . . . . . . 14 (𝑎 = (𝑃‘0) → (∃𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))) ↔ ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))
243 preq2 4212 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)})
244243eleq1d 2671 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
245 preq1 4211 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐})
246245eleq1d 2671 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸))
247244, 246anbi12d 742 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸)))
248247anbi1d 736 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
249 neeq2 2844 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1)))
2502493anbi1d 1394 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑)))
251 neeq1 2843 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → (𝑏𝑐 ↔ (𝑃‘1) ≠ 𝑐))
252 neeq1 2843 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → (𝑏𝑑 ↔ (𝑃‘1) ≠ 𝑑))
253251, 2523anbi12d 1391 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → ((𝑏𝑐𝑏𝑑𝑐𝑑) ↔ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑)))
254250, 253anbi12d 742 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑃‘1) → ((((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑))))
255248, 254anbi12d 742 . . . . . . . . . . . . . . 15 (𝑏 = (𝑃‘1) → (((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))) ↔ ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑)))))
2562552rexbidv 3038 . . . . . . . . . . . . . 14 (𝑏 = (𝑃‘1) → (∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))) ↔ ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑)))))
257242, 256rspc2ev 3294 . . . . . . . . . . . . 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 228 . . . . . . . . . . 11 ((#‘𝐹) = 4 → (((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))
260259expd 450 . . . . . . . . . 10 ((#‘𝐹) = 4 → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))
261260com13 85 . . . . . . . . 9 (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))
2624, 261syl 17 . . . . . . . 8 ((𝐺 ∈ UPGraph ∧ 𝐹(1Walks‘𝐺)𝑃) → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))
263262expcom 449 . . . . . . 7 (𝐹(1Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))))
264263com23 83 . . . . . 6 (𝐹(1Walks‘𝐺)𝑃 → ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))))
265264expd 450 . . . . 5 (𝐹(1Walks‘𝐺)𝑃 → (𝐹(PathS‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))))
2662, 265mpcom 37 . . . 4 (𝐹(PathS‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))))
267266imp 443 . . 3 ((𝐹(PathS‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))
2681, 267syl 17 . 2 (𝐹(CycleS‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))
2692683imp21 1268 1 ((𝐺 ∈ UPGraph ∧ 𝐹(CycleS‘𝐺)𝑃 ∧ (#‘𝐹) = 4) → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wne 2779  wral 2895  wrex 2896  cun 3537  {cpr 4126   class class class wbr 4577  wf 5786  cfv 5790  (class class class)co 6527  0cc0 9793  1c1 9794   + caddc 9796   < clt 9931  cle 9932  cn 10870  2c2 10920  3c3 10921  4c4 10922  0cn0 11142  ...cfz 12155  ..^cfzo 12292  #chash 12937  Vtxcvtx 40251   UPGraph cupgr 40328  Edgcedga 40373  1Walksc1wlks 40818  PathScpths 40941  CycleSccycls 41013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-rep 4693  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6825  ax-cnex 9849  ax-resscn 9850  ax-1cn 9851  ax-icn 9852  ax-addcl 9853  ax-addrcl 9854  ax-mulcl 9855  ax-mulrcl 9856  ax-mulcom 9857  ax-addass 9858  ax-mulass 9859  ax-distr 9860  ax-i2m1 9861  ax-1ne0 9862  ax-1rid 9863  ax-rnegex 9864  ax-rrecex 9865  ax-cnre 9866  ax-pre-lttri 9867  ax-pre-lttrn 9868  ax-pre-ltadd 9869  ax-pre-mulgt0 9870
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-ifp 1006  df-3or 1031  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ne 2781  df-nel 2782  df-ral 2900  df-rex 2901  df-reu 2902  df-rmo 2903  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-pss 3555  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-tp 4129  df-op 4131  df-uni 4367  df-int 4405  df-iun 4451  df-br 4578  df-opab 4638  df-mpt 4639  df-tr 4675  df-eprel 4939  df-id 4943  df-po 4949  df-so 4950  df-fr 4987  df-we 4989  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041  df-pred 5583  df-ord 5629  df-on 5630  df-lim 5631  df-suc 5632  df-iota 5754  df-fun 5792  df-fn 5793  df-f 5794  df-f1 5795  df-fo 5796  df-f1o 5797  df-fv 5798  df-riota 6489  df-ov 6530  df-oprab 6531  df-mpt2 6532  df-om 6936  df-1st 7037  df-2nd 7038  df-wrecs 7272  df-recs 7333  df-rdg 7371  df-1o 7425  df-2o 7426  df-oadd 7429  df-er 7607  df-map 7724  df-pm 7725  df-en 7820  df-dom 7821  df-sdom 7822  df-fin 7823  df-card 8626  df-cda 8851  df-pnf 9933  df-mnf 9934  df-xr 9935  df-ltxr 9936  df-le 9937  df-sub 10120  df-neg 10121  df-nn 10871  df-2 10929  df-3 10930  df-4 10931  df-n0 11143  df-z 11214  df-uz 11523  df-fz 12156  df-fzo 12293  df-hash 12938  df-word 13103  df-uhgr 40302  df-upgr 40330  df-edga 40374  df-1wlks 40822  df-wlks 40823  df-trls 40923  df-pths 40945  df-cycls 41015
This theorem is referenced by:  n4cyclfrgr  41483
  Copyright terms: Public domain W3C validator