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

Theorem vdwlem13 16067
Description: Lemma for vdw 16068. Main induction on 𝐾; 𝐾 = 0, 𝐾 = 1 base cases. (Contributed by Mario Carneiro, 18-Aug-2014.)
Hypotheses
Ref Expression
vdw.r (𝜑𝑅 ∈ Fin)
vdw.k (𝜑𝐾 ∈ ℕ0)
Assertion
Ref Expression
vdwlem13 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅𝑚 (1...𝑛))𝐾 MonoAP 𝑓)
Distinct variable groups:   𝜑,𝑛,𝑓   𝑓,𝐾,𝑛   𝑅,𝑓,𝑛   𝜑,𝑓

Proof of Theorem vdwlem13
Dummy variables 𝑎 𝑐 𝑑 𝑔 𝑘 𝑚 𝑥 𝑟 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elnn1uz2 12047 . . 3 (𝐾 ∈ ℕ ↔ (𝐾 = 1 ∨ 𝐾 ∈ (ℤ‘2)))
2 vdw.r . . . . . . . . . 10 (𝜑𝑅 ∈ Fin)
3 ovex 6936 . . . . . . . . . 10 (1...1) ∈ V
4 elmapg 8134 . . . . . . . . . 10 ((𝑅 ∈ Fin ∧ (1...1) ∈ V) → (𝑓 ∈ (𝑅𝑚 (1...1)) ↔ 𝑓:(1...1)⟶𝑅))
52, 3, 4sylancl 582 . . . . . . . . 9 (𝜑 → (𝑓 ∈ (𝑅𝑚 (1...1)) ↔ 𝑓:(1...1)⟶𝑅))
65biimpa 470 . . . . . . . 8 ((𝜑𝑓 ∈ (𝑅𝑚 (1...1))) → 𝑓:(1...1)⟶𝑅)
7 1nn 11362 . . . . . . . . . 10 1 ∈ ℕ
8 vdwap1 16051 . . . . . . . . . 10 ((1 ∈ ℕ ∧ 1 ∈ ℕ) → (1(AP‘1)1) = {1})
97, 7, 8mp2an 685 . . . . . . . . 9 (1(AP‘1)1) = {1}
10 1z 11734 . . . . . . . . . . . 12 1 ∈ ℤ
11 elfz3 12643 . . . . . . . . . . . 12 (1 ∈ ℤ → 1 ∈ (1...1))
1210, 11mp1i 13 . . . . . . . . . . 11 ((𝜑𝑓:(1...1)⟶𝑅) → 1 ∈ (1...1))
13 eqidd 2825 . . . . . . . . . . 11 ((𝜑𝑓:(1...1)⟶𝑅) → (𝑓‘1) = (𝑓‘1))
14 ffn 6277 . . . . . . . . . . . . 13 (𝑓:(1...1)⟶𝑅𝑓 Fn (1...1))
1514adantl 475 . . . . . . . . . . . 12 ((𝜑𝑓:(1...1)⟶𝑅) → 𝑓 Fn (1...1))
16 fniniseg 6586 . . . . . . . . . . . 12 (𝑓 Fn (1...1) → (1 ∈ (𝑓 “ {(𝑓‘1)}) ↔ (1 ∈ (1...1) ∧ (𝑓‘1) = (𝑓‘1))))
1715, 16syl 17 . . . . . . . . . . 11 ((𝜑𝑓:(1...1)⟶𝑅) → (1 ∈ (𝑓 “ {(𝑓‘1)}) ↔ (1 ∈ (1...1) ∧ (𝑓‘1) = (𝑓‘1))))
1812, 13, 17mpbir2and 706 . . . . . . . . . 10 ((𝜑𝑓:(1...1)⟶𝑅) → 1 ∈ (𝑓 “ {(𝑓‘1)}))
1918snssd 4557 . . . . . . . . 9 ((𝜑𝑓:(1...1)⟶𝑅) → {1} ⊆ (𝑓 “ {(𝑓‘1)}))
209, 19syl5eqss 3873 . . . . . . . 8 ((𝜑𝑓:(1...1)⟶𝑅) → (1(AP‘1)1) ⊆ (𝑓 “ {(𝑓‘1)}))
216, 20syldan 587 . . . . . . 7 ((𝜑𝑓 ∈ (𝑅𝑚 (1...1))) → (1(AP‘1)1) ⊆ (𝑓 “ {(𝑓‘1)}))
2221ralrimiva 3174 . . . . . 6 (𝜑 → ∀𝑓 ∈ (𝑅𝑚 (1...1))(1(AP‘1)1) ⊆ (𝑓 “ {(𝑓‘1)}))
23 fveq2 6432 . . . . . . . . 9 (𝐾 = 1 → (AP‘𝐾) = (AP‘1))
2423oveqd 6921 . . . . . . . 8 (𝐾 = 1 → (1(AP‘𝐾)1) = (1(AP‘1)1))
2524sseq1d 3856 . . . . . . 7 (𝐾 = 1 → ((1(AP‘𝐾)1) ⊆ (𝑓 “ {(𝑓‘1)}) ↔ (1(AP‘1)1) ⊆ (𝑓 “ {(𝑓‘1)})))
2625ralbidv 3194 . . . . . 6 (𝐾 = 1 → (∀𝑓 ∈ (𝑅𝑚 (1...1))(1(AP‘𝐾)1) ⊆ (𝑓 “ {(𝑓‘1)}) ↔ ∀𝑓 ∈ (𝑅𝑚 (1...1))(1(AP‘1)1) ⊆ (𝑓 “ {(𝑓‘1)})))
2722, 26syl5ibrcom 239 . . . . 5 (𝜑 → (𝐾 = 1 → ∀𝑓 ∈ (𝑅𝑚 (1...1))(1(AP‘𝐾)1) ⊆ (𝑓 “ {(𝑓‘1)})))
28 oveq1 6911 . . . . . . . . . . . 12 (𝑎 = 1 → (𝑎(AP‘𝐾)𝑑) = (1(AP‘𝐾)𝑑))
2928sseq1d 3856 . . . . . . . . . . 11 (𝑎 = 1 → ((𝑎(AP‘𝐾)𝑑) ⊆ (𝑓 “ {(𝑓‘1)}) ↔ (1(AP‘𝐾)𝑑) ⊆ (𝑓 “ {(𝑓‘1)})))
30 oveq2 6912 . . . . . . . . . . . 12 (𝑑 = 1 → (1(AP‘𝐾)𝑑) = (1(AP‘𝐾)1))
3130sseq1d 3856 . . . . . . . . . . 11 (𝑑 = 1 → ((1(AP‘𝐾)𝑑) ⊆ (𝑓 “ {(𝑓‘1)}) ↔ (1(AP‘𝐾)1) ⊆ (𝑓 “ {(𝑓‘1)})))
3229, 31rspc2ev 3540 . . . . . . . . . 10 ((1 ∈ ℕ ∧ 1 ∈ ℕ ∧ (1(AP‘𝐾)1) ⊆ (𝑓 “ {(𝑓‘1)})) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝑓 “ {(𝑓‘1)}))
337, 7, 32mp3an12 1581 . . . . . . . . 9 ((1(AP‘𝐾)1) ⊆ (𝑓 “ {(𝑓‘1)}) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝑓 “ {(𝑓‘1)}))
34 fvex 6445 . . . . . . . . . 10 (𝑓‘1) ∈ V
35 sneq 4406 . . . . . . . . . . . . 13 (𝑐 = (𝑓‘1) → {𝑐} = {(𝑓‘1)})
3635imaeq2d 5706 . . . . . . . . . . . 12 (𝑐 = (𝑓‘1) → (𝑓 “ {𝑐}) = (𝑓 “ {(𝑓‘1)}))
3736sseq2d 3857 . . . . . . . . . . 11 (𝑐 = (𝑓‘1) → ((𝑎(AP‘𝐾)𝑑) ⊆ (𝑓 “ {𝑐}) ↔ (𝑎(AP‘𝐾)𝑑) ⊆ (𝑓 “ {(𝑓‘1)})))
38372rexbidv 3266 . . . . . . . . . 10 (𝑐 = (𝑓‘1) → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝑓 “ {𝑐}) ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝑓 “ {(𝑓‘1)})))
3934, 38spcev 3516 . . . . . . . . 9 (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝑓 “ {(𝑓‘1)}) → ∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝑓 “ {𝑐}))
4033, 39syl 17 . . . . . . . 8 ((1(AP‘𝐾)1) ⊆ (𝑓 “ {(𝑓‘1)}) → ∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝑓 “ {𝑐}))
41 vdw.k . . . . . . . . . 10 (𝜑𝐾 ∈ ℕ0)
4241adantr 474 . . . . . . . . 9 ((𝜑𝑓 ∈ (𝑅𝑚 (1...1))) → 𝐾 ∈ ℕ0)
433, 42, 6vdwmc 16052 . . . . . . . 8 ((𝜑𝑓 ∈ (𝑅𝑚 (1...1))) → (𝐾 MonoAP 𝑓 ↔ ∃𝑐𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝑓 “ {𝑐})))
4440, 43syl5ibr 238 . . . . . . 7 ((𝜑𝑓 ∈ (𝑅𝑚 (1...1))) → ((1(AP‘𝐾)1) ⊆ (𝑓 “ {(𝑓‘1)}) → 𝐾 MonoAP 𝑓))
4544ralimdva 3170 . . . . . 6 (𝜑 → (∀𝑓 ∈ (𝑅𝑚 (1...1))(1(AP‘𝐾)1) ⊆ (𝑓 “ {(𝑓‘1)}) → ∀𝑓 ∈ (𝑅𝑚 (1...1))𝐾 MonoAP 𝑓))
46 oveq2 6912 . . . . . . . . . 10 (𝑛 = 1 → (1...𝑛) = (1...1))
4746oveq2d 6920 . . . . . . . . 9 (𝑛 = 1 → (𝑅𝑚 (1...𝑛)) = (𝑅𝑚 (1...1)))
4847raleqdv 3355 . . . . . . . 8 (𝑛 = 1 → (∀𝑓 ∈ (𝑅𝑚 (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑅𝑚 (1...1))𝐾 MonoAP 𝑓))
4948rspcev 3525 . . . . . . 7 ((1 ∈ ℕ ∧ ∀𝑓 ∈ (𝑅𝑚 (1...1))𝐾 MonoAP 𝑓) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅𝑚 (1...𝑛))𝐾 MonoAP 𝑓)
507, 49mpan 683 . . . . . 6 (∀𝑓 ∈ (𝑅𝑚 (1...1))𝐾 MonoAP 𝑓 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅𝑚 (1...𝑛))𝐾 MonoAP 𝑓)
5145, 50syl6 35 . . . . 5 (𝜑 → (∀𝑓 ∈ (𝑅𝑚 (1...1))(1(AP‘𝐾)1) ⊆ (𝑓 “ {(𝑓‘1)}) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅𝑚 (1...𝑛))𝐾 MonoAP 𝑓))
5227, 51syld 47 . . . 4 (𝜑 → (𝐾 = 1 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅𝑚 (1...𝑛))𝐾 MonoAP 𝑓))
53 breq1 4875 . . . . . . . 8 (𝑥 = 2 → (𝑥 MonoAP 𝑓 ↔ 2 MonoAP 𝑓))
5453rexralbidv 3267 . . . . . . 7 (𝑥 = 2 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝑥 MonoAP 𝑓 ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))2 MonoAP 𝑓))
5554ralbidv 3194 . . . . . 6 (𝑥 = 2 → (∀𝑟 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝑥 MonoAP 𝑓 ↔ ∀𝑟 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))2 MonoAP 𝑓))
56 breq1 4875 . . . . . . . 8 (𝑥 = 𝑘 → (𝑥 MonoAP 𝑓𝑘 MonoAP 𝑓))
5756rexralbidv 3267 . . . . . . 7 (𝑥 = 𝑘 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝑥 MonoAP 𝑓 ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝑘 MonoAP 𝑓))
5857ralbidv 3194 . . . . . 6 (𝑥 = 𝑘 → (∀𝑟 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝑥 MonoAP 𝑓 ↔ ∀𝑟 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝑘 MonoAP 𝑓))
59 breq1 4875 . . . . . . . 8 (𝑥 = (𝑘 + 1) → (𝑥 MonoAP 𝑓 ↔ (𝑘 + 1) MonoAP 𝑓))
6059rexralbidv 3267 . . . . . . 7 (𝑥 = (𝑘 + 1) → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝑥 MonoAP 𝑓 ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))(𝑘 + 1) MonoAP 𝑓))
6160ralbidv 3194 . . . . . 6 (𝑥 = (𝑘 + 1) → (∀𝑟 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝑥 MonoAP 𝑓 ↔ ∀𝑟 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))(𝑘 + 1) MonoAP 𝑓))
62 breq1 4875 . . . . . . . 8 (𝑥 = 𝐾 → (𝑥 MonoAP 𝑓𝐾 MonoAP 𝑓))
6362rexralbidv 3267 . . . . . . 7 (𝑥 = 𝐾 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝑥 MonoAP 𝑓 ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝐾 MonoAP 𝑓))
6463ralbidv 3194 . . . . . 6 (𝑥 = 𝐾 → (∀𝑟 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝑥 MonoAP 𝑓 ↔ ∀𝑟 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝐾 MonoAP 𝑓))
65 hashcl 13436 . . . . . . . . . 10 (𝑟 ∈ Fin → (♯‘𝑟) ∈ ℕ0)
66 nn0p1nn 11658 . . . . . . . . . 10 ((♯‘𝑟) ∈ ℕ0 → ((♯‘𝑟) + 1) ∈ ℕ)
6765, 66syl 17 . . . . . . . . 9 (𝑟 ∈ Fin → ((♯‘𝑟) + 1) ∈ ℕ)
68 simpll 785 . . . . . . . . . . . 12 (((𝑟 ∈ Fin ∧ 𝑓 ∈ (𝑟𝑚 (1...((♯‘𝑟) + 1)))) ∧ ¬ 2 MonoAP 𝑓) → 𝑟 ∈ Fin)
69 simplr 787 . . . . . . . . . . . . 13 (((𝑟 ∈ Fin ∧ 𝑓 ∈ (𝑟𝑚 (1...((♯‘𝑟) + 1)))) ∧ ¬ 2 MonoAP 𝑓) → 𝑓 ∈ (𝑟𝑚 (1...((♯‘𝑟) + 1))))
70 vex 3416 . . . . . . . . . . . . . 14 𝑟 ∈ V
71 ovex 6936 . . . . . . . . . . . . . 14 (1...((♯‘𝑟) + 1)) ∈ V
7270, 71elmap 8150 . . . . . . . . . . . . 13 (𝑓 ∈ (𝑟𝑚 (1...((♯‘𝑟) + 1))) ↔ 𝑓:(1...((♯‘𝑟) + 1))⟶𝑟)
7369, 72sylib 210 . . . . . . . . . . . 12 (((𝑟 ∈ Fin ∧ 𝑓 ∈ (𝑟𝑚 (1...((♯‘𝑟) + 1)))) ∧ ¬ 2 MonoAP 𝑓) → 𝑓:(1...((♯‘𝑟) + 1))⟶𝑟)
74 simpr 479 . . . . . . . . . . . 12 (((𝑟 ∈ Fin ∧ 𝑓 ∈ (𝑟𝑚 (1...((♯‘𝑟) + 1)))) ∧ ¬ 2 MonoAP 𝑓) → ¬ 2 MonoAP 𝑓)
7568, 73, 74vdwlem12 16066 . . . . . . . . . . 11 ¬ ((𝑟 ∈ Fin ∧ 𝑓 ∈ (𝑟𝑚 (1...((♯‘𝑟) + 1)))) ∧ ¬ 2 MonoAP 𝑓)
76 iman 392 . . . . . . . . . . 11 (((𝑟 ∈ Fin ∧ 𝑓 ∈ (𝑟𝑚 (1...((♯‘𝑟) + 1)))) → 2 MonoAP 𝑓) ↔ ¬ ((𝑟 ∈ Fin ∧ 𝑓 ∈ (𝑟𝑚 (1...((♯‘𝑟) + 1)))) ∧ ¬ 2 MonoAP 𝑓))
7775, 76mpbir 223 . . . . . . . . . 10 ((𝑟 ∈ Fin ∧ 𝑓 ∈ (𝑟𝑚 (1...((♯‘𝑟) + 1)))) → 2 MonoAP 𝑓)
7877ralrimiva 3174 . . . . . . . . 9 (𝑟 ∈ Fin → ∀𝑓 ∈ (𝑟𝑚 (1...((♯‘𝑟) + 1)))2 MonoAP 𝑓)
79 oveq2 6912 . . . . . . . . . . . 12 (𝑛 = ((♯‘𝑟) + 1) → (1...𝑛) = (1...((♯‘𝑟) + 1)))
8079oveq2d 6920 . . . . . . . . . . 11 (𝑛 = ((♯‘𝑟) + 1) → (𝑟𝑚 (1...𝑛)) = (𝑟𝑚 (1...((♯‘𝑟) + 1))))
8180raleqdv 3355 . . . . . . . . . 10 (𝑛 = ((♯‘𝑟) + 1) → (∀𝑓 ∈ (𝑟𝑚 (1...𝑛))2 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑟𝑚 (1...((♯‘𝑟) + 1)))2 MonoAP 𝑓))
8281rspcev 3525 . . . . . . . . 9 ((((♯‘𝑟) + 1) ∈ ℕ ∧ ∀𝑓 ∈ (𝑟𝑚 (1...((♯‘𝑟) + 1)))2 MonoAP 𝑓) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))2 MonoAP 𝑓)
8367, 78, 82syl2anc 581 . . . . . . . 8 (𝑟 ∈ Fin → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))2 MonoAP 𝑓)
8483rgen 3130 . . . . . . 7 𝑟 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))2 MonoAP 𝑓
8584a1i 11 . . . . . 6 (2 ∈ ℤ → ∀𝑟 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))2 MonoAP 𝑓)
86 oveq1 6911 . . . . . . . . . . 11 (𝑟 = 𝑠 → (𝑟𝑚 (1...𝑛)) = (𝑠𝑚 (1...𝑛)))
8786raleqdv 3355 . . . . . . . . . 10 (𝑟 = 𝑠 → (∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝑘 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑠𝑚 (1...𝑛))𝑘 MonoAP 𝑓))
8887rexbidv 3261 . . . . . . . . 9 (𝑟 = 𝑠 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝑘 MonoAP 𝑓 ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠𝑚 (1...𝑛))𝑘 MonoAP 𝑓))
89 oveq2 6912 . . . . . . . . . . . . 13 (𝑛 = 𝑚 → (1...𝑛) = (1...𝑚))
9089oveq2d 6920 . . . . . . . . . . . 12 (𝑛 = 𝑚 → (𝑠𝑚 (1...𝑛)) = (𝑠𝑚 (1...𝑚)))
9190raleqdv 3355 . . . . . . . . . . 11 (𝑛 = 𝑚 → (∀𝑓 ∈ (𝑠𝑚 (1...𝑛))𝑘 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑠𝑚 (1...𝑚))𝑘 MonoAP 𝑓))
92 breq2 4876 . . . . . . . . . . . 12 (𝑓 = 𝑔 → (𝑘 MonoAP 𝑓𝑘 MonoAP 𝑔))
9392cbvralv 3382 . . . . . . . . . . 11 (∀𝑓 ∈ (𝑠𝑚 (1...𝑚))𝑘 MonoAP 𝑓 ↔ ∀𝑔 ∈ (𝑠𝑚 (1...𝑚))𝑘 MonoAP 𝑔)
9491, 93syl6bb 279 . . . . . . . . . 10 (𝑛 = 𝑚 → (∀𝑓 ∈ (𝑠𝑚 (1...𝑛))𝑘 MonoAP 𝑓 ↔ ∀𝑔 ∈ (𝑠𝑚 (1...𝑚))𝑘 MonoAP 𝑔))
9594cbvrexv 3383 . . . . . . . . 9 (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠𝑚 (1...𝑛))𝑘 MonoAP 𝑓 ↔ ∃𝑚 ∈ ℕ ∀𝑔 ∈ (𝑠𝑚 (1...𝑚))𝑘 MonoAP 𝑔)
9688, 95syl6bb 279 . . . . . . . 8 (𝑟 = 𝑠 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝑘 MonoAP 𝑓 ↔ ∃𝑚 ∈ ℕ ∀𝑔 ∈ (𝑠𝑚 (1...𝑚))𝑘 MonoAP 𝑔))
9796cbvralv 3382 . . . . . . 7 (∀𝑟 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝑘 MonoAP 𝑓 ↔ ∀𝑠 ∈ Fin ∃𝑚 ∈ ℕ ∀𝑔 ∈ (𝑠𝑚 (1...𝑚))𝑘 MonoAP 𝑔)
98 simplr 787 . . . . . . . . . 10 (((𝑘 ∈ (ℤ‘2) ∧ 𝑟 ∈ Fin) ∧ ∀𝑠 ∈ Fin ∃𝑚 ∈ ℕ ∀𝑔 ∈ (𝑠𝑚 (1...𝑚))𝑘 MonoAP 𝑔) → 𝑟 ∈ Fin)
99 simpll 785 . . . . . . . . . 10 (((𝑘 ∈ (ℤ‘2) ∧ 𝑟 ∈ Fin) ∧ ∀𝑠 ∈ Fin ∃𝑚 ∈ ℕ ∀𝑔 ∈ (𝑠𝑚 (1...𝑚))𝑘 MonoAP 𝑔) → 𝑘 ∈ (ℤ‘2))
100 simpr 479 . . . . . . . . . . 11 (((𝑘 ∈ (ℤ‘2) ∧ 𝑟 ∈ Fin) ∧ ∀𝑠 ∈ Fin ∃𝑚 ∈ ℕ ∀𝑔 ∈ (𝑠𝑚 (1...𝑚))𝑘 MonoAP 𝑔) → ∀𝑠 ∈ Fin ∃𝑚 ∈ ℕ ∀𝑔 ∈ (𝑠𝑚 (1...𝑚))𝑘 MonoAP 𝑔)
10195ralbii 3188 . . . . . . . . . . 11 (∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠𝑚 (1...𝑛))𝑘 MonoAP 𝑓 ↔ ∀𝑠 ∈ Fin ∃𝑚 ∈ ℕ ∀𝑔 ∈ (𝑠𝑚 (1...𝑚))𝑘 MonoAP 𝑔)
102100, 101sylibr 226 . . . . . . . . . 10 (((𝑘 ∈ (ℤ‘2) ∧ 𝑟 ∈ Fin) ∧ ∀𝑠 ∈ Fin ∃𝑚 ∈ ℕ ∀𝑔 ∈ (𝑠𝑚 (1...𝑚))𝑘 MonoAP 𝑔) → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠𝑚 (1...𝑛))𝑘 MonoAP 𝑓)
10398, 99, 102vdwlem11 16065 . . . . . . . . 9 (((𝑘 ∈ (ℤ‘2) ∧ 𝑟 ∈ Fin) ∧ ∀𝑠 ∈ Fin ∃𝑚 ∈ ℕ ∀𝑔 ∈ (𝑠𝑚 (1...𝑚))𝑘 MonoAP 𝑔) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))(𝑘 + 1) MonoAP 𝑓)
104103ex 403 . . . . . . . 8 ((𝑘 ∈ (ℤ‘2) ∧ 𝑟 ∈ Fin) → (∀𝑠 ∈ Fin ∃𝑚 ∈ ℕ ∀𝑔 ∈ (𝑠𝑚 (1...𝑚))𝑘 MonoAP 𝑔 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))(𝑘 + 1) MonoAP 𝑓))
105104ralrimdva 3177 . . . . . . 7 (𝑘 ∈ (ℤ‘2) → (∀𝑠 ∈ Fin ∃𝑚 ∈ ℕ ∀𝑔 ∈ (𝑠𝑚 (1...𝑚))𝑘 MonoAP 𝑔 → ∀𝑟 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))(𝑘 + 1) MonoAP 𝑓))
10697, 105syl5bi 234 . . . . . 6 (𝑘 ∈ (ℤ‘2) → (∀𝑟 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝑘 MonoAP 𝑓 → ∀𝑟 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))(𝑘 + 1) MonoAP 𝑓))
10755, 58, 61, 64, 85, 106uzind4 12027 . . . . 5 (𝐾 ∈ (ℤ‘2) → ∀𝑟 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝐾 MonoAP 𝑓)
108 oveq1 6911 . . . . . . . 8 (𝑟 = 𝑅 → (𝑟𝑚 (1...𝑛)) = (𝑅𝑚 (1...𝑛)))
109108raleqdv 3355 . . . . . . 7 (𝑟 = 𝑅 → (∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∀𝑓 ∈ (𝑅𝑚 (1...𝑛))𝐾 MonoAP 𝑓))
110109rexbidv 3261 . . . . . 6 (𝑟 = 𝑅 → (∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝐾 MonoAP 𝑓 ↔ ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅𝑚 (1...𝑛))𝐾 MonoAP 𝑓))
111110rspcv 3521 . . . . 5 (𝑅 ∈ Fin → (∀𝑟 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑟𝑚 (1...𝑛))𝐾 MonoAP 𝑓 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅𝑚 (1...𝑛))𝐾 MonoAP 𝑓))
1122, 107, 111syl2im 40 . . . 4 (𝜑 → (𝐾 ∈ (ℤ‘2) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅𝑚 (1...𝑛))𝐾 MonoAP 𝑓))
11352, 112jaod 892 . . 3 (𝜑 → ((𝐾 = 1 ∨ 𝐾 ∈ (ℤ‘2)) → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅𝑚 (1...𝑛))𝐾 MonoAP 𝑓))
1141, 113syl5bi 234 . 2 (𝜑 → (𝐾 ∈ ℕ → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅𝑚 (1...𝑛))𝐾 MonoAP 𝑓))
115 fveq2 6432 . . . . . . 7 (𝐾 = 0 → (AP‘𝐾) = (AP‘0))
116115oveqd 6921 . . . . . 6 (𝐾 = 0 → (1(AP‘𝐾)1) = (1(AP‘0)1))
117 vdwap0 16050 . . . . . . 7 ((1 ∈ ℕ ∧ 1 ∈ ℕ) → (1(AP‘0)1) = ∅)
1187, 7, 117mp2an 685 . . . . . 6 (1(AP‘0)1) = ∅
119116, 118syl6eq 2876 . . . . 5 (𝐾 = 0 → (1(AP‘𝐾)1) = ∅)
120 0ss 4196 . . . . 5 ∅ ⊆ (𝑓 “ {(𝑓‘1)})
121119, 120syl6eqss 3879 . . . 4 (𝐾 = 0 → (1(AP‘𝐾)1) ⊆ (𝑓 “ {(𝑓‘1)}))
122121ralrimivw 3175 . . 3 (𝐾 = 0 → ∀𝑓 ∈ (𝑅𝑚 (1...1))(1(AP‘𝐾)1) ⊆ (𝑓 “ {(𝑓‘1)}))
123122, 51syl5 34 . 2 (𝜑 → (𝐾 = 0 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅𝑚 (1...𝑛))𝐾 MonoAP 𝑓))
124 elnn0 11619 . . 3 (𝐾 ∈ ℕ0 ↔ (𝐾 ∈ ℕ ∨ 𝐾 = 0))
12541, 124sylib 210 . 2 (𝜑 → (𝐾 ∈ ℕ ∨ 𝐾 = 0))
126114, 123, 125mpjaod 893 1 (𝜑 → ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑅𝑚 (1...𝑛))𝐾 MonoAP 𝑓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wo 880   = wceq 1658  wex 1880  wcel 2166  wral 3116  wrex 3117  Vcvv 3413  wss 3797  c0 4143  {csn 4396   class class class wbr 4872  ccnv 5340  cima 5344   Fn wfn 6117  wf 6118  cfv 6122  (class class class)co 6904  𝑚 cmap 8121  Fincfn 8221  0cc0 10251  1c1 10252   + caddc 10254  cn 11349  2c2 11405  0cn0 11617  cz 11703  cuz 11967  ...cfz 12618  chash 13409  APcvdwa 16039   MonoAP cvdwm 16040
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802  ax-rep 4993  ax-sep 5004  ax-nul 5012  ax-pow 5064  ax-pr 5126  ax-un 7208  ax-cnex 10307  ax-resscn 10308  ax-1cn 10309  ax-icn 10310  ax-addcl 10311  ax-addrcl 10312  ax-mulcl 10313  ax-mulrcl 10314  ax-mulcom 10315  ax-addass 10316  ax-mulass 10317  ax-distr 10318  ax-i2m1 10319  ax-1ne0 10320  ax-1rid 10321  ax-rnegex 10322  ax-rrecex 10323  ax-cnre 10324  ax-pre-lttri 10325  ax-pre-lttrn 10326  ax-pre-ltadd 10327  ax-pre-mulgt0 10328
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2604  df-eu 2639  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-ne 2999  df-nel 3102  df-ral 3121  df-rex 3122  df-reu 3123  df-rmo 3124  df-rab 3125  df-v 3415  df-sbc 3662  df-csb 3757  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-pss 3813  df-nul 4144  df-if 4306  df-pw 4379  df-sn 4397  df-pr 4399  df-tp 4401  df-op 4403  df-uni 4658  df-int 4697  df-iun 4741  df-br 4873  df-opab 4935  df-mpt 4952  df-tr 4975  df-id 5249  df-eprel 5254  df-po 5262  df-so 5263  df-fr 5300  df-we 5302  df-xp 5347  df-rel 5348  df-cnv 5349  df-co 5350  df-dm 5351  df-rn 5352  df-res 5353  df-ima 5354  df-pred 5919  df-ord 5965  df-on 5966  df-lim 5967  df-suc 5968  df-iota 6085  df-fun 6124  df-fn 6125  df-f 6126  df-f1 6127  df-fo 6128  df-f1o 6129  df-fv 6130  df-riota 6865  df-ov 6907  df-oprab 6908  df-mpt2 6909  df-om 7326  df-1st 7427  df-2nd 7428  df-wrecs 7671  df-recs 7733  df-rdg 7771  df-1o 7825  df-2o 7826  df-oadd 7829  df-er 8008  df-map 8123  df-pm 8124  df-en 8222  df-dom 8223  df-sdom 8224  df-fin 8225  df-card 9077  df-cda 9304  df-pnf 10392  df-mnf 10393  df-xr 10394  df-ltxr 10395  df-le 10396  df-sub 10586  df-neg 10587  df-nn 11350  df-2 11413  df-n0 11618  df-xnn0 11690  df-z 11704  df-uz 11968  df-rp 12112  df-fz 12619  df-hash 13410  df-vdwap 16042  df-vdwmc 16043  df-vdwpc 16044
This theorem is referenced by:  vdw  16068
  Copyright terms: Public domain W3C validator