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

Theorem wlkwwlksur 26998
 Description: Lemma 3 for wlkwwlkbij2 27000. (Contributed by Alexander van der Vekens, 23-Jul-2018.) (Revised by AV, 16-Apr-2021.)
Hypotheses
Ref Expression
wlkwwlkbij.t 𝑇 = {𝑝 ∈ (Walks‘𝐺) ∣ ((♯‘(1st𝑝)) = 𝑁 ∧ ((2nd𝑝)‘0) = 𝑃)}
wlkwwlkbij.w 𝑊 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}
wlkwwlkbij.f 𝐹 = (𝑡𝑇 ↦ (2nd𝑡))
Assertion
Ref Expression
wlkwwlksur ((𝐺 ∈ USPGraph ∧ 𝑃𝑉𝑁 ∈ ℕ0) → 𝐹:𝑇onto𝑊)
Distinct variable groups:   𝐺,𝑝,𝑡,𝑤   𝑁,𝑝,𝑡,𝑤   𝑃,𝑝,𝑡,𝑤   𝑡,𝑇,𝑤   𝑡,𝑉   𝑡,𝑊   𝑤,𝐹   𝑤,𝑉   𝐹,𝑝   𝑇,𝑝   𝑊,𝑝
Allowed substitution hints:   𝐹(𝑡)   𝑉(𝑝)   𝑊(𝑤)

