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

Theorem upgr4cycl4dv4e 27163
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 26744 . . 3 (𝐹(Cycles‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))))
2 pthiswlk 26679 . . . . 5 (𝐹(Paths‘𝐺)𝑃𝐹(Walks‘𝐺)𝑃)
3 upgr4cycl4dv4e.e . . . . . . . . . 10 𝐸 = (Edg‘𝐺)
43upgrwlkvtxedg 26597 . . . . . . . . 9 ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸)
5 fveq2 6229 . . . . . . . . . . . . . . 15 ((#‘𝐹) = 4 → (𝑃‘(#‘𝐹)) = (𝑃‘4))
65eqeq2d 2661 . . . . . . . . . . . . . 14 ((#‘𝐹) = 4 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) ↔ (𝑃‘0) = (𝑃‘4)))
76anbi2d 740 . . . . . . . . . . . . 13 ((#‘𝐹) = 4 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ↔ (𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4))))
8 oveq2 6698 . . . . . . . . . . . . . . . 16 ((#‘𝐹) = 4 → (0..^(#‘𝐹)) = (0..^4))
9 fzo0to42pr 12595 . . . . . . . . . . . . . . . 16 (0..^4) = ({0, 1} ∪ {2, 3})
108, 9syl6eq 2701 . . . . . . . . . . . . . . 15 ((#‘𝐹) = 4 → (0..^(#‘𝐹)) = ({0, 1} ∪ {2, 3}))
1110raleqdv 3174 . . . . . . . . . . . . . 14 ((#‘𝐹) = 4 → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
12 ralunb 3827 . . . . . . . . . . . . . . 15 (∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (∀𝑘 ∈ {0, 1} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ∧ ∀𝑘 ∈ {2, 3} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸))
13 c0ex 10072 . . . . . . . . . . . . . . . . 17 0 ∈ V
14 1ex 10073 . . . . . . . . . . . . . . . . 17 1 ∈ V
15 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 0 → (𝑃𝑘) = (𝑃‘0))
16 oveq1 6697 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 0 → (𝑘 + 1) = (0 + 1))
17 0p1e1 11170 . . . . . . . . . . . . . . . . . . . . 21 (0 + 1) = 1
1816, 17syl6eq 2701 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 0 → (𝑘 + 1) = 1)
1918fveq2d 6233 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 0 → (𝑃‘(𝑘 + 1)) = (𝑃‘1))
2015, 19preq12d 4308 . . . . . . . . . . . . . . . . . 18 (𝑘 = 0 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘0), (𝑃‘1)})
2120eleq1d 2715 . . . . . . . . . . . . . . . . 17 (𝑘 = 0 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
22 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 1 → (𝑃𝑘) = (𝑃‘1))
23 oveq1 6697 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 1 → (𝑘 + 1) = (1 + 1))
24 1p1e2 11172 . . . . . . . . . . . . . . . . . . . . 21 (1 + 1) = 2
2523, 24syl6eq 2701 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 1 → (𝑘 + 1) = 2)
2625fveq2d 6233 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 1 → (𝑃‘(𝑘 + 1)) = (𝑃‘2))
2722, 26preq12d 4308 . . . . . . . . . . . . . . . . . 18 (𝑘 = 1 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘1), (𝑃‘2)})
2827eleq1d 2715 . . . . . . . . . . . . . . . . 17 (𝑘 = 1 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
2913, 14, 21, 28ralpr 4270 . . . . . . . . . . . . . . . 16 (∀𝑘 ∈ {0, 1} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
30 2ex 11130 . . . . . . . . . . . . . . . . 17 2 ∈ V
31 3ex 11134 . . . . . . . . . . . . . . . . 17 3 ∈ V
32 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 2 → (𝑃𝑘) = (𝑃‘2))
33 oveq1 6697 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 2 → (𝑘 + 1) = (2 + 1))
34 2p1e3 11189 . . . . . . . . . . . . . . . . . . . . 21 (2 + 1) = 3
3533, 34syl6eq 2701 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 2 → (𝑘 + 1) = 3)
3635fveq2d 6233 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 2 → (𝑃‘(𝑘 + 1)) = (𝑃‘3))
3732, 36preq12d 4308 . . . . . . . . . . . . . . . . . 18 (𝑘 = 2 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘2), (𝑃‘3)})
3837eleq1d 2715 . . . . . . . . . . . . . . . . 17 (𝑘 = 2 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
39 fveq2 6229 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 3 → (𝑃𝑘) = (𝑃‘3))
40 oveq1 6697 . . . . . . . . . . . . . . . . . . . . 21 (𝑘 = 3 → (𝑘 + 1) = (3 + 1))
41 3p1e4 11191 . . . . . . . . . . . . . . . . . . . . 21 (3 + 1) = 4
4240, 41syl6eq 2701 . . . . . . . . . . . . . . . . . . . 20 (𝑘 = 3 → (𝑘 + 1) = 4)
4342fveq2d 6233 . . . . . . . . . . . . . . . . . . 19 (𝑘 = 3 → (𝑃‘(𝑘 + 1)) = (𝑃‘4))
4439, 43preq12d 4308 . . . . . . . . . . . . . . . . . 18 (𝑘 = 3 → {(𝑃𝑘), (𝑃‘(𝑘 + 1))} = {(𝑃‘3), (𝑃‘4)})
4544eleq1d 2715 . . . . . . . . . . . . . . . . 17 (𝑘 = 3 → ({(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))
4630, 31, 38, 45ralpr 4270 . . . . . . . . . . . . . . . 16 (∀𝑘 ∈ {2, 3} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))
4729, 46anbi12i 733 . . . . . . . . . . . . . . 15 ((∀𝑘 ∈ {0, 1} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ∧ ∀𝑘 ∈ {2, 3} {(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))
4812, 47bitri 264 . . . . . . . . . . . . . 14 (∀𝑘 ∈ ({0, 1} ∪ {2, 3}){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))
4911, 48syl6bb 276 . . . . . . . . . . . . 13 ((#‘𝐹) = 4 → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))))
507, 49anbi12d 747 . . . . . . . . . . . 12 ((#‘𝐹) = 4 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) ↔ ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸)))))
51 preq2 4301 . . . . . . . . . . . . . . . . . . . . 21 ((𝑃‘4) = (𝑃‘0) → {(𝑃‘3), (𝑃‘4)} = {(𝑃‘3), (𝑃‘0)})
5251eleq1d 2715 . . . . . . . . . . . . . . . . . . . 20 ((𝑃‘4) = (𝑃‘0) → ({(𝑃‘3), (𝑃‘4)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
5352eqcoms 2659 . . . . . . . . . . . . . . . . . . 19 ((𝑃‘0) = (𝑃‘4) → ({(𝑃‘3), (𝑃‘4)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
5453anbi2d 740 . . . . . . . . . . . . . . . . . 18 ((𝑃‘0) = (𝑃‘4) → (({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸) ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
5554anbi2d 740 . . . . . . . . . . . . . . . . 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 11349 . . . . . . . . . . . . . . . . . . 19 4 ∈ ℕ0
5857a1i 11 . . . . . . . . . . . . . . . . . 18 (((#‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) → 4 ∈ ℕ0)
59 upgr4cycl4dv4e.v . . . . . . . . . . . . . . . . . . . . 21 𝑉 = (Vtx‘𝐺)
6059wlkp 26568 . . . . . . . . . . . . . . . . . . . 20 (𝐹(Walks‘𝐺)𝑃𝑃:(0...(#‘𝐹))⟶𝑉)
61 oveq2 6698 . . . . . . . . . . . . . . . . . . . . . 22 ((#‘𝐹) = 4 → (0...(#‘𝐹)) = (0...4))
6261feq2d 6069 . . . . . . . . . . . . . . . . . . . . 21 ((#‘𝐹) = 4 → (𝑃:(0...(#‘𝐹))⟶𝑉𝑃:(0...4)⟶𝑉))
6362biimpcd 239 . . . . . . . . . . . . . . . . . . . 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 11345 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ ℕ0
6867a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → 0 ∈ ℕ0)
69 4pos 11154 . . . . . . . . . . . . . . . . . . . . . . . 24 0 < 4
7069a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → 0 < 4)
7166, 68, 703jca 1261 . . . . . . . . . . . . . . . . . . . . . 22 (4 ∈ ℕ0 → (4 ∈ ℕ0 ∧ 0 ∈ ℕ0 ∧ 0 < 4))
72 fvffz0 12496 . . . . . . . . . . . . . . . . . . . . . 22 (((4 ∈ ℕ0 ∧ 0 ∈ ℕ0 ∧ 0 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉)
7371, 72sylan 487 . . . . . . . . . . . . . . . . . . . . 21 ((4 ∈ ℕ0𝑃:(0...4)⟶𝑉) → (𝑃‘0) ∈ 𝑉)
7473ad2antlr 763 . . . . . . . . . . . . . . . . . . . 20 (((((#‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘0) ∈ 𝑉)
75 1nn0 11346 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ ℕ0
7675a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → 1 ∈ ℕ0)
77 1lt4 11237 . . . . . . . . . . . . . . . . . . . . . . . 24 1 < 4
7877a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → 1 < 4)
7966, 76, 783jca 1261 . . . . . . . . . . . . . . . . . . . . . 22 (4 ∈ ℕ0 → (4 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 4))
80 fvffz0 12496 . . . . . . . . . . . . . . . . . . . . . 22 (((4 ∈ ℕ0 ∧ 1 ∈ ℕ0 ∧ 1 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
8179, 80sylan 487 . . . . . . . . . . . . . . . . . . . . 21 ((4 ∈ ℕ0𝑃:(0...4)⟶𝑉) → (𝑃‘1) ∈ 𝑉)
8281ad2antlr 763 . . . . . . . . . . . . . . . . . . . 20 (((((#‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘1) ∈ 𝑉)
83 2nn0 11347 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 ∈ ℕ0
8483a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (4 ∈ ℕ0 → 2 ∈ ℕ0)
85 2lt4 11236 . . . . . . . . . . . . . . . . . . . . . . . . 25 2 < 4
8685a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (4 ∈ ℕ0 → 2 < 4)
8766, 84, 863jca 1261 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → (4 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 4))
88 fvffz0 12496 . . . . . . . . . . . . . . . . . . . . . . 23 (((4 ∈ ℕ0 ∧ 2 ∈ ℕ0 ∧ 2 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
8987, 88sylan 487 . . . . . . . . . . . . . . . . . . . . . 22 ((4 ∈ ℕ0𝑃:(0...4)⟶𝑉) → (𝑃‘2) ∈ 𝑉)
9089ad2antlr 763 . . . . . . . . . . . . . . . . . . . . 21 (((((#‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))) → (𝑃‘2) ∈ 𝑉)
91 3nn0 11348 . . . . . . . . . . . . . . . . . . . . . . . . 25 3 ∈ ℕ0
9291a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (4 ∈ ℕ0 → 3 ∈ ℕ0)
93 3lt4 11235 . . . . . . . . . . . . . . . . . . . . . . . . 25 3 < 4
9493a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24 (4 ∈ ℕ0 → 3 < 4)
9566, 92, 943jca 1261 . . . . . . . . . . . . . . . . . . . . . . 23 (4 ∈ ℕ0 → (4 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 3 < 4))
96 fvffz0 12496 . . . . . . . . . . . . . . . . . . . . . . 23 (((4 ∈ ℕ0 ∧ 3 ∈ ℕ0 ∧ 3 < 4) ∧ 𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉)
9795, 96sylan 487 . . . . . . . . . . . . . . . . . . . . . 22 ((4 ∈ ℕ0𝑃:(0...4)⟶𝑉) → (𝑃‘3) ∈ 𝑉)
9897ad2antlr 763 . . . . . . . . . . . . . . . . . . . . 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 807 . . . . . . . . . . . . . . . . . . . . . . 23 ((((#‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) → 𝐹(Paths‘𝐺)𝑃)
101 breq2 4689 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((#‘𝐹) = 4 → (1 < (#‘𝐹) ↔ 1 < 4))
10277, 101mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . 24 ((#‘𝐹) = 4 → 1 < (#‘𝐹))
103102ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . 23 ((((#‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) → 1 < (#‘𝐹))
104 simpll 805 . . . . . . . . . . . . . . . . . . . . . . 23 ((((#‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) → (#‘𝐹) = 4)
1058ad2antrr 762 . . . . . . . . . . . . . . . . . . . . . . 23 ((((#‘𝐹) = 4 ∧ 𝐹(Paths‘𝐺)𝑃) ∧ (4 ∈ ℕ0𝑃:(0...4)⟶𝑉)) → (0..^(#‘𝐹)) = (0..^4))
106 4nn 11225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 4 ∈ ℕ
107 lbfzo0 12547 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (0 ∈ (0..^4) ↔ 4 ∈ ℕ)
108106, 107mpbir 221 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 0 ∈ (0..^4)
109 eleq2 2719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((0..^(#‘𝐹)) = (0..^4) → (0 ∈ (0..^(#‘𝐹)) ↔ 0 ∈ (0..^4)))
110108, 109mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0..^(#‘𝐹)) = (0..^4) → 0 ∈ (0..^(#‘𝐹)))
111110adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → 0 ∈ (0..^(#‘𝐹)))
112 pthdadjvtx 26682 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 0 ∈ (0..^(#‘𝐹))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
113111, 112syl3an3 1401 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘(0 + 1)))
114 1e0p1 11590 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 1 = (0 + 1)
115114fveq2i 6232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃‘1) = (𝑃‘(0 + 1))
116115neeq2i 2888 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃‘0) ≠ (𝑃‘1) ↔ (𝑃‘0) ≠ (𝑃‘(0 + 1)))
117113, 116sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘1))
118 simp1 1081 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → 𝐹(Paths‘𝐺)𝑃)
119 elfzo0 12548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (2 ∈ (0..^4) ↔ (2 ∈ ℕ0 ∧ 4 ∈ ℕ ∧ 2 < 4))
12083, 106, 85, 119mpbir3an 1263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ∈ (0..^4)
121 2ne0 11151 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2 ≠ 0
122 fzo1fzo0n0 12558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (2 ∈ (1..^4) ↔ (2 ∈ (0..^4) ∧ 2 ≠ 0))
123120, 121, 122mpbir2an 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 2 ∈ (1..^4)
124 oveq2 6698 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((#‘𝐹) = 4 → (1..^(#‘𝐹)) = (1..^4))
125123, 124syl5eleqr 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐹) = 4 → 2 ∈ (1..^(#‘𝐹)))
126 0elfz 12475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (4 ∈ ℕ0 → 0 ∈ (0...4))
12757, 126ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 0 ∈ (0...4)
128127, 61syl5eleqr 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐹) = 4 → 0 ∈ (0...(#‘𝐹)))
129121a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐹) = 4 → 2 ≠ 0)
130125, 128, 1293jca 1261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝐹) = 4 → (2 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 2 ≠ 0))
131130adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → (2 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 2 ≠ 0))
1321313ad2ant3 1104 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (2 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 2 ≠ 0))
133 pthdivtx 26681 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(Paths‘𝐺)𝑃 ∧ (2 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 2 ≠ 0)) → (𝑃‘2) ≠ (𝑃‘0))
134118, 132, 133syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘0))
135134necomd 2878 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘2))
136 elfzo0 12548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (3 ∈ (0..^4) ↔ (3 ∈ ℕ0 ∧ 4 ∈ ℕ ∧ 3 < 4))
13791, 106, 93, 136mpbir3an 1263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3 ∈ (0..^4)
138 3ne0 11153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3 ≠ 0
139 fzo1fzo0n0 12558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (3 ∈ (1..^4) ↔ (3 ∈ (0..^4) ∧ 3 ≠ 0))
140137, 138, 139mpbir2an 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3 ∈ (1..^4)
141140, 124syl5eleqr 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐹) = 4 → 3 ∈ (1..^(#‘𝐹)))
142138a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((#‘𝐹) = 4 → 3 ≠ 0)
143141, 128, 1423jca 1261 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝐹) = 4 → (3 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 3 ≠ 0))
144143adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → (3 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 3 ≠ 0))
1451443ad2ant3 1104 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (3 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 3 ≠ 0))
146 pthdivtx 26681 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(Paths‘𝐺)𝑃 ∧ (3 ∈ (1..^(#‘𝐹)) ∧ 0 ∈ (0...(#‘𝐹)) ∧ 3 ≠ 0)) → (𝑃‘3) ≠ (𝑃‘0))
147118, 145, 146syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘3) ≠ (𝑃‘0))
148147necomd 2878 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘0) ≠ (𝑃‘3))
149117, 135, 1483jca 1261 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3)))
150 elfzo0 12548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (1 ∈ (0..^4) ↔ (1 ∈ ℕ0 ∧ 4 ∈ ℕ ∧ 1 < 4))
15175, 106, 77, 150mpbir3an 1263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 1 ∈ (0..^4)
152 eleq2 2719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((0..^(#‘𝐹)) = (0..^4) → (1 ∈ (0..^(#‘𝐹)) ↔ 1 ∈ (0..^4)))
153151, 152mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0..^(#‘𝐹)) = (0..^4) → 1 ∈ (0..^(#‘𝐹)))
154153adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → 1 ∈ (0..^(#‘𝐹)))
155 pthdadjvtx 26682 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 1 ∈ (0..^(#‘𝐹))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
156154, 155syl3an3 1401 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘(1 + 1)))
157 df-2 11117 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 2 = (1 + 1)
158157fveq2i 6232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃‘2) = (𝑃‘(1 + 1))
159158neeq2i 2888 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃‘1) ≠ (𝑃‘2) ↔ (𝑃‘1) ≠ (𝑃‘(1 + 1)))
160156, 159sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘2))
161 ax-1ne0 10043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 ≠ 0
162 fzo1fzo0n0 12558 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (1 ∈ (1..^4) ↔ (1 ∈ (0..^4) ∧ 1 ≠ 0))
163151, 161, 162mpbir2an 975 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1 ∈ (1..^4)
164163, 124syl5eleqr 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝐹) = 4 → 1 ∈ (1..^(#‘𝐹)))
165 3re 11132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 3 ∈ ℝ
166 4re 11135 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 4 ∈ ℝ
167165, 166, 93ltleii 10198 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3 ≤ 4
168 elfz2nn0 12469 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (3 ∈ (0...4) ↔ (3 ∈ ℕ0 ∧ 4 ∈ ℕ0 ∧ 3 ≤ 4))
16991, 57, 167, 168mpbir3an 1263 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3 ∈ (0...4)
170169, 61syl5eleqr 2737 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝐹) = 4 → 3 ∈ (0...(#‘𝐹)))
171 1re 10077 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 ∈ ℝ
172 1lt3 11234 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 1 < 3
173171, 172ltneii 10188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 1 ≠ 3
174173a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((#‘𝐹) = 4 → 1 ≠ 3)
175164, 170, 1743jca 1261 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((#‘𝐹) = 4 → (1 ∈ (1..^(#‘𝐹)) ∧ 3 ∈ (0...(#‘𝐹)) ∧ 1 ≠ 3))
176175adantr 480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → (1 ∈ (1..^(#‘𝐹)) ∧ 3 ∈ (0...(#‘𝐹)) ∧ 1 ≠ 3))
1771763ad2ant3 1104 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (1 ∈ (1..^(#‘𝐹)) ∧ 3 ∈ (0...(#‘𝐹)) ∧ 1 ≠ 3))
178 pthdivtx 26681 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(Paths‘𝐺)𝑃 ∧ (1 ∈ (1..^(#‘𝐹)) ∧ 3 ∈ (0...(#‘𝐹)) ∧ 1 ≠ 3)) → (𝑃‘1) ≠ (𝑃‘3))
179118, 177, 178syl2anc 694 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘1) ≠ (𝑃‘3))
180 eleq2 2719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((0..^(#‘𝐹)) = (0..^4) → (2 ∈ (0..^(#‘𝐹)) ↔ 2 ∈ (0..^4)))
181120, 180mpbiri 248 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((0..^(#‘𝐹)) = (0..^4) → 2 ∈ (0..^(#‘𝐹)))
182181adantl 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4)) → 2 ∈ (0..^(#‘𝐹)))
183 pthdadjvtx 26682 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ 2 ∈ (0..^(#‘𝐹))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
184182, 183syl3an3 1401 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘(2 + 1)))
185 df-3 11118 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 3 = (2 + 1)
186185fveq2i 6232 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑃‘3) = (𝑃‘(2 + 1))
187186neeq2i 2888 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑃‘2) ≠ (𝑃‘3) ↔ (𝑃‘2) ≠ (𝑃‘(2 + 1)))
188184, 187sylibr 224 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝐹(Paths‘𝐺)𝑃 ∧ 1 < (#‘𝐹) ∧ ((#‘𝐹) = 4 ∧ (0..^(#‘𝐹)) = (0..^4))) → (𝑃‘2) ≠ (𝑃‘3))
189160, 179, 1883jca 1261 . . . . . . . . . . . . . . . . . . . . . . . 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 1370 . . . . . . . . . . . . . . . . . . . . . 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 4301 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = (𝑃‘2) → {(𝑃‘1), 𝑐} = {(𝑃‘1), (𝑃‘2)})
194193eleq1d 2715 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑃‘2) → ({(𝑃‘1), 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸))
195194anbi2d 740 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑃‘2) → (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸)))
196 preq1 4300 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑐 = (𝑃‘2) → {𝑐, 𝑑} = {(𝑃‘2), 𝑑})
197196eleq1d 2715 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑃‘2) → ({𝑐, 𝑑} ∈ 𝐸 ↔ {(𝑃‘2), 𝑑} ∈ 𝐸))
198197anbi1d 741 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑃‘2) → (({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))
199195, 198anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = (𝑃‘2) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
200 neeq2 2886 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑃‘2) → ((𝑃‘0) ≠ 𝑐 ↔ (𝑃‘0) ≠ (𝑃‘2)))
2012003anbi2d 1444 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑃‘2) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑)))
202 neeq2 2886 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑃‘2) → ((𝑃‘1) ≠ 𝑐 ↔ (𝑃‘1) ≠ (𝑃‘2)))
203 neeq1 2885 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑐 = (𝑃‘2) → (𝑐𝑑 ↔ (𝑃‘2) ≠ 𝑑))
204202, 2033anbi13d 1441 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑐 = (𝑃‘2) → (((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑) ↔ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑)))
205201, 204anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑐 = (𝑃‘2) → ((((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑))))
206199, 205anbi12d 747 . . . . . . . . . . . . . . . . . . . . . 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 4301 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = (𝑃‘3) → {(𝑃‘2), 𝑑} = {(𝑃‘2), (𝑃‘3)})
208207eleq1d 2715 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑃‘3) → ({(𝑃‘2), 𝑑} ∈ 𝐸 ↔ {(𝑃‘2), (𝑃‘3)} ∈ 𝐸))
209 preq1 4300 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑑 = (𝑃‘3) → {𝑑, (𝑃‘0)} = {(𝑃‘3), (𝑃‘0)})
210209eleq1d 2715 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑃‘3) → ({𝑑, (𝑃‘0)} ∈ 𝐸 ↔ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))
211208, 210anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 = (𝑃‘3) → (({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸) ↔ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸)))
212211anbi2d 740 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 = (𝑃‘3) → ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘0)} ∈ 𝐸))))
213 neeq2 2886 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑃‘3) → ((𝑃‘0) ≠ 𝑑 ↔ (𝑃‘0) ≠ (𝑃‘3)))
2142133anbi3d 1445 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 = (𝑃‘3) → (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ (𝑃‘2) ∧ (𝑃‘0) ≠ (𝑃‘3))))
215 neeq2 2886 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑃‘3) → ((𝑃‘1) ≠ 𝑑 ↔ (𝑃‘1) ≠ (𝑃‘3)))
216 neeq2 2886 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑑 = (𝑃‘3) → ((𝑃‘2) ≠ 𝑑 ↔ (𝑃‘2) ≠ (𝑃‘3)))
217215, 2163anbi23d 1442 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑑 = (𝑃‘3) → (((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ 𝑑 ∧ (𝑃‘2) ≠ 𝑑) ↔ ((𝑃‘1) ≠ (𝑃‘2) ∧ (𝑃‘1) ≠ (𝑃‘3) ∧ (𝑃‘2) ≠ (𝑃‘3))))
218214, 217anbi12d 747 . . . . . . . . . . . . . . . . . . . . . . 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 747 . . . . . . . . . . . . . . . . . . . . . 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 3355 . . . . . . . . . . . . . . . . . . . . 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 1370 . . . . . . . . . . . . . . . . . . . 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 1261 . . . . . . . . . . . . . . . . . . 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 629 . . . . . . . . . . . . . . . . . 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 715 . . . . . . . . . . . . . . . . 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 230 . . . . . . . . . . . . . . 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 629 . . . . . . . . . . . . . 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 616 . . . . . . . . . . . . 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 4300 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑃‘0) → {𝑎, 𝑏} = {(𝑃‘0), 𝑏})
230229eleq1d 2715 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → ({𝑎, 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), 𝑏} ∈ 𝐸))
231230anbi1d 741 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → (({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸)))
232 preq2 4301 . . . . . . . . . . . . . . . . . . 19 (𝑎 = (𝑃‘0) → {𝑑, 𝑎} = {𝑑, (𝑃‘0)})
233232eleq1d 2715 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → ({𝑑, 𝑎} ∈ 𝐸 ↔ {𝑑, (𝑃‘0)} ∈ 𝐸))
234233anbi2d 740 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → (({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸) ↔ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)))
235231, 234anbi12d 747 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑃‘0) → ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ↔ (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
236 neeq1 2885 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → (𝑎𝑏 ↔ (𝑃‘0) ≠ 𝑏))
237 neeq1 2885 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → (𝑎𝑐 ↔ (𝑃‘0) ≠ 𝑐))
238 neeq1 2885 . . . . . . . . . . . . . . . . . 18 (𝑎 = (𝑃‘0) → (𝑎𝑑 ↔ (𝑃‘0) ≠ 𝑑))
239236, 237, 2383anbi123d 1439 . . . . . . . . . . . . . . . . 17 (𝑎 = (𝑃‘0) → ((𝑎𝑏𝑎𝑐𝑎𝑑) ↔ ((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑)))
240239anbi1d 741 . . . . . . . . . . . . . . . 16 (𝑎 = (𝑃‘0) → (((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)) ↔ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))
241235, 240anbi12d 747 . . . . . . . . . . . . . . 15 (𝑎 = (𝑃‘0) → (((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))) ↔ ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))
2422412rexbidv 3086 . . . . . . . . . . . . . 14 (𝑎 = (𝑃‘0) → (∃𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))) ↔ ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))
243 preq2 4301 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑃‘1) → {(𝑃‘0), 𝑏} = {(𝑃‘0), (𝑃‘1)})
244243eleq1d 2715 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → ({(𝑃‘0), 𝑏} ∈ 𝐸 ↔ {(𝑃‘0), (𝑃‘1)} ∈ 𝐸))
245 preq1 4300 . . . . . . . . . . . . . . . . . . 19 (𝑏 = (𝑃‘1) → {𝑏, 𝑐} = {(𝑃‘1), 𝑐})
246245eleq1d 2715 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → ({𝑏, 𝑐} ∈ 𝐸 ↔ {(𝑃‘1), 𝑐} ∈ 𝐸))
247244, 246anbi12d 747 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → (({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ↔ ({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸)))
248247anbi1d 741 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑃‘1) → ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ↔ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸))))
249 neeq2 2886 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → ((𝑃‘0) ≠ 𝑏 ↔ (𝑃‘0) ≠ (𝑃‘1)))
2502493anbi1d 1443 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ↔ ((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑)))
251 neeq1 2885 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → (𝑏𝑐 ↔ (𝑃‘1) ≠ 𝑐))
252 neeq1 2885 . . . . . . . . . . . . . . . . . 18 (𝑏 = (𝑃‘1) → (𝑏𝑑 ↔ (𝑃‘1) ≠ 𝑑))
253251, 2523anbi12d 1440 . . . . . . . . . . . . . . . . 17 (𝑏 = (𝑃‘1) → ((𝑏𝑐𝑏𝑑𝑐𝑑) ↔ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑)))
254250, 253anbi12d 747 . . . . . . . . . . . . . . . 16 (𝑏 = (𝑃‘1) → ((((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)) ↔ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑))))
255248, 254anbi12d 747 . . . . . . . . . . . . . . 15 (𝑏 = (𝑃‘1) → (((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))) ↔ ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑)))))
2562552rexbidv 3086 . . . . . . . . . . . . . 14 (𝑏 = (𝑃‘1) → (∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ 𝑏 ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))) ↔ ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑)))))
257242, 256rspc2ev 3355 . . . . . . . . . . . . 13 (((𝑃‘0) ∈ 𝑉 ∧ (𝑃‘1) ∈ 𝑉 ∧ ∃𝑐𝑉𝑑𝑉 ((({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, (𝑃‘0)} ∈ 𝐸)) ∧ (((𝑃‘0) ≠ (𝑃‘1) ∧ (𝑃‘0) ≠ 𝑐 ∧ (𝑃‘0) ≠ 𝑑) ∧ ((𝑃‘1) ≠ 𝑐 ∧ (𝑃‘1) ≠ 𝑑𝑐𝑑)))) → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))
258228, 257syl6 35 . . . . . . . . . . . 12 ((#‘𝐹) = 4 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘4)) ∧ (({(𝑃‘0), (𝑃‘1)} ∈ 𝐸 ∧ {(𝑃‘1), (𝑃‘2)} ∈ 𝐸) ∧ ({(𝑃‘2), (𝑃‘3)} ∈ 𝐸 ∧ {(𝑃‘3), (𝑃‘4)} ∈ 𝐸))) → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))
25950, 258sylbid 230 . . . . . . . . . . 11 ((#‘𝐹) = 4 → (((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) ∧ ∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸) → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))
260259expd 451 . . . . . . . . . 10 ((#‘𝐹) = 4 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))
261260com13 88 . . . . . . . . 9 (∀𝑘 ∈ (0..^(#‘𝐹)){(𝑃𝑘), (𝑃‘(𝑘 + 1))} ∈ 𝐸 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))
2624, 261syl 17 . . . . . . . 8 ((𝐺 ∈ UPGraph ∧ 𝐹(Walks‘𝐺)𝑃) → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))
263262expcom 450 . . . . . . 7 (𝐹(Walks‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))))
264263com23 86 . . . . . 6 (𝐹(Walks‘𝐺)𝑃 → ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))))
265264expd 451 . . . . 5 (𝐹(Walks‘𝐺)𝑃 → (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))))
2662, 265mpcom 38 . . . 4 (𝐹(Paths‘𝐺)𝑃 → ((𝑃‘0) = (𝑃‘(#‘𝐹)) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑)))))))
267266imp 444 . . 3 ((𝐹(Paths‘𝐺)𝑃 ∧ (𝑃‘0) = (𝑃‘(#‘𝐹))) → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))
2681, 267syl 17 . 2 (𝐹(Cycles‘𝐺)𝑃 → (𝐺 ∈ UPGraph → ((#‘𝐹) = 4 → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))))
2692683imp21 1298 1 ((𝐺 ∈ UPGraph ∧ 𝐹(Cycles‘𝐺)𝑃 ∧ (#‘𝐹) = 4) → ∃𝑎𝑉𝑏𝑉𝑐𝑉𝑑𝑉 ((({𝑎, 𝑏} ∈ 𝐸 ∧ {𝑏, 𝑐} ∈ 𝐸) ∧ ({𝑐, 𝑑} ∈ 𝐸 ∧ {𝑑, 𝑎} ∈ 𝐸)) ∧ ((𝑎𝑏𝑎𝑐𝑎𝑑) ∧ (𝑏𝑐𝑏𝑑𝑐𝑑))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  cun 3605  {cpr 4212   class class class wbr 4685  wf 5922  cfv 5926  (class class class)co 6690  0cc0 9974  1c1 9975   + caddc 9977   < clt 10112  cle 10113  cn 11058  2c2 11108  3c3 11109  4c4 11110  0cn0 11330  ...cfz 12364  ..^cfzo 12504  #chash 13157  Vtxcvtx 25919  Edgcedg 25984  UPGraphcupgr 26020  Walkscwlks 26548  Pathscpths 26664  Cyclesccycls 26736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ifp 1033  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-n0 11331  df-xnn0 11402  df-z 11416  df-uz 11726  df-fz 12365  df-fzo 12505  df-hash 13158  df-word 13331  df-edg 25985  df-uhgr 25998  df-upgr 26022  df-wlks 26551  df-trls 26645  df-pths 26668  df-cycls 26738
This theorem is referenced by:  n4cyclfrgr  27271
  Copyright terms: Public domain W3C validator