Step | Hyp | Ref
| Expression |
1 | | vdwlem1.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℕ) |
2 | | vdwlem1.d |
. . . . 5
⊢ (𝜑 → 𝐷:(1...𝑀)⟶ℕ) |
3 | | vdwlem1.i |
. . . . 5
⊢ (𝜑 → 𝐼 ∈ (1...𝑀)) |
4 | 2, 3 | ffvelrnd 6962 |
. . . 4
⊢ (𝜑 → (𝐷‘𝐼) ∈ ℕ) |
5 | | vdwlem1.k |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ ℕ) |
6 | 5 | nnnn0d 12293 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
7 | | vdwapun 16675 |
. . . . . 6
⊢ ((𝐾 ∈ ℕ0
∧ 𝐴 ∈ ℕ
∧ (𝐷‘𝐼) ∈ ℕ) → (𝐴(AP‘(𝐾 + 1))(𝐷‘𝐼)) = ({𝐴} ∪ ((𝐴 + (𝐷‘𝐼))(AP‘𝐾)(𝐷‘𝐼)))) |
8 | 6, 1, 4, 7 | syl3anc 1370 |
. . . . 5
⊢ (𝜑 → (𝐴(AP‘(𝐾 + 1))(𝐷‘𝐼)) = ({𝐴} ∪ ((𝐴 + (𝐷‘𝐼))(AP‘𝐾)(𝐷‘𝐼)))) |
9 | 1 | nnred 11988 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
10 | | vdwlem1.m |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈ ℕ) |
11 | | nnuz 12621 |
. . . . . . . . . . . . . . 15
⊢ ℕ =
(ℤ≥‘1) |
12 | 10, 11 | eleqtrdi 2849 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
13 | | eluzfz1 13263 |
. . . . . . . . . . . . . 14
⊢ (𝑀 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑀)) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ∈ (1...𝑀)) |
15 | 2, 14 | ffvelrnd 6962 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐷‘1) ∈ ℕ) |
16 | 1, 15 | nnaddcld 12025 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 + (𝐷‘1)) ∈ ℕ) |
17 | 16 | nnred 11988 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 + (𝐷‘1)) ∈ ℝ) |
18 | | vdwlem1.w |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ ℕ) |
19 | 18 | nnred 11988 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ ℝ) |
20 | 15 | nnrpd 12770 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐷‘1) ∈
ℝ+) |
21 | 9, 20 | ltaddrpd 12805 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 < (𝐴 + (𝐷‘1))) |
22 | 9, 17, 21 | ltled 11123 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ≤ (𝐴 + (𝐷‘1))) |
23 | | fveq2 6774 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = 1 → (𝐷‘𝑖) = (𝐷‘1)) |
24 | 23 | oveq2d 7291 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 1 → (𝐴 + (𝐷‘𝑖)) = (𝐴 + (𝐷‘1))) |
25 | 24 | eleq1d 2823 |
. . . . . . . . . . . 12
⊢ (𝑖 = 1 → ((𝐴 + (𝐷‘𝑖)) ∈ (1...𝑊) ↔ (𝐴 + (𝐷‘1)) ∈ (1...𝑊))) |
26 | | vdwlem1.s |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝑖)))})) |
27 | 26 | r19.21bi 3134 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝑖)))})) |
28 | | cnvimass 5989 |
. . . . . . . . . . . . . . . . 17
⊢ (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝑖)))}) ⊆ dom 𝐹 |
29 | | vdwlem1.f |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:(1...𝑊)⟶𝑅) |
30 | 28, 29 | fssdm 6620 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝑖)))}) ⊆ (1...𝑊)) |
31 | 30 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝑖)))}) ⊆ (1...𝑊)) |
32 | 27, 31 | sstrd 3931 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖)) ⊆ (1...𝑊)) |
33 | | nnm1nn0 12274 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈
ℕ0) |
34 | 5, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐾 − 1) ∈
ℕ0) |
35 | | nn0uz 12620 |
. . . . . . . . . . . . . . . . . . 19
⊢
ℕ0 = (ℤ≥‘0) |
36 | 34, 35 | eleqtrdi 2849 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐾 − 1) ∈
(ℤ≥‘0)) |
37 | | eluzfz1 13263 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 − 1) ∈
(ℤ≥‘0) → 0 ∈ (0...(𝐾 − 1))) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 ∈ (0...(𝐾 − 1))) |
39 | 38 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 0 ∈ (0...(𝐾 − 1))) |
40 | 2 | ffvelrnda 6961 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐷‘𝑖) ∈ ℕ) |
41 | 40 | nncnd 11989 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐷‘𝑖) ∈ ℂ) |
42 | 41 | mul02d 11173 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (0 · (𝐷‘𝑖)) = 0) |
43 | 42 | oveq2d 7291 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐴 + (𝐷‘𝑖)) + (0 · (𝐷‘𝑖))) = ((𝐴 + (𝐷‘𝑖)) + 0)) |
44 | 1 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐴 ∈ ℕ) |
45 | 44, 40 | nnaddcld 12025 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐴 + (𝐷‘𝑖)) ∈ ℕ) |
46 | 45 | nncnd 11989 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐴 + (𝐷‘𝑖)) ∈ ℂ) |
47 | 46 | addid1d 11175 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐴 + (𝐷‘𝑖)) + 0) = (𝐴 + (𝐷‘𝑖))) |
48 | 43, 47 | eqtr2d 2779 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐴 + (𝐷‘𝑖)) = ((𝐴 + (𝐷‘𝑖)) + (0 · (𝐷‘𝑖)))) |
49 | | oveq1 7282 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 = 0 → (𝑚 · (𝐷‘𝑖)) = (0 · (𝐷‘𝑖))) |
50 | 49 | oveq2d 7291 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = 0 → ((𝐴 + (𝐷‘𝑖)) + (𝑚 · (𝐷‘𝑖))) = ((𝐴 + (𝐷‘𝑖)) + (0 · (𝐷‘𝑖)))) |
51 | 50 | rspceeqv 3575 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ (0...(𝐾 − 1))
∧ (𝐴 + (𝐷‘𝑖)) = ((𝐴 + (𝐷‘𝑖)) + (0 · (𝐷‘𝑖)))) → ∃𝑚 ∈ (0...(𝐾 − 1))(𝐴 + (𝐷‘𝑖)) = ((𝐴 + (𝐷‘𝑖)) + (𝑚 · (𝐷‘𝑖)))) |
52 | 39, 48, 51 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ∃𝑚 ∈ (0...(𝐾 − 1))(𝐴 + (𝐷‘𝑖)) = ((𝐴 + (𝐷‘𝑖)) + (𝑚 · (𝐷‘𝑖)))) |
53 | 5 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐾 ∈ ℕ) |
54 | 53 | nnnn0d 12293 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → 𝐾 ∈
ℕ0) |
55 | | vdwapval 16674 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ ℕ0
∧ (𝐴 + (𝐷‘𝑖)) ∈ ℕ ∧ (𝐷‘𝑖) ∈ ℕ) → ((𝐴 + (𝐷‘𝑖)) ∈ ((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))(𝐴 + (𝐷‘𝑖)) = ((𝐴 + (𝐷‘𝑖)) + (𝑚 · (𝐷‘𝑖))))) |
56 | 54, 45, 40, 55 | syl3anc 1370 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → ((𝐴 + (𝐷‘𝑖)) ∈ ((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖)) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))(𝐴 + (𝐷‘𝑖)) = ((𝐴 + (𝐷‘𝑖)) + (𝑚 · (𝐷‘𝑖))))) |
57 | 52, 56 | mpbird 256 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐴 + (𝐷‘𝑖)) ∈ ((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖))) |
58 | 32, 57 | sseldd 3922 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐴 + (𝐷‘𝑖)) ∈ (1...𝑊)) |
59 | 58 | ralrimiva 3103 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)(𝐴 + (𝐷‘𝑖)) ∈ (1...𝑊)) |
60 | 25, 59, 14 | rspcdva 3562 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 + (𝐷‘1)) ∈ (1...𝑊)) |
61 | | elfzle2 13260 |
. . . . . . . . . . 11
⊢ ((𝐴 + (𝐷‘1)) ∈ (1...𝑊) → (𝐴 + (𝐷‘1)) ≤ 𝑊) |
62 | 60, 61 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 + (𝐷‘1)) ≤ 𝑊) |
63 | 9, 17, 19, 22, 62 | letrd 11132 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≤ 𝑊) |
64 | 1, 11 | eleqtrdi 2849 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈
(ℤ≥‘1)) |
65 | 18 | nnzd 12425 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ ℤ) |
66 | | elfz5 13248 |
. . . . . . . . . 10
⊢ ((𝐴 ∈
(ℤ≥‘1) ∧ 𝑊 ∈ ℤ) → (𝐴 ∈ (1...𝑊) ↔ 𝐴 ≤ 𝑊)) |
67 | 64, 65, 66 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 ∈ (1...𝑊) ↔ 𝐴 ≤ 𝑊)) |
68 | 63, 67 | mpbird 256 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ (1...𝑊)) |
69 | | eqidd 2739 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘𝐴)) |
70 | | ffn 6600 |
. . . . . . . . 9
⊢ (𝐹:(1...𝑊)⟶𝑅 → 𝐹 Fn (1...𝑊)) |
71 | | fniniseg 6937 |
. . . . . . . . 9
⊢ (𝐹 Fn (1...𝑊) → (𝐴 ∈ (◡𝐹 “ {(𝐹‘𝐴)}) ↔ (𝐴 ∈ (1...𝑊) ∧ (𝐹‘𝐴) = (𝐹‘𝐴)))) |
72 | 29, 70, 71 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∈ (◡𝐹 “ {(𝐹‘𝐴)}) ↔ (𝐴 ∈ (1...𝑊) ∧ (𝐹‘𝐴) = (𝐹‘𝐴)))) |
73 | 68, 69, 72 | mpbir2and 710 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ (◡𝐹 “ {(𝐹‘𝐴)})) |
74 | 73 | snssd 4742 |
. . . . . 6
⊢ (𝜑 → {𝐴} ⊆ (◡𝐹 “ {(𝐹‘𝐴)})) |
75 | | fveq2 6774 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → (𝐷‘𝑖) = (𝐷‘𝐼)) |
76 | 75 | oveq2d 7291 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐼 → (𝐴 + (𝐷‘𝑖)) = (𝐴 + (𝐷‘𝐼))) |
77 | 76, 75 | oveq12d 7293 |
. . . . . . . . 9
⊢ (𝑖 = 𝐼 → ((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖)) = ((𝐴 + (𝐷‘𝐼))(AP‘𝐾)(𝐷‘𝐼))) |
78 | 76 | fveq2d 6778 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝐼 → (𝐹‘(𝐴 + (𝐷‘𝑖))) = (𝐹‘(𝐴 + (𝐷‘𝐼)))) |
79 | 78 | sneqd 4573 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐼 → {(𝐹‘(𝐴 + (𝐷‘𝑖)))} = {(𝐹‘(𝐴 + (𝐷‘𝐼)))}) |
80 | 79 | imaeq2d 5969 |
. . . . . . . . 9
⊢ (𝑖 = 𝐼 → (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝑖)))}) = (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝐼)))})) |
81 | 77, 80 | sseq12d 3954 |
. . . . . . . 8
⊢ (𝑖 = 𝐼 → (((𝐴 + (𝐷‘𝑖))(AP‘𝐾)(𝐷‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝑖)))}) ↔ ((𝐴 + (𝐷‘𝐼))(AP‘𝐾)(𝐷‘𝐼)) ⊆ (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝐼)))}))) |
82 | 81, 26, 3 | rspcdva 3562 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 + (𝐷‘𝐼))(AP‘𝐾)(𝐷‘𝐼)) ⊆ (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝐼)))})) |
83 | | vdwlem1.e |
. . . . . . . . 9
⊢ (𝜑 → (𝐹‘𝐴) = (𝐹‘(𝐴 + (𝐷‘𝐼)))) |
84 | 83 | sneqd 4573 |
. . . . . . . 8
⊢ (𝜑 → {(𝐹‘𝐴)} = {(𝐹‘(𝐴 + (𝐷‘𝐼)))}) |
85 | 84 | imaeq2d 5969 |
. . . . . . 7
⊢ (𝜑 → (◡𝐹 “ {(𝐹‘𝐴)}) = (◡𝐹 “ {(𝐹‘(𝐴 + (𝐷‘𝐼)))})) |
86 | 82, 85 | sseqtrrd 3962 |
. . . . . 6
⊢ (𝜑 → ((𝐴 + (𝐷‘𝐼))(AP‘𝐾)(𝐷‘𝐼)) ⊆ (◡𝐹 “ {(𝐹‘𝐴)})) |
87 | 74, 86 | unssd 4120 |
. . . . 5
⊢ (𝜑 → ({𝐴} ∪ ((𝐴 + (𝐷‘𝐼))(AP‘𝐾)(𝐷‘𝐼))) ⊆ (◡𝐹 “ {(𝐹‘𝐴)})) |
88 | 8, 87 | eqsstrd 3959 |
. . . 4
⊢ (𝜑 → (𝐴(AP‘(𝐾 + 1))(𝐷‘𝐼)) ⊆ (◡𝐹 “ {(𝐹‘𝐴)})) |
89 | | oveq1 7282 |
. . . . . 6
⊢ (𝑎 = 𝐴 → (𝑎(AP‘(𝐾 + 1))𝑑) = (𝐴(AP‘(𝐾 + 1))𝑑)) |
90 | 89 | sseq1d 3952 |
. . . . 5
⊢ (𝑎 = 𝐴 → ((𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝐴)}) ↔ (𝐴(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝐴)}))) |
91 | | oveq2 7283 |
. . . . . 6
⊢ (𝑑 = (𝐷‘𝐼) → (𝐴(AP‘(𝐾 + 1))𝑑) = (𝐴(AP‘(𝐾 + 1))(𝐷‘𝐼))) |
92 | 91 | sseq1d 3952 |
. . . . 5
⊢ (𝑑 = (𝐷‘𝐼) → ((𝐴(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝐴)}) ↔ (𝐴(AP‘(𝐾 + 1))(𝐷‘𝐼)) ⊆ (◡𝐹 “ {(𝐹‘𝐴)}))) |
93 | 90, 92 | rspc2ev 3572 |
. . . 4
⊢ ((𝐴 ∈ ℕ ∧ (𝐷‘𝐼) ∈ ℕ ∧ (𝐴(AP‘(𝐾 + 1))(𝐷‘𝐼)) ⊆ (◡𝐹 “ {(𝐹‘𝐴)})) → ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝐴)})) |
94 | 1, 4, 88, 93 | syl3anc 1370 |
. . 3
⊢ (𝜑 → ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝐴)})) |
95 | | fvex 6787 |
. . . 4
⊢ (𝐹‘𝐴) ∈ V |
96 | | sneq 4571 |
. . . . . . 7
⊢ (𝑐 = (𝐹‘𝐴) → {𝑐} = {(𝐹‘𝐴)}) |
97 | 96 | imaeq2d 5969 |
. . . . . 6
⊢ (𝑐 = (𝐹‘𝐴) → (◡𝐹 “ {𝑐}) = (◡𝐹 “ {(𝐹‘𝐴)})) |
98 | 97 | sseq2d 3953 |
. . . . 5
⊢ (𝑐 = (𝐹‘𝐴) → ((𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝐴)}))) |
99 | 98 | 2rexbidv 3229 |
. . . 4
⊢ (𝑐 = (𝐹‘𝐴) → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {𝑐}) ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝐴)}))) |
100 | 95, 99 | spcev 3545 |
. . 3
⊢
(∃𝑎 ∈
ℕ ∃𝑑 ∈
ℕ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {(𝐹‘𝐴)}) → ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {𝑐})) |
101 | 94, 100 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {𝑐})) |
102 | | ovex 7308 |
. . 3
⊢
(1...𝑊) ∈
V |
103 | | peano2nn0 12273 |
. . . 4
⊢ (𝐾 ∈ ℕ0
→ (𝐾 + 1) ∈
ℕ0) |
104 | 6, 103 | syl 17 |
. . 3
⊢ (𝜑 → (𝐾 + 1) ∈
ℕ0) |
105 | 102, 104,
29 | vdwmc 16679 |
. 2
⊢ (𝜑 → ((𝐾 + 1) MonoAP 𝐹 ↔ ∃𝑐∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘(𝐾 + 1))𝑑) ⊆ (◡𝐹 “ {𝑐}))) |
106 | 101, 105 | mpbird 256 |
1
⊢ (𝜑 → (𝐾 + 1) MonoAP 𝐹) |