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

Theorem clwlkclwwlkOLD 27383
 Description: Obsolete version of clwlkclwwlk 27382 as of 12-Oct-2022. (Contributed by Alexander van der Vekens, 22-Jun-2018.) (Revised by AV, 24-Apr-2021.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
clwlkclwwlk.v 𝑉 = (Vtx‘𝐺)
clwlkclwwlk.e 𝐸 = (iEdg‘𝐺)
Assertion
Ref Expression
clwlkclwwlkOLD ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓 𝑓(ClWalks‘𝐺)𝑃 ↔ ((lastS‘𝑃) = (𝑃‘0) ∧ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ (ClWWalks‘𝐺))))
Distinct variable groups:   𝑓,𝐸   𝑃,𝑓   𝑓,𝑉   𝑓,𝐺

Proof of Theorem clwlkclwwlkOLD
Dummy variable 𝑖 is distinct from all other variables.
StepHypRef Expression
1 clwlkclwwlk.e . . . . . 6 𝐸 = (iEdg‘𝐺)
21uspgrf1oedg 26522 . . . . 5 (𝐺 ∈ USPGraph → 𝐸:dom 𝐸1-1-onto→(Edg‘𝐺))
3 f1of1 6390 . . . . 5 (𝐸:dom 𝐸1-1-onto→(Edg‘𝐺) → 𝐸:dom 𝐸1-1→(Edg‘𝐺))
42, 3syl 17 . . . 4 (𝐺 ∈ USPGraph → 𝐸:dom 𝐸1-1→(Edg‘𝐺))
5 clwlkclwwlklem3 27381 . . . 4 ((𝐸:dom 𝐸1-1→(Edg‘𝐺) ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓((𝑓 ∈ Word dom 𝐸𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓𝑖)) = {(𝑃𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))) ↔ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))))
64, 5syl3an1 1163 . . 3 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓((𝑓 ∈ Word dom 𝐸𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓𝑖)) = {(𝑃𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))) ↔ ((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))))
7 lencl 13621 . . . . . . . . . . . . . 14 (𝑃 ∈ Word 𝑉 → (♯‘𝑃) ∈ ℕ0)
8 ige2m1fz 12748 . . . . . . . . . . . . . 14 (((♯‘𝑃) ∈ ℕ0 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈ (0...(♯‘𝑃)))
97, 8sylan 575 . . . . . . . . . . . . 13 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈ (0...(♯‘𝑃)))
10 swrd0lenOLD 13738 . . . . . . . . . . . . 13 ((𝑃 ∈ Word 𝑉 ∧ ((♯‘𝑃) − 1) ∈ (0...(♯‘𝑃))) → (♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) = ((♯‘𝑃) − 1))
119, 10syldan 585 . . . . . . . . . . . 12 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) = ((♯‘𝑃) − 1))
127nn0cnd 11704 . . . . . . . . . . . . . . . 16 (𝑃 ∈ Word 𝑉 → (♯‘𝑃) ∈ ℂ)
13 1cnd 10371 . . . . . . . . . . . . . . . 16 (𝑃 ∈ Word 𝑉 → 1 ∈ ℂ)
1412, 13subcld 10734 . . . . . . . . . . . . . . 15 (𝑃 ∈ Word 𝑉 → ((♯‘𝑃) − 1) ∈ ℂ)
1514subid1d 10723 . . . . . . . . . . . . . 14 (𝑃 ∈ Word 𝑉 → (((♯‘𝑃) − 1) − 0) = ((♯‘𝑃) − 1))
1615eqcomd 2784 . . . . . . . . . . . . 13 (𝑃 ∈ Word 𝑉 → ((♯‘𝑃) − 1) = (((♯‘𝑃) − 1) − 0))
1716adantr 474 . . . . . . . . . . . 12 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) = (((♯‘𝑃) − 1) − 0))
1811, 17eqtrd 2814 . . . . . . . . . . 11 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) = (((♯‘𝑃) − 1) − 0))
1918oveq1d 6937 . . . . . . . . . 10 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1) = ((((♯‘𝑃) − 1) − 0) − 1))
2019oveq2d 6938 . . . . . . . . 9 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)) = (0..^((((♯‘𝑃) − 1) − 0) − 1)))
2111oveq1d 6937 . . . . . . . . . . . . 13 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1) = (((♯‘𝑃) − 1) − 1))
2221oveq2d 6938 . . . . . . . . . . . 12 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)) = (0..^(((♯‘𝑃) − 1) − 1)))
2322eleq2d 2845 . . . . . . . . . . 11 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)) ↔ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))))
24 simpll 757 . . . . . . . . . . . . . . 15 (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → 𝑃 ∈ Word 𝑉)
25 wrdlenge2n0 13642 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → 𝑃 ≠ ∅)
2625adantr 474 . . . . . . . . . . . . . . 15 (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → 𝑃 ≠ ∅)
27 nn0z 11752 . . . . . . . . . . . . . . . . . . 19 ((♯‘𝑃) ∈ ℕ0 → (♯‘𝑃) ∈ ℤ)
28 peano2zm 11772 . . . . . . . . . . . . . . . . . . 19 ((♯‘𝑃) ∈ ℤ → ((♯‘𝑃) − 1) ∈ ℤ)
2927, 28syl 17 . . . . . . . . . . . . . . . . . 18 ((♯‘𝑃) ∈ ℕ0 → ((♯‘𝑃) − 1) ∈ ℤ)
307, 29syl 17 . . . . . . . . . . . . . . . . 17 (𝑃 ∈ Word 𝑉 → ((♯‘𝑃) − 1) ∈ ℤ)
3130adantr 474 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈ ℤ)
32 elfzom1elfzo 12855 . . . . . . . . . . . . . . . 16 ((((♯‘𝑃) − 1) ∈ ℤ ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → 𝑖 ∈ (0..^((♯‘𝑃) − 1)))
3331, 32sylan 575 . . . . . . . . . . . . . . 15 (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → 𝑖 ∈ (0..^((♯‘𝑃) − 1)))
34 swrdtrcfvOLD 13760 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word 𝑉𝑃 ≠ ∅ ∧ 𝑖 ∈ (0..^((♯‘𝑃) − 1))) → ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖) = (𝑃𝑖))
3524, 26, 33, 34syl3anc 1439 . . . . . . . . . . . . . 14 (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖) = (𝑃𝑖))
367adantr 474 . . . . . . . . . . . . . . . 16 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (♯‘𝑃) ∈ ℕ0)
37 elfzom1elp1fzo 12854 . . . . . . . . . . . . . . . . 17 ((((♯‘𝑃) − 1) ∈ ℤ ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → (𝑖 + 1) ∈ (0..^((♯‘𝑃) − 1)))
3829, 37sylan 575 . . . . . . . . . . . . . . . 16 (((♯‘𝑃) ∈ ℕ0𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → (𝑖 + 1) ∈ (0..^((♯‘𝑃) − 1)))
3936, 38sylan 575 . . . . . . . . . . . . . . 15 (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → (𝑖 + 1) ∈ (0..^((♯‘𝑃) − 1)))
40 swrdtrcfvOLD 13760 . . . . . . . . . . . . . . 15 ((𝑃 ∈ Word 𝑉𝑃 ≠ ∅ ∧ (𝑖 + 1) ∈ (0..^((♯‘𝑃) − 1))) → ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1)))
4124, 26, 39, 40syl3anc 1439 . . . . . . . . . . . . . 14 (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1)) = (𝑃‘(𝑖 + 1)))
4235, 41preq12d 4508 . . . . . . . . . . . . 13 (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → {((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} = {(𝑃𝑖), (𝑃‘(𝑖 + 1))})
4342eleq1d 2844 . . . . . . . . . . . 12 (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1))) → ({((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))
4443ex 403 . . . . . . . . . . 11 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑖 ∈ (0..^(((♯‘𝑃) − 1) − 1)) → ({((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)))
4523, 44sylbid 232 . . . . . . . . . 10 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)) → ({((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸)))
4645imp 397 . . . . . . . . 9 (((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) ∧ 𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1))) → ({((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ {(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))
4720, 46raleqbidva 3350 . . . . . . . 8 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ↔ ∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸))
48 swrdtrcfvlOLD 13770 . . . . . . . . . 10 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) = (𝑃‘((♯‘𝑃) − 2)))
49 swrdtrcfv0OLD 13761 . . . . . . . . . 10 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0) = (𝑃‘0))
5048, 49preq12d 4508 . . . . . . . . 9 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} = {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)})
5150eleq1d 2844 . . . . . . . 8 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ({(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸 ↔ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸))
5247, 51anbi12d 624 . . . . . . 7 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸) ↔ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)))
5352bicomd 215 . . . . . 6 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) ↔ (∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸)))
54533adant1 1121 . . . . 5 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) ↔ (∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸)))
55 swrdcl 13735 . . . . . . 7 (𝑃 ∈ Word 𝑉 → (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉)
56553ad2ant2 1125 . . . . . 6 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉)
57563biant1d 1551 . . . . 5 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸) ↔ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸)))
5854, 57bitrd 271 . . . 4 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸) ↔ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸)))
5958anbi2d 622 . . 3 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (((lastS‘𝑃) = (𝑃‘0) ∧ (∀𝑖 ∈ (0..^((((♯‘𝑃) − 1) − 0) − 1)){(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(𝑃‘((♯‘𝑃) − 2)), (𝑃‘0)} ∈ ran 𝐸)) ↔ ((lastS‘𝑃) = (𝑃‘0) ∧ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸))))
606, 59bitrd 271 . 2 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓((𝑓 ∈ Word dom 𝐸𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓𝑖)) = {(𝑃𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))) ↔ ((lastS‘𝑃) = (𝑃‘0) ∧ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸))))
61 uspgrupgr 26525 . . . . . 6 (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph)
62 clwlkclwwlk.v . . . . . . . 8 𝑉 = (Vtx‘𝐺)
6362, 1isclwlkupgr 27130 . . . . . . 7 (𝐺 ∈ UPGraph → (𝑓(ClWalks‘𝐺)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸𝑃:(0...(♯‘𝑓))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓𝑖)) = {(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))))))
64 3an4anass 1092 . . . . . . 7 (((𝑓 ∈ Word dom 𝐸𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓𝑖)) = {(𝑃𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓))) ↔ ((𝑓 ∈ Word dom 𝐸𝑃:(0...(♯‘𝑓))⟶𝑉) ∧ (∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓𝑖)) = {(𝑃𝑖), (𝑃‘(𝑖 + 1))} ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓)))))
6563, 64syl6bbr 281 . . . . . 6 (𝐺 ∈ UPGraph → (𝑓(ClWalks‘𝐺)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓𝑖)) = {(𝑃𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓)))))
6661, 65syl 17 . . . . 5 (𝐺 ∈ USPGraph → (𝑓(ClWalks‘𝐺)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓𝑖)) = {(𝑃𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓)))))
6766adantr 474 . . . 4 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉) → (𝑓(ClWalks‘𝐺)𝑃 ↔ ((𝑓 ∈ Word dom 𝐸𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓𝑖)) = {(𝑃𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓)))))
6867exbidv 1964 . . 3 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉) → (∃𝑓 𝑓(ClWalks‘𝐺)𝑃 ↔ ∃𝑓((𝑓 ∈ Word dom 𝐸𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓𝑖)) = {(𝑃𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓)))))
69683adant3 1123 . 2 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓 𝑓(ClWalks‘𝐺)𝑃 ↔ ∃𝑓((𝑓 ∈ Word dom 𝐸𝑃:(0...(♯‘𝑓))⟶𝑉 ∧ ∀𝑖 ∈ (0..^(♯‘𝑓))(𝐸‘(𝑓𝑖)) = {(𝑃𝑖), (𝑃‘(𝑖 + 1))}) ∧ (𝑃‘0) = (𝑃‘(♯‘𝑓)))))
70 eqid 2778 . . . . . 6 (Edg‘𝐺) = (Edg‘𝐺)
7162, 70isclwwlk 27364 . . . . 5 ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ (ClWWalks‘𝐺) ↔ (((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ (Edg‘𝐺)))
72 simpl 476 . . . . . . . . . . 11 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → 𝑃 ∈ Word 𝑉)
73 nn0ge2m1nn 11711 . . . . . . . . . . . 12 (((♯‘𝑃) ∈ ℕ0 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈ ℕ)
747, 73sylan 575 . . . . . . . . . . 11 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ∈ ℕ)
75 nn0re 11652 . . . . . . . . . . . . . . 15 ((♯‘𝑃) ∈ ℕ0 → (♯‘𝑃) ∈ ℝ)
7675lem1d 11311 . . . . . . . . . . . . . 14 ((♯‘𝑃) ∈ ℕ0 → ((♯‘𝑃) − 1) ≤ (♯‘𝑃))
7776a1d 25 . . . . . . . . . . . . 13 ((♯‘𝑃) ∈ ℕ0 → (2 ≤ (♯‘𝑃) → ((♯‘𝑃) − 1) ≤ (♯‘𝑃)))
787, 77syl 17 . . . . . . . . . . . 12 (𝑃 ∈ Word 𝑉 → (2 ≤ (♯‘𝑃) → ((♯‘𝑃) − 1) ≤ (♯‘𝑃)))
7978imp 397 . . . . . . . . . . 11 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((♯‘𝑃) − 1) ≤ (♯‘𝑃))
8072, 74, 793jca 1119 . . . . . . . . . 10 ((𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃 ∈ Word 𝑉 ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧ ((♯‘𝑃) − 1) ≤ (♯‘𝑃)))
81803adant1 1121 . . . . . . . . 9 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃 ∈ Word 𝑉 ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧ ((♯‘𝑃) − 1) ≤ (♯‘𝑃)))
82 swrdn0OLD 13747 . . . . . . . . 9 ((𝑃 ∈ Word 𝑉 ∧ ((♯‘𝑃) − 1) ∈ ℕ ∧ ((♯‘𝑃) − 1) ≤ (♯‘𝑃)) → (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ≠ ∅)
8381, 82syl 17 . . . . . . . 8 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ≠ ∅)
8483biantrud 527 . . . . . . 7 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ↔ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ≠ ∅)))
8584bicomd 215 . . . . . 6 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ≠ ∅) ↔ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉))
86853anbi1d 1513 . . . . 5 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ≠ ∅) ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ (Edg‘𝐺)) ↔ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ (Edg‘𝐺))))
8771, 86syl5bb 275 . . . 4 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ (ClWWalks‘𝐺) ↔ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ (Edg‘𝐺))))
88 biid 253 . . . . 5 ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ↔ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉)
89 edgval 26397 . . . . . . . 8 (Edg‘𝐺) = ran (iEdg‘𝐺)
901eqcomi 2787 . . . . . . . . 9 (iEdg‘𝐺) = 𝐸
9190rneqi 5597 . . . . . . . 8 ran (iEdg‘𝐺) = ran 𝐸
9289, 91eqtri 2802 . . . . . . 7 (Edg‘𝐺) = ran 𝐸
9392eleq2i 2851 . . . . . 6 ({((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ {((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸)
9493ralbii 3162 . . . . 5 (∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ↔ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸)
9592eleq2i 2851 . . . . 5 ({(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ (Edg‘𝐺) ↔ {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸)
9688, 94, 953anbi123i 1155 . . . 4 (((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ (Edg‘𝐺) ∧ {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ (Edg‘𝐺)) ↔ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸))
9787, 96syl6bb 279 . . 3 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ (ClWWalks‘𝐺) ↔ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸)))
9897anbi2d 622 . 2 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (((lastS‘𝑃) = (𝑃‘0) ∧ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ (ClWWalks‘𝐺)) ↔ ((lastS‘𝑃) = (𝑃‘0) ∧ ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ Word 𝑉 ∧ ∀𝑖 ∈ (0..^((♯‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)) − 1)){((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘𝑖), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘(𝑖 + 1))} ∈ ran 𝐸 ∧ {(lastS‘(𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)), ((𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩)‘0)} ∈ ran 𝐸))))
9960, 69, 983bitr4d 303 1 ((𝐺 ∈ USPGraph ∧ 𝑃 ∈ Word 𝑉 ∧ 2 ≤ (♯‘𝑃)) → (∃𝑓 𝑓(ClWalks‘𝐺)𝑃 ↔ ((lastS‘𝑃) = (𝑃‘0) ∧ (𝑃 substr ⟨0, ((♯‘𝑃) − 1)⟩) ∈ (ClWWalks‘𝐺))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1071   = wceq 1601  ∃wex 1823   ∈ wcel 2107   ≠ wne 2969  ∀wral 3090  ∅c0 4141  {cpr 4400  ⟨cop 4404   class class class wbr 4886  dom cdm 5355  ran crn 5356  ⟶wf 6131  –1-1→wf1 6132  –1-1-onto→wf1o 6134  ‘cfv 6135  (class class class)co 6922  0cc0 10272  1c1 10273   + caddc 10275   ≤ cle 10412   − cmin 10606  ℕcn 11374  2c2 11430  ℕ0cn0 11642  ℤcz 11728  ...cfz 12643  ..^cfzo 12784  ♯chash 13435  Word cword 13599  lastSclsw 13652   substr csubstr 13730  Vtxcvtx 26344  iEdgciedg 26345  Edgcedg 26395  UPGraphcupgr 26428  USPGraphcuspgr 26497  ClWalkscclwlks 27122  ClWWalkscclwwlk 27361 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-ifp 1047  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-om 7344  df-1st 7445  df-2nd 7446  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-2o 7844  df-oadd 7847  df-er 8026  df-map 8142  df-pm 8143  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-card 9098  df-cda 9325  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-nn 11375  df-2 11438  df-n0 11643  df-xnn0 11715  df-z 11729  df-uz 11993  df-fz 12644  df-fzo 12785  df-hash 13436  df-word 13600  df-lsw 13653  df-substr 13731  df-edg 26396  df-uhgr 26406  df-upgr 26430  df-uspgr 26499  df-wlks 26947  df-clwlks 27123  df-clwwlk 27362 This theorem is referenced by:  clwlkclwwlk2OLD  27385  clwlkclwwlkfOLD  27392
 Copyright terms: Public domain W3C validator