Proof of Theorem wlkwwlksur
Dummy variables 𝑢 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uspgrupgr 26262 . . 3 (𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph)
2 wlkwwlkbij.t . . . 4 𝑇 = {𝑝 ∈ (Walks‘𝐺) ∣ ((♯‘(1st𝑝)) = 𝑁 ∧ ((2nd𝑝)‘0) = 𝑃)}
3 wlkwwlkbij.w . . . 4 𝑊 = {𝑤 ∈ (𝑁 WWalksN 𝐺) ∣ (𝑤‘0) = 𝑃}
4 wlkwwlkbij.f . . . 4 𝐹 = (𝑡𝑇 ↦ (2nd𝑡))
52, 3, 4wlkwwlkfun 26996 . . 3 ((𝐺 ∈ UPGraph ∧ 𝑃𝑉𝑁 ∈ ℕ0) → 𝐹:𝑇𝑊)
61, 5syl3an1 1166 . 2 ((𝐺 ∈ USPGraph ∧ 𝑃𝑉𝑁 ∈ ℕ0) → 𝐹:𝑇𝑊)
7 fveq1 6343 . . . . . . 7 (𝑤 = 𝑝 → (𝑤‘0) = (𝑝‘0))
87eqeq1d 2754 . . . . . 6 (𝑤 = 𝑝 → ((𝑤‘0) = 𝑃 ↔ (𝑝‘0) = 𝑃))
98, 3elrab2 3499 . . . . 5 (𝑝𝑊 ↔ (𝑝 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑝‘0) = 𝑃))
10 wlklnwwlkn 26985 . . . . . . . . . . 11 (𝐺 ∈ USPGraph → (∃𝑓(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 𝑁) ↔ 𝑝 ∈ (𝑁 WWalksN 𝐺)))
11 df-br 4797 . . . . . . . . . . . . 13 (𝑓(Walks‘𝐺)𝑝 ↔ ⟨𝑓, 𝑝⟩ ∈ (Walks‘𝐺))
12 vex 3335 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
13 vex 3335 . . . . . . . . . . . . . . . . 17 𝑝 ∈ V
1412, 13op1st 7333 . . . . . . . . . . . . . . . 16 (1st ‘⟨𝑓, 𝑝⟩) = 𝑓
1514eqcomi 2761 . . . . . . . . . . . . . . 15 𝑓 = (1st ‘⟨𝑓, 𝑝⟩)
1615fveq2i 6347 . . . . . . . . . . . . . 14 (♯‘𝑓) = (♯‘(1st ‘⟨𝑓, 𝑝⟩))
1716eqeq1i 2757 . . . . . . . . . . . . 13 ((♯‘𝑓) = 𝑁 ↔ (♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁)
1812, 13op2nd 7334 . . . . . . . . . . . . . . . . 17 (2nd ‘⟨𝑓, 𝑝⟩) = 𝑝
1918eqcomi 2761 . . . . . . . . . . . . . . . 16 𝑝 = (2nd ‘⟨𝑓, 𝑝⟩)
2019fveq1i 6345 . . . . . . . . . . . . . . 15 (𝑝‘0) = ((2nd ‘⟨𝑓, 𝑝⟩)‘0)
2120eqeq1i 2757 . . . . . . . . . . . . . 14 ((𝑝‘0) = 𝑃 ↔ ((2nd ‘⟨𝑓, 𝑝⟩)‘0) = 𝑃)
22 opex 5073 . . . . . . . . . . . . . . . 16 𝑓, 𝑝⟩ ∈ V
2322a1i 11 . . . . . . . . . . . . . . 15 ((⟨𝑓, 𝑝⟩ ∈ (Walks‘𝐺) ∧ (♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁) → ⟨𝑓, 𝑝⟩ ∈ V)
24 simpll 807 . . . . . . . . . . . . . . . . . 18 (((⟨𝑓, 𝑝⟩ ∈ (Walks‘𝐺) ∧ (♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁) ∧ ((2nd ‘⟨𝑓, 𝑝⟩)‘0) = 𝑃) → ⟨𝑓, 𝑝⟩ ∈ (Walks‘𝐺))
25 simpr 479 . . . . . . . . . . . . . . . . . . 19 ((⟨𝑓, 𝑝⟩ ∈ (Walks‘𝐺) ∧ (♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁) → (♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁)
2625anim1i 593 . . . . . . . . . . . . . . . . . 18 (((⟨𝑓, 𝑝⟩ ∈ (Walks‘𝐺) ∧ (♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁) ∧ ((2nd ‘⟨𝑓, 𝑝⟩)‘0) = 𝑃) → ((♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁 ∧ ((2nd ‘⟨𝑓, 𝑝⟩)‘0) = 𝑃))
2719a1i 11 . . . . . . . . . . . . . . . . . 18 (((⟨𝑓, 𝑝⟩ ∈ (Walks‘𝐺) ∧ (♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁) ∧ ((2nd ‘⟨𝑓, 𝑝⟩)‘0) = 𝑃) → 𝑝 = (2nd ‘⟨𝑓, 𝑝⟩))
2824, 26, 27jca31 558 . . . . . . . . . . . . . . . . 17 (((⟨𝑓, 𝑝⟩ ∈ (Walks‘𝐺) ∧ (♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁) ∧ ((2nd ‘⟨𝑓, 𝑝⟩)‘0) = 𝑃) → ((⟨𝑓, 𝑝⟩ ∈ (Walks‘𝐺) ∧ ((♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁 ∧ ((2nd ‘⟨𝑓, 𝑝⟩)‘0) = 𝑃)) ∧ 𝑝 = (2nd ‘⟨𝑓, 𝑝⟩)))
29 eleq1 2819 . . . . . . . . . . . . . . . . . . 19 (𝑢 = ⟨𝑓, 𝑝⟩ → (𝑢 ∈ (Walks‘𝐺) ↔ ⟨𝑓, 𝑝⟩ ∈ (Walks‘𝐺)))
30 fveq2 6344 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = ⟨𝑓, 𝑝⟩ → (1st𝑢) = (1st ‘⟨𝑓, 𝑝⟩))
3130fveq2d 6348 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = ⟨𝑓, 𝑝⟩ → (♯‘(1st𝑢)) = (♯‘(1st ‘⟨𝑓, 𝑝⟩)))
3231eqeq1d 2754 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = ⟨𝑓, 𝑝⟩ → ((♯‘(1st𝑢)) = 𝑁 ↔ (♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁))
33 fveq2 6344 . . . . . . . . . . . . . . . . . . . . . 22 (𝑢 = ⟨𝑓, 𝑝⟩ → (2nd𝑢) = (2nd ‘⟨𝑓, 𝑝⟩))
3433fveq1d 6346 . . . . . . . . . . . . . . . . . . . . 21 (𝑢 = ⟨𝑓, 𝑝⟩ → ((2nd𝑢)‘0) = ((2nd ‘⟨𝑓, 𝑝⟩)‘0))
3534eqeq1d 2754 . . . . . . . . . . . . . . . . . . . 20 (𝑢 = ⟨𝑓, 𝑝⟩ → (((2nd𝑢)‘0) = 𝑃 ↔ ((2nd ‘⟨𝑓, 𝑝⟩)‘0) = 𝑃))
3632, 35anbi12d 749 . . . . . . . . . . . . . . . . . . 19 (𝑢 = ⟨𝑓, 𝑝⟩ → (((♯‘(1st𝑢)) = 𝑁 ∧ ((2nd𝑢)‘0) = 𝑃) ↔ ((♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁 ∧ ((2nd ‘⟨𝑓, 𝑝⟩)‘0) = 𝑃)))
3729, 36anbi12d 749 . . . . . . . . . . . . . . . . . 18 (𝑢 = ⟨𝑓, 𝑝⟩ → ((𝑢 ∈ (Walks‘𝐺) ∧ ((♯‘(1st𝑢)) = 𝑁 ∧ ((2nd𝑢)‘0) = 𝑃)) ↔ (⟨𝑓, 𝑝⟩ ∈ (Walks‘𝐺) ∧ ((♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁 ∧ ((2nd ‘⟨𝑓, 𝑝⟩)‘0) = 𝑃))))
3833eqeq2d 2762 . . . . . . . . . . . . . . . . . 18 (𝑢 = ⟨𝑓, 𝑝⟩ → (𝑝 = (2nd𝑢) ↔ 𝑝 = (2nd ‘⟨𝑓, 𝑝⟩)))
3937, 38anbi12d 749 . . . . . . . . . . . . . . . . 17 (𝑢 = ⟨𝑓, 𝑝⟩ → (((𝑢 ∈ (Walks‘𝐺) ∧ ((♯‘(1st𝑢)) = 𝑁 ∧ ((2nd𝑢)‘0) = 𝑃)) ∧ 𝑝 = (2nd𝑢)) ↔ ((⟨𝑓, 𝑝⟩ ∈ (Walks‘𝐺) ∧ ((♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁 ∧ ((2nd ‘⟨𝑓, 𝑝⟩)‘0) = 𝑃)) ∧ 𝑝 = (2nd ‘⟨𝑓, 𝑝⟩))))
4028, 39syl5ibrcom 237 . . . . . . . . . . . . . . . 16 (((⟨𝑓, 𝑝⟩ ∈ (Walks‘𝐺) ∧ (♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁) ∧ ((2nd ‘⟨𝑓, 𝑝⟩)‘0) = 𝑃) → (𝑢 = ⟨𝑓, 𝑝⟩ → ((𝑢 ∈ (Walks‘𝐺) ∧ ((♯‘(1st𝑢)) = 𝑁 ∧ ((2nd𝑢)‘0) = 𝑃)) ∧ 𝑝 = (2nd𝑢))))
4140impancom 455 . . . . . . . . . . . . . . 15 (((⟨𝑓, 𝑝⟩ ∈ (Walks‘𝐺) ∧ (♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁) ∧ 𝑢 = ⟨𝑓, 𝑝⟩) → (((2nd ‘⟨𝑓, 𝑝⟩)‘0) = 𝑃 → ((𝑢 ∈ (Walks‘𝐺) ∧ ((♯‘(1st𝑢)) = 𝑁 ∧ ((2nd𝑢)‘0) = 𝑃)) ∧ 𝑝 = (2nd𝑢))))
4223, 41spcimedv 3424 . . . . . . . . . . . . . 14 ((⟨𝑓, 𝑝⟩ ∈ (Walks‘𝐺) ∧ (♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁) → (((2nd ‘⟨𝑓, 𝑝⟩)‘0) = 𝑃 → ∃𝑢((𝑢 ∈ (Walks‘𝐺) ∧ ((♯‘(1st𝑢)) = 𝑁 ∧ ((2nd𝑢)‘0) = 𝑃)) ∧ 𝑝 = (2nd𝑢))))
4321, 42syl5bi 232 . . . . . . . . . . . . 13 ((⟨𝑓, 𝑝⟩ ∈ (Walks‘𝐺) ∧ (♯‘(1st ‘⟨𝑓, 𝑝⟩)) = 𝑁) → ((𝑝‘0) = 𝑃 → ∃𝑢((𝑢 ∈ (Walks‘𝐺) ∧ ((♯‘(1st𝑢)) = 𝑁 ∧ ((2nd𝑢)‘0) = 𝑃)) ∧ 𝑝 = (2nd𝑢))))
4411, 17, 43syl2anb 497 . . . . . . . . . . . 12 ((𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 𝑁) → ((𝑝‘0) = 𝑃 → ∃𝑢((𝑢 ∈ (Walks‘𝐺) ∧ ((♯‘(1st𝑢)) = 𝑁 ∧ ((2nd𝑢)‘0) = 𝑃)) ∧ 𝑝 = (2nd𝑢))))
4544exlimiv 1999 . . . . . . . . . . 11 (∃𝑓(𝑓(Walks‘𝐺)𝑝 ∧ (♯‘𝑓) = 𝑁) → ((𝑝‘0) = 𝑃 → ∃𝑢((𝑢 ∈ (Walks‘𝐺) ∧ ((♯‘(1st𝑢)) = 𝑁 ∧ ((2nd𝑢)‘0) = 𝑃)) ∧ 𝑝 = (2nd𝑢))))
4610, 45syl6bir 244 . . . . . . . . . 10 (𝐺 ∈ USPGraph → (𝑝 ∈ (𝑁 WWalksN 𝐺) → ((𝑝‘0) = 𝑃 → ∃𝑢((𝑢 ∈ (Walks‘𝐺) ∧ ((♯‘(1st𝑢)) = 𝑁 ∧ ((2nd𝑢)‘0) = 𝑃)) ∧ 𝑝 = (2nd𝑢)))))
4746imp32 448 . . . . . . . . 9 ((𝐺 ∈ USPGraph ∧ (𝑝 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑝‘0) = 𝑃)) → ∃𝑢((𝑢 ∈ (Walks‘𝐺) ∧ ((♯‘(1st𝑢)) = 𝑁 ∧ ((2nd𝑢)‘0) = 𝑃)) ∧ 𝑝 = (2nd𝑢)))
48 fveq2 6344 . . . . . . . . . . . . . . 15 (𝑝 = 𝑢 → (1st𝑝) = (1st𝑢))
4948fveq2d 6348 . . . . . . . . . . . . . 14 (𝑝 = 𝑢 → (♯‘(1st𝑝)) = (♯‘(1st𝑢)))
5049eqeq1d 2754 . . . . . . . . . . . . 13 (𝑝 = 𝑢 → ((♯‘(1st𝑝)) = 𝑁 ↔ (♯‘(1st𝑢)) = 𝑁))
51 fveq2 6344 . . . . . . . . . . . . . . 15 (𝑝 = 𝑢 → (2nd𝑝) = (2nd𝑢))
5251fveq1d 6346 . . . . . . . . . . . . . 14 (𝑝 = 𝑢 → ((2nd𝑝)‘0) = ((2nd𝑢)‘0))
5352eqeq1d 2754 . . . . . . . . . . . . 13 (𝑝 = 𝑢 → (((2nd𝑝)‘0) = 𝑃 ↔ ((2nd𝑢)‘0) = 𝑃))
5450, 53anbi12d 749 . . . . . . . . . . . 12 (𝑝 = 𝑢 → (((♯‘(1st𝑝)) = 𝑁 ∧ ((2nd𝑝)‘0) = 𝑃) ↔ ((♯‘(1st𝑢)) = 𝑁 ∧ ((2nd𝑢)‘0) = 𝑃)))
5554elrab 3496 . . . . . . . . . . 11 (𝑢 ∈ {𝑝 ∈ (Walks‘𝐺) ∣ ((♯‘(1st𝑝)) = 𝑁 ∧ ((2nd𝑝)‘0) = 𝑃)} ↔ (𝑢 ∈ (Walks‘𝐺) ∧ ((♯‘(1st𝑢)) = 𝑁 ∧ ((2nd𝑢)‘0) = 𝑃)))
5655anbi1i 733 . . . . . . . . . 10 ((𝑢 ∈ {𝑝 ∈ (Walks‘𝐺) ∣ ((♯‘(1st𝑝)) = 𝑁 ∧ ((2nd𝑝)‘0) = 𝑃)} ∧ 𝑝 = (2nd𝑢)) ↔ ((𝑢 ∈ (Walks‘𝐺) ∧ ((♯‘(1st𝑢)) = 𝑁 ∧ ((2nd𝑢)‘0) = 𝑃)) ∧ 𝑝 = (2nd𝑢)))
5756exbii 1915 . . . . . . . . 9 (∃𝑢(𝑢 ∈ {𝑝 ∈ (Walks‘𝐺) ∣ ((♯‘(1st𝑝)) = 𝑁 ∧ ((2nd𝑝)‘0) = 𝑃)} ∧ 𝑝 = (2nd𝑢)) ↔ ∃𝑢((𝑢 ∈ (Walks‘𝐺) ∧ ((♯‘(1st𝑢)) = 𝑁 ∧ ((2nd𝑢)‘0) = 𝑃)) ∧ 𝑝 = (2nd𝑢)))
5847, 57sylibr 224 . . . . . . . 8 ((𝐺 ∈ USPGraph ∧ (𝑝 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑝‘0) = 𝑃)) → ∃𝑢(𝑢 ∈ {𝑝 ∈ (Walks‘𝐺) ∣ ((♯‘(1st𝑝)) = 𝑁 ∧ ((2nd𝑝)‘0) = 𝑃)} ∧ 𝑝 = (2nd𝑢)))
59 df-rex 3048 . . . . . . . 8 (∃𝑢 ∈ {𝑝 ∈ (Walks‘𝐺) ∣ ((♯‘(1st𝑝)) = 𝑁 ∧ ((2nd𝑝)‘0) = 𝑃)}𝑝 = (2nd𝑢) ↔ ∃𝑢(𝑢 ∈ {𝑝 ∈ (Walks‘𝐺) ∣ ((♯‘(1st𝑝)) = 𝑁 ∧ ((2nd𝑝)‘0) = 𝑃)} ∧ 𝑝 = (2nd𝑢)))
6058, 59sylibr 224 . . . . . . 7 ((𝐺 ∈ USPGraph ∧ (𝑝 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑝‘0) = 𝑃)) → ∃𝑢 ∈ {𝑝 ∈ (Walks‘𝐺) ∣ ((♯‘(1st𝑝)) = 𝑁 ∧ ((2nd𝑝)‘0) = 𝑃)}𝑝 = (2nd𝑢))
612rexeqi 3274 . . . . . . 7 (∃𝑢𝑇 𝑝 = (2nd𝑢) ↔ ∃𝑢 ∈ {𝑝 ∈ (Walks‘𝐺) ∣ ((♯‘(1st𝑝)) = 𝑁 ∧ ((2nd𝑝)‘0) = 𝑃)}𝑝 = (2nd𝑢))
6260, 61sylibr 224 . . . . . 6 ((𝐺 ∈ USPGraph ∧ (𝑝 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑝‘0) = 𝑃)) → ∃𝑢𝑇 𝑝 = (2nd𝑢))
63 fveq2 6344 . . . . . . . . 9 (𝑡 = 𝑢 → (2nd𝑡) = (2nd𝑢))
64 fvex 6354 . . . . . . . . 9 (2nd𝑢) ∈ V
6563, 4, 64fvmpt 6436 . . . . . . . 8 (𝑢𝑇 → (𝐹𝑢) = (2nd𝑢))
6665eqeq2d 2762 . . . . . . 7 (𝑢𝑇 → (𝑝 = (𝐹𝑢) ↔ 𝑝 = (2nd𝑢)))
6766rexbiia 3170 . . . . . 6 (∃𝑢𝑇 𝑝 = (𝐹𝑢) ↔ ∃𝑢𝑇 𝑝 = (2nd𝑢))
6862, 67sylibr 224 . . . . 5 ((𝐺 ∈ USPGraph ∧ (𝑝 ∈ (𝑁 WWalksN 𝐺) ∧ (𝑝‘0) = 𝑃)) → ∃𝑢𝑇 𝑝 = (𝐹𝑢))
699, 68sylan2b 493 . . . 4 ((𝐺 ∈ USPGraph ∧ 𝑝𝑊) → ∃𝑢𝑇 𝑝 = (𝐹𝑢))
7069ralrimiva 3096 . . 3 (𝐺 ∈ USPGraph → ∀𝑝𝑊𝑢𝑇 𝑝 = (𝐹𝑢))
71703ad2ant1 1127 . 2 ((𝐺 ∈ USPGraph ∧ 𝑃𝑉𝑁 ∈ ℕ0) → ∀𝑝𝑊𝑢𝑇 𝑝 = (𝐹𝑢))
72 dffo3 6529 . 2 (𝐹:𝑇onto𝑊 ↔ (𝐹:𝑇𝑊 ∧ ∀𝑝𝑊𝑢𝑇 𝑝 = (𝐹𝑢)))
736, 71, 72sylanbrc 701 1 ((𝐺 ∈ USPGraph ∧ 𝑃𝑉𝑁 ∈ ℕ0) → 𝐹:𝑇onto𝑊)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072   = wceq 1624  ∃wex 1845   ∈ wcel 2131  ∀wral 3042  ∃wrex 3043  {crab 3046  Vcvv 3332  ⟨cop 4319   class class class wbr 4796   ↦ cmpt 4873  ⟶wf 6037  –onto→wfo 6039  ‘cfv 6041  (class class class)co 6805  1st c1st 7323  2nd c2nd 7324  0cc0 10120  ℕ0cn0 11476  ♯chash 13303  UPGraphcupgr 26166  USPGraphcuspgr 26234  Walkscwlks 26694   WWalksN cwwlksn 26921 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-8 2133  ax-9 2140  ax-10 2160  ax-11 2175  ax-12 2188  ax-13 2383  ax-ext 2732  ax-rep 4915  ax-sep 4925  ax-nul 4933  ax-pow 4984  ax-pr 5047  ax-un 7106  ax-cnex 10176  ax-resscn 10177  ax-1cn 10178  ax-icn 10179  ax-addcl 10180  ax-addrcl 10181  ax-mulcl 10182  ax-mulrcl 10183  ax-mulcom 10184  ax-addass 10185  ax-mulass 10186  ax-distr 10187  ax-i2m1 10188  ax-1ne0 10189  ax-1rid 10190  ax-rnegex 10191  ax-rrecex 10192  ax-cnre 10193  ax-pre-lttri 10194  ax-pre-lttrn 10195  ax-pre-ltadd 10196  ax-pre-mulgt0 10197 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-ifp 1051  df-3or 1073  df-3an 1074  df-tru 1627  df-ex 1846  df-nf 1851  df-sb 2039  df-eu 2603  df-mo 2604  df-clab 2739  df-cleq 2745  df-clel 2748  df-nfc 2883  df-ne 2925  df-nel 3028  df-ral 3047  df-rex 3048  df-reu 3049  df-rmo 3050  df-rab 3051  df-v 3334  df-sbc 3569  df-csb 3667  df-dif 3710  df-un 3712  df-in 3714  df-ss 3721  df-pss 3723  df-nul 4051  df-if 4223  df-pw 4296  df-sn 4314  df-pr 4316  df-tp 4318  df-op 4320  df-uni 4581  df-int 4620  df-iun 4666  df-br 4797  df-opab 4857  df-mpt 4874  df-tr 4897  df-id 5166  df-eprel 5171  df-po 5179  df-so 5180  df-fr 5217  df-we 5219  df-xp 5264  df-rel 5265  df-cnv 5266  df-co 5267  df-dm 5268  df-rn 5269  df-res 5270  df-ima 5271  df-pred 5833  df-ord 5879  df-on 5880  df-lim 5881  df-suc 5882  df-iota 6004  df-fun 6043  df-fn 6044  df-f 6045  df-f1 6046  df-fo 6047  df-f1o 6048  df-fv 6049  df-riota 6766  df-ov 6808  df-oprab 6809  df-mpt2 6810  df-om 7223  df-1st 7325  df-2nd 7326  df-wrecs 7568  df-recs 7629  df-rdg 7667  df-1o 7721  df-2o 7722  df-oadd 7725  df-er 7903  df-map 8017  df-pm 8018  df-en 8114  df-dom 8115  df-sdom 8116  df-fin 8117  df-card 8947  df-cda 9174  df-pnf 10260  df-mnf 10261  df-xr 10262  df-ltxr 10263  df-le 10264  df-sub 10452  df-neg 10453  df-nn 11205  df-2 11263  df-n0 11477  df-xnn0 11548  df-z 11562  df-uz 11872  df-fz 12512  df-fzo 12652  df-hash 13304  df-word 13477  df-edg 26131  df-uhgr 26144  df-upgr 26168  df-uspgr 26236  df-wlks 26697  df-wwlks 26925  df-wwlksn 26926 This theorem is referenced by:  wlkwwlkbij  26999
 Copyright terms: Public domain W3C validator